MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alexsublem Structured version   Visualization version   GIF version

Theorem alexsublem 23411
Description: Lemma for alexsub 23412. (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 3921 . . . . . . . . . 10 (π‘₯ ∈ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) ↔ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹)))
2 alexsub.3 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐽 = (topGenβ€˜(fiβ€˜π΅)))
32eleq2d 2820 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑦 ∈ 𝐽 ↔ 𝑦 ∈ (topGenβ€˜(fiβ€˜π΅))))
43anbi1d 631 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦) ↔ (𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦)))
54biimpa 478 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ (𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦))
65adantlr 714 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ (𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦))
7 tg2 22331 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦) β†’ βˆƒπ‘§ ∈ (fiβ€˜π΅)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))
86, 7syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ βˆƒπ‘§ ∈ (fiβ€˜π΅)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))
9 alexsub.5 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐹 ∈ (UFilβ€˜π‘‹))
10 ufilfil 23271 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (UFilβ€˜π‘‹) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
119, 10syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐹 ∈ (Filβ€˜π‘‹))
1211ad3antrrr 729 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
13 alexsub.2 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑋 = βˆͺ 𝐡)
149elfvexd 6882 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑋 ∈ V)
1513, 14eqeltrrd 2835 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ βˆͺ 𝐡 ∈ V)
16 uniexb 7699 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐡 ∈ V ↔ βˆͺ 𝐡 ∈ V)
1715, 16sylibr 233 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝐡 ∈ V)
18 elfi2 9355 . . . . . . . . . . . . . . . . . . . . . 22 (𝐡 ∈ V β†’ (𝑧 ∈ (fiβ€˜π΅) ↔ βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦))
1917, 18syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑧 ∈ (fiβ€˜π΅) ↔ βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦))
2019adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ (𝑧 ∈ (fiβ€˜π΅) ↔ βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦))
2111ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
22 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))
23 intss1 4925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ 𝑦 β†’ ∩ 𝑦 βŠ† 𝑧)
2423adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) β†’ ∩ 𝑦 βŠ† 𝑧)
25 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) β†’ π‘₯ ∈ ∩ 𝑦)
2624, 25sseldd 3946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) β†’ π‘₯ ∈ 𝑧)
2726ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ π‘₯ ∈ 𝑧)
28 eldifsn 4748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ↔ (𝑦 ∈ (𝒫 𝐡 ∩ Fin) ∧ 𝑦 β‰  βˆ…))
2928simplbi 499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) β†’ 𝑦 ∈ (𝒫 𝐡 ∩ Fin))
3029ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 ∈ (𝒫 𝐡 ∩ Fin))
31 elfpw 9301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (𝒫 𝐡 ∩ Fin) ↔ (𝑦 βŠ† 𝐡 ∧ 𝑦 ∈ Fin))
3231simplbi 499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ (𝒫 𝐡 ∩ Fin) β†’ 𝑦 βŠ† 𝐡)
3330, 32syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 βŠ† 𝐡)
3433sselda 3945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ 𝐡)
3534anasss 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ 𝑧 ∈ 𝐡)
3635anim1i 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ∈ 𝐹))
37 eldif 3921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ (𝐡 βˆ– 𝐹) ↔ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ∈ 𝐹))
3836, 37sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ 𝑧 ∈ (𝐡 βˆ– 𝐹))
39 elunii 4871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((π‘₯ ∈ 𝑧 ∧ 𝑧 ∈ (𝐡 βˆ– 𝐹)) β†’ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))
4027, 38, 39syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))
4140ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ (Β¬ 𝑧 ∈ 𝐹 β†’ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹)))
4222, 41mt3d 148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ 𝑧 ∈ 𝐹)
4342expr 458 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ (𝑧 ∈ 𝑦 β†’ 𝑧 ∈ 𝐹))
4443ssrdv 3951 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 βŠ† 𝐹)
45 eldifsni 4751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) β†’ 𝑦 β‰  βˆ…)
4645ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 β‰  βˆ…)
47 elinel2 4157 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (𝒫 𝐡 ∩ Fin) β†’ 𝑦 ∈ Fin)
4830, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 ∈ Fin)
49 elfir 9356 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ (𝑦 βŠ† 𝐹 ∧ 𝑦 β‰  βˆ… ∧ 𝑦 ∈ Fin)) β†’ ∩ 𝑦 ∈ (fiβ€˜πΉ))
5021, 44, 46, 48, 49syl13anc 1373 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ ∩ 𝑦 ∈ (fiβ€˜πΉ))
51 filfi 23226 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (fiβ€˜πΉ) = 𝐹)
5221, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ (fiβ€˜πΉ) = 𝐹)
5350, 52eleqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ ∩ 𝑦 ∈ 𝐹)
5453expr 458 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})) β†’ (π‘₯ ∈ ∩ 𝑦 β†’ ∩ 𝑦 ∈ 𝐹))
55 eleq2 2823 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = ∩ 𝑦 β†’ (π‘₯ ∈ 𝑧 ↔ π‘₯ ∈ ∩ 𝑦))
56 eleq1 2822 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = ∩ 𝑦 β†’ (𝑧 ∈ 𝐹 ↔ ∩ 𝑦 ∈ 𝐹))
5755, 56imbi12d 345 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = ∩ 𝑦 β†’ ((π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹) ↔ (π‘₯ ∈ ∩ 𝑦 β†’ ∩ 𝑦 ∈ 𝐹)))
5854, 57syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})) β†’ (𝑧 = ∩ 𝑦 β†’ (π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹)))
5958rexlimdva 3149 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ (βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦 β†’ (π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹)))
6020, 59sylbid 239 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ (𝑧 ∈ (fiβ€˜π΅) β†’ (π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹)))
6160imp32 420 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ π‘₯ ∈ 𝑧)) β†’ 𝑧 ∈ 𝐹)
6261adantrrr 724 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑧 ∈ 𝐹)
6362adantlr 714 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑧 ∈ 𝐹)
64 elssuni 4899 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ 𝐽 β†’ 𝑦 βŠ† βˆͺ 𝐽)
6564ad2antrl 727 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑦 βŠ† βˆͺ 𝐽)
66 fibas 22343 . . . . . . . . . . . . . . . . . . . . . . 23 (fiβ€˜π΅) ∈ TopBases
67 tgtopon 22337 . . . . . . . . . . . . . . . . . . . . . . 23 ((fiβ€˜π΅) ∈ TopBases β†’ (topGenβ€˜(fiβ€˜π΅)) ∈ (TopOnβ€˜βˆͺ (fiβ€˜π΅)))
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (topGenβ€˜(fiβ€˜π΅)) ∈ (TopOnβ€˜βˆͺ (fiβ€˜π΅))
692, 68eqeltrdi 2842 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜βˆͺ (fiβ€˜π΅)))
70 fiuni 9369 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐡 ∈ V β†’ βˆͺ 𝐡 = βˆͺ (fiβ€˜π΅))
7117, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ βˆͺ 𝐡 = βˆͺ (fiβ€˜π΅))
7213, 71eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝑋 = βˆͺ (fiβ€˜π΅))
7372fveq2d 6847 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (TopOnβ€˜π‘‹) = (TopOnβ€˜βˆͺ (fiβ€˜π΅)))
7469, 73eleqtrrd 2837 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
75 toponuni 22279 . . . . . . . . . . . . . . . . . . . 20 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 = βˆͺ 𝐽)
7776ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑋 = βˆͺ 𝐽)
7865, 77sseqtrrd 3986 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑦 βŠ† 𝑋)
7978adantr 482 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑦 βŠ† 𝑋)
80 simprrr 781 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑧 βŠ† 𝑦)
81 filss 23220 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦 βŠ† 𝑋 ∧ 𝑧 βŠ† 𝑦)) β†’ 𝑦 ∈ 𝐹)
8212, 63, 79, 80, 81syl13anc 1373 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑦 ∈ 𝐹)
838, 82rexlimddv 3155 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑦 ∈ 𝐹)
8483expr 458 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ 𝑦 ∈ 𝐽) β†’ (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))
8584ralrimiva 3140 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))
8685expr 458 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹) β†’ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹)))
8786imdistanda 573 . . . . . . . . . 10 (πœ‘ β†’ ((π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹)) β†’ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
881, 87biimtrid 241 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) β†’ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
89 flimopn 23342 . . . . . . . . . 10 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐹 ∈ (Filβ€˜π‘‹)) β†’ (π‘₯ ∈ (𝐽 fLim 𝐹) ↔ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
9074, 11, 89syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (𝐽 fLim 𝐹) ↔ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
9188, 90sylibrd 259 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) β†’ π‘₯ ∈ (𝐽 fLim 𝐹)))
9291ssrdv 3951 . . . . . . 7 (πœ‘ β†’ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) βŠ† (𝐽 fLim 𝐹))
93 alexsub.6 . . . . . . 7 (πœ‘ β†’ (𝐽 fLim 𝐹) = βˆ…)
94 sseq0 4360 . . . . . . 7 (((𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) βŠ† (𝐽 fLim 𝐹) ∧ (𝐽 fLim 𝐹) = βˆ…) β†’ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) = βˆ…)
9592, 93, 94syl2anc 585 . . . . . 6 (πœ‘ β†’ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) = βˆ…)
96 ssdif0 4324 . . . . . 6 (𝑋 βŠ† βˆͺ (𝐡 βˆ– 𝐹) ↔ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) = βˆ…)
9795, 96sylibr 233 . . . . 5 (πœ‘ β†’ 𝑋 βŠ† βˆͺ (𝐡 βˆ– 𝐹))
98 difss 4092 . . . . . . 7 (𝐡 βˆ– 𝐹) βŠ† 𝐡
9998unissi 4875 . . . . . 6 βˆͺ (𝐡 βˆ– 𝐹) βŠ† βˆͺ 𝐡
10099, 13sseqtrrid 3998 . . . . 5 (πœ‘ β†’ βˆͺ (𝐡 βˆ– 𝐹) βŠ† 𝑋)
10197, 100eqssd 3962 . . . 4 (πœ‘ β†’ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))
102101, 98jctil 521 . . 3 (πœ‘ β†’ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹)))
10317difexd 5287 . . . . 5 (πœ‘ β†’ (𝐡 βˆ– 𝐹) ∈ V)
104103adantr 482 . . . 4 ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ (𝐡 βˆ– 𝐹) ∈ V)
105 sseq1 3970 . . . . . . . 8 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (π‘₯ βŠ† 𝐡 ↔ (𝐡 βˆ– 𝐹) βŠ† 𝐡))
106 unieq 4877 . . . . . . . . 9 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ βˆͺ π‘₯ = βˆͺ (𝐡 βˆ– 𝐹))
107106eqeq2d 2744 . . . . . . . 8 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (𝑋 = βˆͺ π‘₯ ↔ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹)))
108105, 107anbi12d 632 . . . . . . 7 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ ((π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯) ↔ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))))
109108anbi2d 630 . . . . . 6 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ ((πœ‘ ∧ (π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯)) ↔ (πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹)))))
110 pweq 4575 . . . . . . . 8 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ 𝒫 π‘₯ = 𝒫 (𝐡 βˆ– 𝐹))
111110ineq1d 4172 . . . . . . 7 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (𝒫 π‘₯ ∩ Fin) = (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin))
112111rexeqdv 3313 . . . . . 6 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑋 = βˆͺ 𝑦 ↔ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦))
113109, 112imbi12d 345 . . . . 5 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (((πœ‘ ∧ (π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯)) β†’ βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑋 = βˆͺ 𝑦) ↔ ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)))
114 alexsub.4 . . . . 5 ((πœ‘ ∧ (π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯)) β†’ βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑋 = βˆͺ 𝑦)
115113, 114vtoclg 3524 . . . 4 ((𝐡 βˆ– 𝐹) ∈ V β†’ ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦))
116104, 115mpcom 38 . . 3 ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)
117102, 116mpdan 686 . 2 (πœ‘ β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)
118 unieq 4877 . . . . . . 7 (𝑦 = βˆ… β†’ βˆͺ 𝑦 = βˆͺ βˆ…)
119 uni0 4897 . . . . . . 7 βˆͺ βˆ… = βˆ…
120118, 119eqtrdi 2789 . . . . . 6 (𝑦 = βˆ… β†’ βˆͺ 𝑦 = βˆ…)
121120neeq2d 3001 . . . . 5 (𝑦 = βˆ… β†’ (𝑋 β‰  βˆͺ 𝑦 ↔ 𝑋 β‰  βˆ…))
122 difssd 4093 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ (𝑋 βˆ– 𝑧) βŠ† 𝑋)
123122ralrimivw 3144 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) βŠ† 𝑋)
124 riinn0 5044 . . . . . . . . . 10 ((βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) βŠ† 𝑋 ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧))
125123, 124sylan 581 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧))
12614ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑋 ∈ V)
127126difexd 5287 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 βˆ– 𝑧) ∈ V)
128127ralrimivw 3144 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) ∈ V)
129 dfiin2g 4993 . . . . . . . . . . 11 (βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) ∈ V β†’ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧) = ∩ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)})
130128, 129syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧) = ∩ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)})
131 eqid 2733 . . . . . . . . . . . 12 (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧))
132131rnmpt 5911 . . . . . . . . . . 11 ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)}
133132inteqi 4912 . . . . . . . . . 10 ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = ∩ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)}
134130, 133eqtr4di 2791 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)))
135125, 134eqtrd 2773 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)))
13611ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
137 elfpw 9301 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin) ↔ (𝑦 βŠ† (𝐡 βˆ– 𝐹) ∧ 𝑦 ∈ Fin))
138137simplbi 499 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin) β†’ 𝑦 βŠ† (𝐡 βˆ– 𝐹))
139138ad2antlr 726 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 βŠ† (𝐡 βˆ– 𝐹))
140139sselda 3945 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ (𝐡 βˆ– 𝐹))
141140eldifbd 3924 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ Β¬ 𝑧 ∈ 𝐹)
1429ad3antrrr 729 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝐹 ∈ (UFilβ€˜π‘‹))
143139difss2d 4095 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 βŠ† 𝐡)
144143sselda 3945 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ 𝐡)
145 elssuni 4899 . . . . . . . . . . . . . . 15 (𝑧 ∈ 𝐡 β†’ 𝑧 βŠ† βˆͺ 𝐡)
146144, 145syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 βŠ† βˆͺ 𝐡)
14713ad3antrrr 729 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑋 = βˆͺ 𝐡)
148146, 147sseqtrrd 3986 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 βŠ† 𝑋)
149 ufilb 23273 . . . . . . . . . . . . 13 ((𝐹 ∈ (UFilβ€˜π‘‹) ∧ 𝑧 βŠ† 𝑋) β†’ (Β¬ 𝑧 ∈ 𝐹 ↔ (𝑋 βˆ– 𝑧) ∈ 𝐹))
150142, 148, 149syl2anc 585 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ (Β¬ 𝑧 ∈ 𝐹 ↔ (𝑋 βˆ– 𝑧) ∈ 𝐹))
151141, 150mpbid 231 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ (𝑋 βˆ– 𝑧) ∈ 𝐹)
152151fmpttd 7064 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)):π‘¦βŸΆπΉ)
153152frnd 6677 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) βŠ† 𝐹)
154131, 151dmmptd 6647 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = 𝑦)
155 simpr 486 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 β‰  βˆ…)
156154, 155eqnetrd 3008 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
157 dm0rn0 5881 . . . . . . . . . . 11 (dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = βˆ… ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = βˆ…)
158157necon3bii 2993 . . . . . . . . . 10 (dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ… ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
159156, 158sylib 217 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
160 elinel2 4157 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin) β†’ 𝑦 ∈ Fin)
161160ad2antlr 726 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 ∈ Fin)
162 abrexfi 9299 . . . . . . . . . . 11 (𝑦 ∈ Fin β†’ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)} ∈ Fin)
163132, 162eqeltrid 2838 . . . . . . . . . 10 (𝑦 ∈ Fin β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) ∈ Fin)
164161, 163syl 17 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) ∈ Fin)
165 filintn0 23228 . . . . . . . . 9 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ (ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) βŠ† 𝐹 ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ… ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) ∈ Fin)) β†’ ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
166136, 153, 159, 164, 165syl13anc 1373 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
167135, 166eqnetrd 3008 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) β‰  βˆ…)
168 disj3 4414 . . . . . . . 8 ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = βˆ… ↔ 𝑋 = (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)))
169168necon3bii 2993 . . . . . . 7 ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) β‰  βˆ… ↔ 𝑋 β‰  (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)))
170167, 169sylib 217 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑋 β‰  (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)))
171 iundif2 5035 . . . . . . 7 βˆͺ 𝑧 ∈ 𝑦 (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧))
172 dfss4 4219 . . . . . . . . . 10 (𝑧 βŠ† 𝑋 ↔ (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = 𝑧)
173148, 172sylib 217 . . . . . . . . 9 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = 𝑧)
174173iuneq2dv 4979 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ βˆͺ 𝑧 ∈ 𝑦 (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = βˆͺ 𝑧 ∈ 𝑦 𝑧)
175 uniiun 5019 . . . . . . . 8 βˆͺ 𝑦 = βˆͺ 𝑧 ∈ 𝑦 𝑧
176174, 175eqtr4di 2791 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ βˆͺ 𝑧 ∈ 𝑦 (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = βˆͺ 𝑦)
177171, 176eqtr3id 2787 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = βˆͺ 𝑦)
178170, 177neeqtrd 3010 . . . . 5 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑋 β‰  βˆͺ 𝑦)
17911adantr 482 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
180 filtop 23222 . . . . . 6 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝑋 ∈ 𝐹)
181 fileln0 23217 . . . . . 6 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑋 ∈ 𝐹) β†’ 𝑋 β‰  βˆ…)
182179, 180, 181syl2anc2 586 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ 𝑋 β‰  βˆ…)
183121, 178, 182pm2.61ne 3027 . . . 4 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ 𝑋 β‰  βˆͺ 𝑦)
184183neneqd 2945 . . 3 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ Β¬ 𝑋 = βˆͺ 𝑦)
185184nrexdv 3143 . 2 (πœ‘ β†’ Β¬ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)
186117, 185pm2.65i 193 1 Β¬ πœ‘
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2710   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3444   βˆ– cdif 3908   ∩ cin 3910   βŠ† wss 3911  βˆ…c0 4283  π’« cpw 4561  {csn 4587  βˆͺ cuni 4866  βˆ© cint 4908  βˆͺ ciun 4955  βˆ© ciin 4956   ↦ cmpt 5189  dom cdm 5634  ran crn 5635  β€˜cfv 6497  (class class class)co 7358  Fincfn 8886  ficfi 9351  topGenctg 17324  TopOnctopon 22275  TopBasesctb 22311  Filcfil 23212  UFilcufil 23266  UFLcufl 23267   fLim cflim 23301
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-1o 8413  df-er 8651  df-en 8887  df-dom 8888  df-fin 8890  df-fi 9352  df-topgen 17330  df-fbas 20809  df-top 22259  df-topon 22276  df-bases 22312  df-ntr 22387  df-nei 22465  df-fil 23213  df-ufil 23268  df-flim 23306
This theorem is referenced by:  alexsub  23412
  Copyright terms: Public domain W3C validator