Step | Hyp | Ref
| Expression |
1 | | fmfnfm.l |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) |
2 | | filin 21468 |
. . . . . . . . 9
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑦 ∈ 𝐿 ∧ 𝑧 ∈ 𝐿) → (𝑦 ∩ 𝑧) ∈ 𝐿) |
3 | 2 | 3expb 1258 |
. . . . . . . 8
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝑦 ∈ 𝐿 ∧ 𝑧 ∈ 𝐿)) → (𝑦 ∩ 𝑧) ∈ 𝐿) |
4 | 1, 3 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐿 ∧ 𝑧 ∈ 𝐿)) → (𝑦 ∩ 𝑧) ∈ 𝐿) |
5 | | fmfnfm.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑌⟶𝑋) |
6 | | ffun 5961 |
. . . . . . . . 9
⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹) |
7 | | funcnvcnv 5870 |
. . . . . . . . 9
⊢ (Fun
𝐹 → Fun ◡◡𝐹) |
8 | | imain 5888 |
. . . . . . . . . 10
⊢ (Fun
◡◡𝐹 → (◡𝐹 “ (𝑦 ∩ 𝑧)) = ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ 𝑧))) |
9 | 8 | eqcomd 2616 |
. . . . . . . . 9
⊢ (Fun
◡◡𝐹 → ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ 𝑧)) = (◡𝐹 “ (𝑦 ∩ 𝑧))) |
10 | 5, 6, 7, 9 | 4syl 19 |
. . . . . . . 8
⊢ (𝜑 → ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ 𝑧)) = (◡𝐹 “ (𝑦 ∩ 𝑧))) |
11 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐿 ∧ 𝑧 ∈ 𝐿)) → ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ 𝑧)) = (◡𝐹 “ (𝑦 ∩ 𝑧))) |
12 | | imaeq2 5381 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 ∩ 𝑧) → (◡𝐹 “ 𝑥) = (◡𝐹 “ (𝑦 ∩ 𝑧))) |
13 | 12 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∩ 𝑧) → (((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ 𝑧)) = (◡𝐹 “ 𝑥) ↔ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ 𝑧)) = (◡𝐹 “ (𝑦 ∩ 𝑧)))) |
14 | 13 | rspcev 3282 |
. . . . . . 7
⊢ (((𝑦 ∩ 𝑧) ∈ 𝐿 ∧ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ 𝑧)) = (◡𝐹 “ (𝑦 ∩ 𝑧))) → ∃𝑥 ∈ 𝐿 ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ 𝑧)) = (◡𝐹 “ 𝑥)) |
15 | 4, 11, 14 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐿 ∧ 𝑧 ∈ 𝐿)) → ∃𝑥 ∈ 𝐿 ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ 𝑧)) = (◡𝐹 “ 𝑥)) |
16 | | ineq12 3771 |
. . . . . . . 8
⊢ ((𝑠 = (◡𝐹 “ 𝑦) ∧ 𝑡 = (◡𝐹 “ 𝑧)) → (𝑠 ∩ 𝑡) = ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ 𝑧))) |
17 | 16 | eqeq1d 2612 |
. . . . . . 7
⊢ ((𝑠 = (◡𝐹 “ 𝑦) ∧ 𝑡 = (◡𝐹 “ 𝑧)) → ((𝑠 ∩ 𝑡) = (◡𝐹 “ 𝑥) ↔ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ 𝑧)) = (◡𝐹 “ 𝑥))) |
18 | 17 | rexbidv 3034 |
. . . . . 6
⊢ ((𝑠 = (◡𝐹 “ 𝑦) ∧ 𝑡 = (◡𝐹 “ 𝑧)) → (∃𝑥 ∈ 𝐿 (𝑠 ∩ 𝑡) = (◡𝐹 “ 𝑥) ↔ ∃𝑥 ∈ 𝐿 ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ 𝑧)) = (◡𝐹 “ 𝑥))) |
19 | 15, 18 | syl5ibrcom 236 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐿 ∧ 𝑧 ∈ 𝐿)) → ((𝑠 = (◡𝐹 “ 𝑦) ∧ 𝑡 = (◡𝐹 “ 𝑧)) → ∃𝑥 ∈ 𝐿 (𝑠 ∩ 𝑡) = (◡𝐹 “ 𝑥))) |
20 | 19 | rexlimdvva 3020 |
. . . 4
⊢ (𝜑 → (∃𝑦 ∈ 𝐿 ∃𝑧 ∈ 𝐿 (𝑠 = (◡𝐹 “ 𝑦) ∧ 𝑡 = (◡𝐹 “ 𝑧)) → ∃𝑥 ∈ 𝐿 (𝑠 ∩ 𝑡) = (◡𝐹 “ 𝑥))) |
21 | | imaeq2 5381 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝑦)) |
22 | 21 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑠 = (◡𝐹 “ 𝑥) ↔ 𝑠 = (◡𝐹 “ 𝑦))) |
23 | 22 | cbvrexv 3148 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐿 𝑠 = (◡𝐹 “ 𝑥) ↔ ∃𝑦 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑦)) |
24 | | imaeq2 5381 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝑧)) |
25 | 24 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑡 = (◡𝐹 “ 𝑥) ↔ 𝑡 = (◡𝐹 “ 𝑧))) |
26 | 25 | cbvrexv 3148 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐿 𝑡 = (◡𝐹 “ 𝑥) ↔ ∃𝑧 ∈ 𝐿 𝑡 = (◡𝐹 “ 𝑧)) |
27 | 23, 26 | anbi12i 729 |
. . . . 5
⊢
((∃𝑥 ∈
𝐿 𝑠 = (◡𝐹 “ 𝑥) ∧ ∃𝑥 ∈ 𝐿 𝑡 = (◡𝐹 “ 𝑥)) ↔ (∃𝑦 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑦) ∧ ∃𝑧 ∈ 𝐿 𝑡 = (◡𝐹 “ 𝑧))) |
28 | | vex 3176 |
. . . . . . 7
⊢ 𝑠 ∈ V |
29 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) |
30 | 29 | elrnmpt 5293 |
. . . . . . 7
⊢ (𝑠 ∈ V → (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥))) |
31 | 28, 30 | ax-mp 5 |
. . . . . 6
⊢ (𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥)) |
32 | | vex 3176 |
. . . . . . 7
⊢ 𝑡 ∈ V |
33 | 29 | elrnmpt 5293 |
. . . . . . 7
⊢ (𝑡 ∈ V → (𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑡 = (◡𝐹 “ 𝑥))) |
34 | 32, 33 | ax-mp 5 |
. . . . . 6
⊢ (𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑡 = (◡𝐹 “ 𝑥)) |
35 | 31, 34 | anbi12i 729 |
. . . . 5
⊢ ((𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ 𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) ∧ ∃𝑥 ∈ 𝐿 𝑡 = (◡𝐹 “ 𝑥))) |
36 | | reeanv 3086 |
. . . . 5
⊢
(∃𝑦 ∈
𝐿 ∃𝑧 ∈ 𝐿 (𝑠 = (◡𝐹 “ 𝑦) ∧ 𝑡 = (◡𝐹 “ 𝑧)) ↔ (∃𝑦 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑦) ∧ ∃𝑧 ∈ 𝐿 𝑡 = (◡𝐹 “ 𝑧))) |
37 | 27, 35, 36 | 3bitr4i 291 |
. . . 4
⊢ ((𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ 𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ↔ ∃𝑦 ∈ 𝐿 ∃𝑧 ∈ 𝐿 (𝑠 = (◡𝐹 “ 𝑦) ∧ 𝑡 = (◡𝐹 “ 𝑧))) |
38 | 28 | inex1 4727 |
. . . . 5
⊢ (𝑠 ∩ 𝑡) ∈ V |
39 | 29 | elrnmpt 5293 |
. . . . 5
⊢ ((𝑠 ∩ 𝑡) ∈ V → ((𝑠 ∩ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (𝑠 ∩ 𝑡) = (◡𝐹 “ 𝑥))) |
40 | 38, 39 | ax-mp 5 |
. . . 4
⊢ ((𝑠 ∩ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 (𝑠 ∩ 𝑡) = (◡𝐹 “ 𝑥)) |
41 | 20, 37, 40 | 3imtr4g 284 |
. . 3
⊢ (𝜑 → ((𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∧ 𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) → (𝑠 ∩ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) |
42 | 41 | ralrimivv 2953 |
. 2
⊢ (𝜑 → ∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) |
43 | | mptexg 6389 |
. . 3
⊢ (𝐿 ∈ (Fil‘𝑋) → (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) |
44 | | rnexg 6990 |
. . 3
⊢ ((𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V) |
45 | | inficl 8214 |
. . 3
⊢ (ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ V → (∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) = ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) |
46 | 1, 43, 44, 45 | 4syl 19 |
. 2
⊢ (𝜑 → (∀𝑠 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) = ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) |
47 | 42, 46 | mpbid 221 |
1
⊢ (𝜑 → (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) = ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) |