MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alexsublem Structured version   Visualization version   GIF version
Theorem alexsublem 23768
Description: Lemma for alexsub 23769. (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 3957 . . . . . . . . . 10 (π‘₯ ∈ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) ↔ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹)))
2 alexsub.3 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐽 = (topGenβ€˜(fiβ€˜π΅)))
32eleq2d 2817 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑦 ∈ 𝐽 ↔ 𝑦 ∈ (topGenβ€˜(fiβ€˜π΅))))
43anbi1d 628 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦) ↔ (𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦)))
54biimpa 475 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ (𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦))
65adantlr 711 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ (𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦))
7 tg2 22688 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦) β†’ βˆƒπ‘§ ∈ (fiβ€˜π΅)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))
86, 7syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ βˆƒπ‘§ ∈ (fiβ€˜π΅)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))
9 alexsub.5 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐹 ∈ (UFilβ€˜π‘‹))
10 ufilfil 23628 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (UFilβ€˜π‘‹) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
119, 10syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐹 ∈ (Filβ€˜π‘‹))
1211ad3antrrr 726 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
13 alexsub.2 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑋 = βˆͺ 𝐡)
149elfvexd 6929 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑋 ∈ V)
1513, 14eqeltrrd 2832 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ βˆͺ 𝐡 ∈ V)
16 uniexb 7753 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐡 ∈ V ↔ βˆͺ 𝐡 ∈ V)
1715, 16sylibr 233 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝐡 ∈ V)
18 elfi2 9411 . . . . . . . . . . . . . . . . . . . . . 22 (𝐡 ∈ V β†’ (𝑧 ∈ (fiβ€˜π΅) ↔ βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦))
1917, 18syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑧 ∈ (fiβ€˜π΅) ↔ βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦))
2019adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ (𝑧 ∈ (fiβ€˜π΅) ↔ βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦))
2111ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
22 simplrr 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))
23 intss1 4966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ 𝑦 β†’ ∩ 𝑦 βŠ† 𝑧)
2423adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) β†’ ∩ 𝑦 βŠ† 𝑧)
25 simplr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) β†’ π‘₯ ∈ ∩ 𝑦)
2624, 25sseldd 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) β†’ π‘₯ ∈ 𝑧)
2726ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ π‘₯ ∈ 𝑧)
28 eldifsn 4789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ↔ (𝑦 ∈ (𝒫 𝐡 ∩ Fin) ∧ 𝑦 β‰  βˆ…))
2928simplbi 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) β†’ 𝑦 ∈ (𝒫 𝐡 ∩ Fin))
3029ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 ∈ (𝒫 𝐡 ∩ Fin))
31 elfpw 9356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (𝒫 𝐡 ∩ Fin) ↔ (𝑦 βŠ† 𝐡 ∧ 𝑦 ∈ Fin))
3231simplbi 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ (𝒫 𝐡 ∩ Fin) β†’ 𝑦 βŠ† 𝐡)
3330, 32syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 βŠ† 𝐡)
3433sselda 3981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ 𝐡)
3534anasss 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ 𝑧 ∈ 𝐡)
3635anim1i 613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ∈ 𝐹))
37 eldif 3957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ (𝐡 βˆ– 𝐹) ↔ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ∈ 𝐹))
3836, 37sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ 𝑧 ∈ (𝐡 βˆ– 𝐹))
39 elunii 4912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((π‘₯ ∈ 𝑧 ∧ 𝑧 ∈ (𝐡 βˆ– 𝐹)) β†’ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))
4027, 38, 39syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))
4140ex 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ (Β¬ 𝑧 ∈ 𝐹 β†’ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹)))
4222, 41mt3d 148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ 𝑧 ∈ 𝐹)
4342expr 455 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ (𝑧 ∈ 𝑦 β†’ 𝑧 ∈ 𝐹))
4443ssrdv 3987 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 βŠ† 𝐹)
45 eldifsni 4792 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) β†’ 𝑦 β‰  βˆ…)
4645ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 β‰  βˆ…)
47 elinel2 4195 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (𝒫 𝐡 ∩ Fin) β†’ 𝑦 ∈ Fin)
4830, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 ∈ Fin)
49 elfir 9412 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ (𝑦 βŠ† 𝐹 ∧ 𝑦 β‰  βˆ… ∧ 𝑦 ∈ Fin)) β†’ ∩ 𝑦 ∈ (fiβ€˜πΉ))
5021, 44, 46, 48, 49syl13anc 1370 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ ∩ 𝑦 ∈ (fiβ€˜πΉ))
51 filfi 23583 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (fiβ€˜πΉ) = 𝐹)
5221, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ (fiβ€˜πΉ) = 𝐹)
5350, 52eleqtrd 2833 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ ∩ 𝑦 ∈ 𝐹)
5453expr 455 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})) β†’ (π‘₯ ∈ ∩ 𝑦 β†’ ∩ 𝑦 ∈ 𝐹))
55 eleq2 2820 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = ∩ 𝑦 β†’ (π‘₯ ∈ 𝑧 ↔ π‘₯ ∈ ∩ 𝑦))
56 eleq1 2819 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = ∩ 𝑦 β†’ (𝑧 ∈ 𝐹 ↔ ∩ 𝑦 ∈ 𝐹))
5755, 56imbi12d 343 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = ∩ 𝑦 β†’ ((π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹) ↔ (π‘₯ ∈ ∩ 𝑦 β†’ ∩ 𝑦 ∈ 𝐹)))
5854, 57syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})) β†’ (𝑧 = ∩ 𝑦 β†’ (π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹)))
5958rexlimdva 3153 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ (βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦 β†’ (π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹)))
6020, 59sylbid 239 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ (𝑧 ∈ (fiβ€˜π΅) β†’ (π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹)))
6160imp32 417 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ π‘₯ ∈ 𝑧)) β†’ 𝑧 ∈ 𝐹)
6261adantrrr 721 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑧 ∈ 𝐹)
6362adantlr 711 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑧 ∈ 𝐹)
64 elssuni 4940 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ 𝐽 β†’ 𝑦 βŠ† βˆͺ 𝐽)
6564ad2antrl 724 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑦 βŠ† βˆͺ 𝐽)
66 fibas 22700 . . . . . . . . . . . . . . . . . . . . . . 23 (fiβ€˜π΅) ∈ TopBases
67 tgtopon 22694 . . . . . . . . . . . . . . . . . . . . . . 23 ((fiβ€˜π΅) ∈ TopBases β†’ (topGenβ€˜(fiβ€˜π΅)) ∈ (TopOnβ€˜βˆͺ (fiβ€˜π΅)))
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (topGenβ€˜(fiβ€˜π΅)) ∈ (TopOnβ€˜βˆͺ (fiβ€˜π΅))
692, 68eqeltrdi 2839 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜βˆͺ (fiβ€˜π΅)))
70 fiuni 9425 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐡 ∈ V β†’ βˆͺ 𝐡 = βˆͺ (fiβ€˜π΅))
7117, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ βˆͺ 𝐡 = βˆͺ (fiβ€˜π΅))
7213, 71eqtrd 2770 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝑋 = βˆͺ (fiβ€˜π΅))
7372fveq2d 6894 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (TopOnβ€˜π‘‹) = (TopOnβ€˜βˆͺ (fiβ€˜π΅)))
7469, 73eleqtrrd 2834 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
75 toponuni 22636 . . . . . . . . . . . . . . . . . . . 20 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 = βˆͺ 𝐽)
7776ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑋 = βˆͺ 𝐽)
7865, 77sseqtrrd 4022 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑦 βŠ† 𝑋)
7978adantr 479 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑦 βŠ† 𝑋)
80 simprrr 778 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑧 βŠ† 𝑦)
81 filss 23577 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦 βŠ† 𝑋 ∧ 𝑧 βŠ† 𝑦)) β†’ 𝑦 ∈ 𝐹)
8212, 63, 79, 80, 81syl13anc 1370 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑦 ∈ 𝐹)
838, 82rexlimddv 3159 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑦 ∈ 𝐹)
8483expr 455 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ 𝑦 ∈ 𝐽) β†’ (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))
8584ralrimiva 3144 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))
8685expr 455 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹) β†’ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹)))
8786imdistanda 570 . . . . . . . . . 10 (πœ‘ β†’ ((π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹)) β†’ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
881, 87biimtrid 241 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) β†’ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
89 flimopn 23699 . . . . . . . . . 10 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐹 ∈ (Filβ€˜π‘‹)) β†’ (π‘₯ ∈ (𝐽 fLim 𝐹) ↔ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
9074, 11, 89syl2anc 582 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (𝐽 fLim 𝐹) ↔ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
9188, 90sylibrd 258 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) β†’ π‘₯ ∈ (𝐽 fLim 𝐹)))
9291ssrdv 3987 . . . . . . 7 (πœ‘ β†’ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) βŠ† (𝐽 fLim 𝐹))
93 alexsub.6 . . . . . . 7 (πœ‘ β†’ (𝐽 fLim 𝐹) = βˆ…)
94 sseq0 4398 . . . . . . 7 (((𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) βŠ† (𝐽 fLim 𝐹) ∧ (𝐽 fLim 𝐹) = βˆ…) β†’ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) = βˆ…)
9592, 93, 94syl2anc 582 . . . . . 6 (πœ‘ β†’ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) = βˆ…)
96 ssdif0 4362 . . . . . 6 (𝑋 βŠ† βˆͺ (𝐡 βˆ– 𝐹) ↔ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) = βˆ…)
9795, 96sylibr 233 . . . . 5 (πœ‘ β†’ 𝑋 βŠ† βˆͺ (𝐡 βˆ– 𝐹))
98 difss 4130 . . . . . . 7 (𝐡 βˆ– 𝐹) βŠ† 𝐡
9998unissi 4916 . . . . . 6 βˆͺ (𝐡 βˆ– 𝐹) βŠ† βˆͺ 𝐡
10099, 13sseqtrrid 4034 . . . . 5 (πœ‘ β†’ βˆͺ (𝐡 βˆ– 𝐹) βŠ† 𝑋)
10197, 100eqssd 3998 . . . 4 (πœ‘ β†’ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))
102101, 98jctil 518 . . 3 (πœ‘ β†’ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹)))
10317difexd 5328 . . . . 5 (πœ‘ β†’ (𝐡 βˆ– 𝐹) ∈ V)
104103adantr 479 . . . 4 ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ (𝐡 βˆ– 𝐹) ∈ V)
105 sseq1 4006 . . . . . . . 8 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (π‘₯ βŠ† 𝐡 ↔ (𝐡 βˆ– 𝐹) βŠ† 𝐡))
106 unieq 4918 . . . . . . . . 9 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ βˆͺ π‘₯ = βˆͺ (𝐡 βˆ– 𝐹))
107106eqeq2d 2741 . . . . . . . 8 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (𝑋 = βˆͺ π‘₯ ↔ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹)))
108105, 107anbi12d 629 . . . . . . 7 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ ((π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯) ↔ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))))
109108anbi2d 627 . . . . . 6 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ ((πœ‘ ∧ (π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯)) ↔ (πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹)))))
110 pweq 4615 . . . . . . . 8 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ 𝒫 π‘₯ = 𝒫 (𝐡 βˆ– 𝐹))
111110ineq1d 4210 . . . . . . 7 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (𝒫 π‘₯ ∩ Fin) = (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin))
112111rexeqdv 3324 . . . . . 6 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑋 = βˆͺ 𝑦 ↔ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦))
113109, 112imbi12d 343 . . . . 5 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (((πœ‘ ∧ (π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯)) β†’ βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑋 = βˆͺ 𝑦) ↔ ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)))
114 alexsub.4 . . . . 5 ((πœ‘ ∧ (π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯)) β†’ βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑋 = βˆͺ 𝑦)
115113, 114vtoclg 3541 . . . 4 ((𝐡 βˆ– 𝐹) ∈ V β†’ ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦))
116104, 115mpcom 38 . . 3 ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)
117102, 116mpdan 683 . 2 (πœ‘ β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)
118 unieq 4918 . . . . . . 7 (𝑦 = βˆ… β†’ βˆͺ 𝑦 = βˆͺ βˆ…)
119 uni0 4938 . . . . . . 7 βˆͺ βˆ… = βˆ…
120118, 119eqtrdi 2786 . . . . . 6 (𝑦 = βˆ… β†’ βˆͺ 𝑦 = βˆ…)
121120neeq2d 2999 . . . . 5 (𝑦 = βˆ… β†’ (𝑋 β‰  βˆͺ 𝑦 ↔ 𝑋 β‰  βˆ…))
122 difssd 4131 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ (𝑋 βˆ– 𝑧) βŠ† 𝑋)
123122ralrimivw 3148 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) βŠ† 𝑋)
124 riinn0 5085 . . . . . . . . . 10 ((βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) βŠ† 𝑋 ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧))
125123, 124sylan 578 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧))
12614ad2antrr 722 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑋 ∈ V)
127126difexd 5328 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 βˆ– 𝑧) ∈ V)
128127ralrimivw 3148 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) ∈ V)
129 dfiin2g 5034 . . . . . . . . . . 11 (βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) ∈ V β†’ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧) = ∩ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)})
130128, 129syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧) = ∩ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)})
131 eqid 2730 . . . . . . . . . . . 12 (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧))
132131rnmpt 5953 . . . . . . . . . . 11 ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)}
133132inteqi 4953 . . . . . . . . . 10 ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = ∩ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)}
134130, 133eqtr4di 2788 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)))
135125, 134eqtrd 2770 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)))
13611ad2antrr 722 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
137 elfpw 9356 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin) ↔ (𝑦 βŠ† (𝐡 βˆ– 𝐹) ∧ 𝑦 ∈ Fin))
138137simplbi 496 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin) β†’ 𝑦 βŠ† (𝐡 βˆ– 𝐹))
139138ad2antlr 723 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 βŠ† (𝐡 βˆ– 𝐹))
140139sselda 3981 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ (𝐡 βˆ– 𝐹))
141140eldifbd 3960 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ Β¬ 𝑧 ∈ 𝐹)
1429ad3antrrr 726 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝐹 ∈ (UFilβ€˜π‘‹))
143139difss2d 4133 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 βŠ† 𝐡)
144143sselda 3981 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ 𝐡)
145 elssuni 4940 . . . . . . . . . . . . . . 15 (𝑧 ∈ 𝐡 β†’ 𝑧 βŠ† βˆͺ 𝐡)
146144, 145syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 βŠ† βˆͺ 𝐡)
14713ad3antrrr 726 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑋 = βˆͺ 𝐡)
148146, 147sseqtrrd 4022 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 βŠ† 𝑋)
149 ufilb 23630 . . . . . . . . . . . . 13 ((𝐹 ∈ (UFilβ€˜π‘‹) ∧ 𝑧 βŠ† 𝑋) β†’ (Β¬ 𝑧 ∈ 𝐹 ↔ (𝑋 βˆ– 𝑧) ∈ 𝐹))
150142, 148, 149syl2anc 582 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ (Β¬ 𝑧 ∈ 𝐹 ↔ (𝑋 βˆ– 𝑧) ∈ 𝐹))
151141, 150mpbid 231 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ (𝑋 βˆ– 𝑧) ∈ 𝐹)
152151fmpttd 7115 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)):π‘¦βŸΆπΉ)
153152frnd 6724 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) βŠ† 𝐹)
154131, 151dmmptd 6694 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = 𝑦)
155 simpr 483 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 β‰  βˆ…)
156154, 155eqnetrd 3006 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
157 dm0rn0 5923 . . . . . . . . . . 11 (dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = βˆ… ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = βˆ…)
158157necon3bii 2991 . . . . . . . . . 10 (dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ… ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
159156, 158sylib 217 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
160 elinel2 4195 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin) β†’ 𝑦 ∈ Fin)
161160ad2antlr 723 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 ∈ Fin)
162 abrexfi 9354 . . . . . . . . . . 11 (𝑦 ∈ Fin β†’ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)} ∈ Fin)
163132, 162eqeltrid 2835 . . . . . . . . . 10 (𝑦 ∈ Fin β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) ∈ Fin)
164161, 163syl 17 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) ∈ Fin)
165 filintn0 23585 . . . . . . . . 9 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ (ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) βŠ† 𝐹 ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ… ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) ∈ Fin)) β†’ ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
166136, 153, 159, 164, 165syl13anc 1370 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
167135, 166eqnetrd 3006 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) β‰  βˆ…)
168 disj3 4452 . . . . . . . 8 ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = βˆ… ↔ 𝑋 = (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)))
169168necon3bii 2991 . . . . . . 7 ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) β‰  βˆ… ↔ 𝑋 β‰  (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)))
170167, 169sylib 217 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑋 β‰  (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)))
171 iundif2 5076 . . . . . . 7 βˆͺ 𝑧 ∈ 𝑦 (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧))
172 dfss4 4257 . . . . . . . . . 10 (𝑧 βŠ† 𝑋 ↔ (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = 𝑧)
173148, 172sylib 217 . . . . . . . . 9 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = 𝑧)
174173iuneq2dv 5020 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ βˆͺ 𝑧 ∈ 𝑦 (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = βˆͺ 𝑧 ∈ 𝑦 𝑧)
175 uniiun 5060 . . . . . . . 8 βˆͺ 𝑦 = βˆͺ 𝑧 ∈ 𝑦 𝑧
176174, 175eqtr4di 2788 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ βˆͺ 𝑧 ∈ 𝑦 (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = βˆͺ 𝑦)
177171, 176eqtr3id 2784 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = βˆͺ 𝑦)
178170, 177neeqtrd 3008 . . . . 5 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑋 β‰  βˆͺ 𝑦)
17911adantr 479 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
180 filtop 23579 . . . . . 6 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝑋 ∈ 𝐹)
181 fileln0 23574 . . . . . 6 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑋 ∈ 𝐹) β†’ 𝑋 β‰  βˆ…)
182179, 180, 181syl2anc2 583 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ 𝑋 β‰  βˆ…)
183121, 178, 182pm2.61ne 3025 . . . 4 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ 𝑋 β‰  βˆͺ 𝑦)
184183neneqd 2943 . . 3 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ Β¬ 𝑋 = βˆͺ 𝑦)
185184nrexdv 3147 . 2 (πœ‘ β†’ Β¬ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)
186117, 185pm2.65i 193 1 Β¬ πœ‘
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  {cab 2707   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  Vcvv 3472   βˆ– cdif 3944   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907  βˆ© cint 4949  βˆͺ ciun 4996  βˆ© ciin 4997   ↦ cmpt 5230  dom cdm 5675  ran crn 5676  β€˜cfv 6542  (class class class)co 7411  Fincfn 8941  ficfi 9407  topGenctg 17387  TopOnctopon 22632  TopBasesctb 22668  Filcfil 23569  UFilcufil 23623  UFLcufl 23624   fLim cflim 23658
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-fin 8945  df-fi 9408  df-topgen 17393  df-fbas 21141  df-top 22616  df-topon 22633  df-bases 22669  df-ntr 22744  df-nei 22822  df-fil 23570  df-ufil 23625  df-flim 23663
This theorem is referenced by:  alexsub  23769
  Copyright terms: Public domain W3C validator