MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alexsublem Structured version   Visualization version   GIF version
Theorem alexsublem 23769
Description: Lemma for alexsub 23770. (Contributed by Mario Carneiro, 26-Aug-2015.)
Hypotheses
Ref Expression
alexsub.1 (πœ‘ β†’ 𝑋 ∈ UFL)
alexsub.2 (πœ‘ β†’ 𝑋 = βˆͺ 𝐡)
alexsub.3 (πœ‘ β†’ 𝐽 = (topGenβ€˜(fiβ€˜π΅)))
alexsub.4 ((πœ‘ ∧ (π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯)) β†’ βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑋 = βˆͺ 𝑦)
alexsub.5 (πœ‘ β†’ 𝐹 ∈ (UFilβ€˜π‘‹))
alexsub.6 (πœ‘ β†’ (𝐽 fLim 𝐹) = βˆ…)
Assertion
Ref Expression
alexsublem Β¬ πœ‘
Distinct variable groups:   π‘₯,𝑦,𝐡   π‘₯,𝐽,𝑦   πœ‘,π‘₯,𝑦   π‘₯,𝑋,𝑦   π‘₯,𝐹,𝑦
Proof of Theorem alexsublem
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 eldif 3959 . . . . . . . . . 10 (π‘₯ ∈ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) ↔ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹)))
2 alexsub.3 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐽 = (topGenβ€˜(fiβ€˜π΅)))
32eleq2d 2818 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑦 ∈ 𝐽 ↔ 𝑦 ∈ (topGenβ€˜(fiβ€˜π΅))))
43anbi1d 629 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦) ↔ (𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦)))
54biimpa 476 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ (𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦))
65adantlr 712 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ (𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦))
7 tg2 22689 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦) β†’ βˆƒπ‘§ ∈ (fiβ€˜π΅)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))
86, 7syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ βˆƒπ‘§ ∈ (fiβ€˜π΅)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))
9 alexsub.5 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐹 ∈ (UFilβ€˜π‘‹))
10 ufilfil 23629 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (UFilβ€˜π‘‹) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
119, 10syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐹 ∈ (Filβ€˜π‘‹))
1211ad3antrrr 727 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
13 alexsub.2 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑋 = βˆͺ 𝐡)
149elfvexd 6931 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑋 ∈ V)
1513, 14eqeltrrd 2833 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ βˆͺ 𝐡 ∈ V)
16 uniexb 7754 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐡 ∈ V ↔ βˆͺ 𝐡 ∈ V)
1715, 16sylibr 233 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝐡 ∈ V)
18 elfi2 9412 . . . . . . . . . . . . . . . . . . . . . 22 (𝐡 ∈ V β†’ (𝑧 ∈ (fiβ€˜π΅) ↔ βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦))
1917, 18syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑧 ∈ (fiβ€˜π΅) ↔ βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦))
2019adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ (𝑧 ∈ (fiβ€˜π΅) ↔ βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦))
2111ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
22 simplrr 775 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))
23 intss1 4968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ 𝑦 β†’ ∩ 𝑦 βŠ† 𝑧)
2423adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) β†’ ∩ 𝑦 βŠ† 𝑧)
25 simplr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) β†’ π‘₯ ∈ ∩ 𝑦)
2624, 25sseldd 3984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) β†’ π‘₯ ∈ 𝑧)
2726ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ π‘₯ ∈ 𝑧)
28 eldifsn 4791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ↔ (𝑦 ∈ (𝒫 𝐡 ∩ Fin) ∧ 𝑦 β‰  βˆ…))
2928simplbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) β†’ 𝑦 ∈ (𝒫 𝐡 ∩ Fin))
3029ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 ∈ (𝒫 𝐡 ∩ Fin))
31 elfpw 9357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (𝒫 𝐡 ∩ Fin) ↔ (𝑦 βŠ† 𝐡 ∧ 𝑦 ∈ Fin))
3231simplbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ (𝒫 𝐡 ∩ Fin) β†’ 𝑦 βŠ† 𝐡)
3330, 32syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 βŠ† 𝐡)
3433sselda 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ 𝐡)
3534anasss 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ 𝑧 ∈ 𝐡)
3635anim1i 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ∈ 𝐹))
37 eldif 3959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ (𝐡 βˆ– 𝐹) ↔ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ∈ 𝐹))
3836, 37sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ 𝑧 ∈ (𝐡 βˆ– 𝐹))
39 elunii 4914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((π‘₯ ∈ 𝑧 ∧ 𝑧 ∈ (𝐡 βˆ– 𝐹)) β†’ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))
4027, 38, 39syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))
4140ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ (Β¬ 𝑧 ∈ 𝐹 β†’ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹)))
4222, 41mt3d 148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ 𝑧 ∈ 𝐹)
4342expr 456 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ (𝑧 ∈ 𝑦 β†’ 𝑧 ∈ 𝐹))
4443ssrdv 3989 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 βŠ† 𝐹)
45 eldifsni 4794 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) β†’ 𝑦 β‰  βˆ…)
4645ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 β‰  βˆ…)
47 elinel2 4197 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (𝒫 𝐡 ∩ Fin) β†’ 𝑦 ∈ Fin)
4830, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 ∈ Fin)
49 elfir 9413 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ (𝑦 βŠ† 𝐹 ∧ 𝑦 β‰  βˆ… ∧ 𝑦 ∈ Fin)) β†’ ∩ 𝑦 ∈ (fiβ€˜πΉ))
5021, 44, 46, 48, 49syl13anc 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ ∩ 𝑦 ∈ (fiβ€˜πΉ))
51 filfi 23584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (fiβ€˜πΉ) = 𝐹)
5221, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ (fiβ€˜πΉ) = 𝐹)
5350, 52eleqtrd 2834 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ ∩ 𝑦 ∈ 𝐹)
5453expr 456 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})) β†’ (π‘₯ ∈ ∩ 𝑦 β†’ ∩ 𝑦 ∈ 𝐹))
55 eleq2 2821 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = ∩ 𝑦 β†’ (π‘₯ ∈ 𝑧 ↔ π‘₯ ∈ ∩ 𝑦))
56 eleq1 2820 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = ∩ 𝑦 β†’ (𝑧 ∈ 𝐹 ↔ ∩ 𝑦 ∈ 𝐹))
5755, 56imbi12d 343 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = ∩ 𝑦 β†’ ((π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹) ↔ (π‘₯ ∈ ∩ 𝑦 β†’ ∩ 𝑦 ∈ 𝐹)))
5854, 57syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})) β†’ (𝑧 = ∩ 𝑦 β†’ (π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹)))
5958rexlimdva 3154 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ (βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦 β†’ (π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹)))
6020, 59sylbid 239 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ (𝑧 ∈ (fiβ€˜π΅) β†’ (π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹)))
6160imp32 418 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ π‘₯ ∈ 𝑧)) β†’ 𝑧 ∈ 𝐹)
6261adantrrr 722 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑧 ∈ 𝐹)
6362adantlr 712 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑧 ∈ 𝐹)
64 elssuni 4942 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ 𝐽 β†’ 𝑦 βŠ† βˆͺ 𝐽)
6564ad2antrl 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑦 βŠ† βˆͺ 𝐽)
66 fibas 22701 . . . . . . . . . . . . . . . . . . . . . . 23 (fiβ€˜π΅) ∈ TopBases
67 tgtopon 22695 . . . . . . . . . . . . . . . . . . . . . . 23 ((fiβ€˜π΅) ∈ TopBases β†’ (topGenβ€˜(fiβ€˜π΅)) ∈ (TopOnβ€˜βˆͺ (fiβ€˜π΅)))
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (topGenβ€˜(fiβ€˜π΅)) ∈ (TopOnβ€˜βˆͺ (fiβ€˜π΅))
692, 68eqeltrdi 2840 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜βˆͺ (fiβ€˜π΅)))
70 fiuni 9426 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐡 ∈ V β†’ βˆͺ 𝐡 = βˆͺ (fiβ€˜π΅))
7117, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ βˆͺ 𝐡 = βˆͺ (fiβ€˜π΅))
7213, 71eqtrd 2771 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝑋 = βˆͺ (fiβ€˜π΅))
7372fveq2d 6896 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (TopOnβ€˜π‘‹) = (TopOnβ€˜βˆͺ (fiβ€˜π΅)))
7469, 73eleqtrrd 2835 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
75 toponuni 22637 . . . . . . . . . . . . . . . . . . . 20 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 = βˆͺ 𝐽)
7776ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑋 = βˆͺ 𝐽)
7865, 77sseqtrrd 4024 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑦 βŠ† 𝑋)
7978adantr 480 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑦 βŠ† 𝑋)
80 simprrr 779 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑧 βŠ† 𝑦)
81 filss 23578 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦 βŠ† 𝑋 ∧ 𝑧 βŠ† 𝑦)) β†’ 𝑦 ∈ 𝐹)
8212, 63, 79, 80, 81syl13anc 1371 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑦 ∈ 𝐹)
838, 82rexlimddv 3160 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑦 ∈ 𝐹)
8483expr 456 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ 𝑦 ∈ 𝐽) β†’ (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))
8584ralrimiva 3145 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))
8685expr 456 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹) β†’ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹)))
8786imdistanda 571 . . . . . . . . . 10 (πœ‘ β†’ ((π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹)) β†’ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
881, 87biimtrid 241 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) β†’ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
89 flimopn 23700 . . . . . . . . . 10 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐹 ∈ (Filβ€˜π‘‹)) β†’ (π‘₯ ∈ (𝐽 fLim 𝐹) ↔ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
9074, 11, 89syl2anc 583 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (𝐽 fLim 𝐹) ↔ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
9188, 90sylibrd 258 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) β†’ π‘₯ ∈ (𝐽 fLim 𝐹)))
9291ssrdv 3989 . . . . . . 7 (πœ‘ β†’ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) βŠ† (𝐽 fLim 𝐹))
93 alexsub.6 . . . . . . 7 (πœ‘ β†’ (𝐽 fLim 𝐹) = βˆ…)
94 sseq0 4400 . . . . . . 7 (((𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) βŠ† (𝐽 fLim 𝐹) ∧ (𝐽 fLim 𝐹) = βˆ…) β†’ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) = βˆ…)
9592, 93, 94syl2anc 583 . . . . . 6 (πœ‘ β†’ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) = βˆ…)
96 ssdif0 4364 . . . . . 6 (𝑋 βŠ† βˆͺ (𝐡 βˆ– 𝐹) ↔ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) = βˆ…)
9795, 96sylibr 233 . . . . 5 (πœ‘ β†’ 𝑋 βŠ† βˆͺ (𝐡 βˆ– 𝐹))
98 difss 4132 . . . . . . 7 (𝐡 βˆ– 𝐹) βŠ† 𝐡
9998unissi 4918 . . . . . 6 βˆͺ (𝐡 βˆ– 𝐹) βŠ† βˆͺ 𝐡
10099, 13sseqtrrid 4036 . . . . 5 (πœ‘ β†’ βˆͺ (𝐡 βˆ– 𝐹) βŠ† 𝑋)
10197, 100eqssd 4000 . . . 4 (πœ‘ β†’ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))
102101, 98jctil 519 . . 3 (πœ‘ β†’ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹)))
10317difexd 5330 . . . . 5 (πœ‘ β†’ (𝐡 βˆ– 𝐹) ∈ V)
104103adantr 480 . . . 4 ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ (𝐡 βˆ– 𝐹) ∈ V)
105 sseq1 4008 . . . . . . . 8 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (π‘₯ βŠ† 𝐡 ↔ (𝐡 βˆ– 𝐹) βŠ† 𝐡))
106 unieq 4920 . . . . . . . . 9 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ βˆͺ π‘₯ = βˆͺ (𝐡 βˆ– 𝐹))
107106eqeq2d 2742 . . . . . . . 8 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (𝑋 = βˆͺ π‘₯ ↔ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹)))
108105, 107anbi12d 630 . . . . . . 7 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ ((π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯) ↔ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))))
109108anbi2d 628 . . . . . 6 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ ((πœ‘ ∧ (π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯)) ↔ (πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹)))))
110 pweq 4617 . . . . . . . 8 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ 𝒫 π‘₯ = 𝒫 (𝐡 βˆ– 𝐹))
111110ineq1d 4212 . . . . . . 7 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (𝒫 π‘₯ ∩ Fin) = (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin))
112111rexeqdv 3325 . . . . . 6 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑋 = βˆͺ 𝑦 ↔ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦))
113109, 112imbi12d 343 . . . . 5 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (((πœ‘ ∧ (π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯)) β†’ βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑋 = βˆͺ 𝑦) ↔ ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)))
114 alexsub.4 . . . . 5 ((πœ‘ ∧ (π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯)) β†’ βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑋 = βˆͺ 𝑦)
115113, 114vtoclg 3557 . . . 4 ((𝐡 βˆ– 𝐹) ∈ V β†’ ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦))
116104, 115mpcom 38 . . 3 ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)
117102, 116mpdan 684 . 2 (πœ‘ β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)
118 unieq 4920 . . . . . . 7 (𝑦 = βˆ… β†’ βˆͺ 𝑦 = βˆͺ βˆ…)
119 uni0 4940 . . . . . . 7 βˆͺ βˆ… = βˆ…
120118, 119eqtrdi 2787 . . . . . 6 (𝑦 = βˆ… β†’ βˆͺ 𝑦 = βˆ…)
121120neeq2d 3000 . . . . 5 (𝑦 = βˆ… β†’ (𝑋 β‰  βˆͺ 𝑦 ↔ 𝑋 β‰  βˆ…))
122 difssd 4133 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ (𝑋 βˆ– 𝑧) βŠ† 𝑋)
123122ralrimivw 3149 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) βŠ† 𝑋)
124 riinn0 5087 . . . . . . . . . 10 ((βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) βŠ† 𝑋 ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧))
125123, 124sylan 579 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧))
12614ad2antrr 723 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑋 ∈ V)
127126difexd 5330 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 βˆ– 𝑧) ∈ V)
128127ralrimivw 3149 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) ∈ V)
129 dfiin2g 5036 . . . . . . . . . . 11 (βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) ∈ V β†’ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧) = ∩ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)})
130128, 129syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧) = ∩ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)})
131 eqid 2731 . . . . . . . . . . . 12 (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧))
132131rnmpt 5955 . . . . . . . . . . 11 ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)}
133132inteqi 4955 . . . . . . . . . 10 ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = ∩ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)}
134130, 133eqtr4di 2789 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)))
135125, 134eqtrd 2771 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)))
13611ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
137 elfpw 9357 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin) ↔ (𝑦 βŠ† (𝐡 βˆ– 𝐹) ∧ 𝑦 ∈ Fin))
138137simplbi 497 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin) β†’ 𝑦 βŠ† (𝐡 βˆ– 𝐹))
139138ad2antlr 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 βŠ† (𝐡 βˆ– 𝐹))
140139sselda 3983 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ (𝐡 βˆ– 𝐹))
141140eldifbd 3962 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ Β¬ 𝑧 ∈ 𝐹)
1429ad3antrrr 727 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝐹 ∈ (UFilβ€˜π‘‹))
143139difss2d 4135 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 βŠ† 𝐡)
144143sselda 3983 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ 𝐡)
145 elssuni 4942 . . . . . . . . . . . . . . 15 (𝑧 ∈ 𝐡 β†’ 𝑧 βŠ† βˆͺ 𝐡)
146144, 145syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 βŠ† βˆͺ 𝐡)
14713ad3antrrr 727 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑋 = βˆͺ 𝐡)
148146, 147sseqtrrd 4024 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 βŠ† 𝑋)
149 ufilb 23631 . . . . . . . . . . . . 13 ((𝐹 ∈ (UFilβ€˜π‘‹) ∧ 𝑧 βŠ† 𝑋) β†’ (Β¬ 𝑧 ∈ 𝐹 ↔ (𝑋 βˆ– 𝑧) ∈ 𝐹))
150142, 148, 149syl2anc 583 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ (Β¬ 𝑧 ∈ 𝐹 ↔ (𝑋 βˆ– 𝑧) ∈ 𝐹))
151141, 150mpbid 231 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ (𝑋 βˆ– 𝑧) ∈ 𝐹)
152151fmpttd 7117 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)):π‘¦βŸΆπΉ)
153152frnd 6726 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) βŠ† 𝐹)
154131, 151dmmptd 6696 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = 𝑦)
155 simpr 484 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 β‰  βˆ…)
156154, 155eqnetrd 3007 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
157 dm0rn0 5925 . . . . . . . . . . 11 (dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = βˆ… ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = βˆ…)
158157necon3bii 2992 . . . . . . . . . 10 (dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ… ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
159156, 158sylib 217 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
160 elinel2 4197 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin) β†’ 𝑦 ∈ Fin)
161160ad2antlr 724 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 ∈ Fin)
162 abrexfi 9355 . . . . . . . . . . 11 (𝑦 ∈ Fin β†’ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)} ∈ Fin)
163132, 162eqeltrid 2836 . . . . . . . . . 10 (𝑦 ∈ Fin β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) ∈ Fin)
164161, 163syl 17 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) ∈ Fin)
165 filintn0 23586 . . . . . . . . 9 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ (ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) βŠ† 𝐹 ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ… ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) ∈ Fin)) β†’ ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
166136, 153, 159, 164, 165syl13anc 1371 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
167135, 166eqnetrd 3007 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) β‰  βˆ…)
168 disj3 4454 . . . . . . . 8 ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = βˆ… ↔ 𝑋 = (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)))
169168necon3bii 2992 . . . . . . 7 ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) β‰  βˆ… ↔ 𝑋 β‰  (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)))
170167, 169sylib 217 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑋 β‰  (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)))
171 iundif2 5078 . . . . . . 7 βˆͺ 𝑧 ∈ 𝑦 (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧))
172 dfss4 4259 . . . . . . . . . 10 (𝑧 βŠ† 𝑋 ↔ (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = 𝑧)
173148, 172sylib 217 . . . . . . . . 9 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = 𝑧)
174173iuneq2dv 5022 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ βˆͺ 𝑧 ∈ 𝑦 (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = βˆͺ 𝑧 ∈ 𝑦 𝑧)
175 uniiun 5062 . . . . . . . 8 βˆͺ 𝑦 = βˆͺ 𝑧 ∈ 𝑦 𝑧
176174, 175eqtr4di 2789 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ βˆͺ 𝑧 ∈ 𝑦 (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = βˆͺ 𝑦)
177171, 176eqtr3id 2785 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = βˆͺ 𝑦)
178170, 177neeqtrd 3009 . . . . 5 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑋 β‰  βˆͺ 𝑦)
17911adantr 480 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
180 filtop 23580 . . . . . 6 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝑋 ∈ 𝐹)
181 fileln0 23575 . . . . . 6 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑋 ∈ 𝐹) β†’ 𝑋 β‰  βˆ…)
182179, 180, 181syl2anc2 584 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ 𝑋 β‰  βˆ…)
183121, 178, 182pm2.61ne 3026 . . . 4 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ 𝑋 β‰  βˆͺ 𝑦)
184183neneqd 2944 . . 3 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ Β¬ 𝑋 = βˆͺ 𝑦)
185184nrexdv 3148 . 2 (πœ‘ β†’ Β¬ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)
186117, 185pm2.65i 193 1 Β¬ πœ‘
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1540   ∈ wcel 2105  {cab 2708   β‰  wne 2939  βˆ€wral 3060  βˆƒwrex 3069  Vcvv 3473   βˆ– cdif 3946   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  π’« cpw 4603  {csn 4629  βˆͺ cuni 4909  βˆ© cint 4951  βˆͺ ciun 4998  βˆ© ciin 4999   ↦ cmpt 5232  dom cdm 5677  ran crn 5678  β€˜cfv 6544  (class class class)co 7412  Fincfn 8942  ficfi 9408  topGenctg 17388  TopOnctopon 22633  TopBasesctb 22669  Filcfil 23570  UFilcufil 23624  UFLcufl 23625   fLim cflim 23659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7859  df-1st 7978  df-2nd 7979  df-1o 8469  df-er 8706  df-en 8943  df-dom 8944  df-fin 8946  df-fi 9409  df-topgen 17394  df-fbas 21142  df-top 22617  df-topon 22634  df-bases 22670  df-ntr 22745  df-nei 22823  df-fil 23571  df-ufil 23626  df-flim 23664
This theorem is referenced by:  alexsub  23770
  Copyright terms: Public domain W3C validator