MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alexsublem Structured version   Visualization version   GIF version
Theorem alexsublem 23539
Description: Lemma for alexsub 23540. (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 2819 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑦 ∈ 𝐽 ↔ 𝑦 ∈ (topGenβ€˜(fiβ€˜π΅))))
43anbi1d 630 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦) ↔ (𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦)))
54biimpa 477 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ (𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦))
65adantlr 713 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ (𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦))
7 tg2 22459 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (topGenβ€˜(fiβ€˜π΅)) ∧ π‘₯ ∈ 𝑦) β†’ βˆƒπ‘§ ∈ (fiβ€˜π΅)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))
86, 7syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ βˆƒπ‘§ ∈ (fiβ€˜π΅)(π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))
9 alexsub.5 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐹 ∈ (UFilβ€˜π‘‹))
10 ufilfil 23399 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (UFilβ€˜π‘‹) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
119, 10syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐹 ∈ (Filβ€˜π‘‹))
1211ad3antrrr 728 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
13 alexsub.2 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑋 = βˆͺ 𝐡)
149elfvexd 6927 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑋 ∈ V)
1513, 14eqeltrrd 2834 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ βˆͺ 𝐡 ∈ V)
16 uniexb 7747 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐡 ∈ V ↔ βˆͺ 𝐡 ∈ V)
1715, 16sylibr 233 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝐡 ∈ V)
18 elfi2 9405 . . . . . . . . . . . . . . . . . . . . . 22 (𝐡 ∈ V β†’ (𝑧 ∈ (fiβ€˜π΅) ↔ βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦))
1917, 18syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑧 ∈ (fiβ€˜π΅) ↔ βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦))
2019adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ (𝑧 ∈ (fiβ€˜π΅) ↔ βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦))
2111ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
22 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))
23 intss1 4966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧 ∈ 𝑦 β†’ ∩ 𝑦 βŠ† 𝑧)
2423adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) β†’ ∩ 𝑦 βŠ† 𝑧)
25 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) β†’ π‘₯ ∈ ∩ 𝑦)
2624, 25sseldd 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) β†’ π‘₯ ∈ 𝑧)
2726ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ π‘₯ ∈ 𝑧)
28 eldifsn 4789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ↔ (𝑦 ∈ (𝒫 𝐡 ∩ Fin) ∧ 𝑦 β‰  βˆ…))
2928simplbi 498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) β†’ 𝑦 ∈ (𝒫 𝐡 ∩ Fin))
3029ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 ∈ (𝒫 𝐡 ∩ Fin))
31 elfpw 9350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (𝒫 𝐡 ∩ Fin) ↔ (𝑦 βŠ† 𝐡 ∧ 𝑦 ∈ Fin))
3231simplbi 498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ (𝒫 𝐡 ∩ Fin) β†’ 𝑦 βŠ† 𝐡)
3330, 32syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 βŠ† 𝐡)
3433sselda 3981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ 𝐡)
3534anasss 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ 𝑧 ∈ 𝐡)
3635anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ∈ 𝐹))
37 eldif 3957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ (𝐡 βˆ– 𝐹) ↔ (𝑧 ∈ 𝐡 ∧ Β¬ 𝑧 ∈ 𝐹))
3836, 37sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ 𝑧 ∈ (𝐡 βˆ– 𝐹))
39 elunii 4912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((π‘₯ ∈ 𝑧 ∧ 𝑧 ∈ (𝐡 βˆ– 𝐹)) β†’ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))
4027, 38, 39syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ Β¬ 𝑧 ∈ 𝐹) β†’ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))
4140ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ (Β¬ 𝑧 ∈ 𝐹 β†’ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹)))
4222, 41mt3d 148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) β†’ 𝑧 ∈ 𝐹)
4342expr 457 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ (𝑧 ∈ 𝑦 β†’ 𝑧 ∈ 𝐹))
4443ssrdv 3987 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 βŠ† 𝐹)
45 eldifsni 4792 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) β†’ 𝑦 β‰  βˆ…)
4645ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 β‰  βˆ…)
47 elinel2 4195 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (𝒫 𝐡 ∩ Fin) β†’ 𝑦 ∈ Fin)
4830, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ 𝑦 ∈ Fin)
49 elfir 9406 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ (𝑦 βŠ† 𝐹 ∧ 𝑦 β‰  βˆ… ∧ 𝑦 ∈ Fin)) β†’ ∩ 𝑦 ∈ (fiβ€˜πΉ))
5021, 44, 46, 48, 49syl13anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ ∩ 𝑦 ∈ (fiβ€˜πΉ))
51 filfi 23354 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 ∈ (Filβ€˜π‘‹) β†’ (fiβ€˜πΉ) = 𝐹)
5221, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ (fiβ€˜πΉ) = 𝐹)
5350, 52eleqtrd 2835 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…}) ∧ π‘₯ ∈ ∩ 𝑦)) β†’ ∩ 𝑦 ∈ 𝐹)
5453expr 457 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})) β†’ (π‘₯ ∈ ∩ 𝑦 β†’ ∩ 𝑦 ∈ 𝐹))
55 eleq2 2822 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = ∩ 𝑦 β†’ (π‘₯ ∈ 𝑧 ↔ π‘₯ ∈ ∩ 𝑦))
56 eleq1 2821 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = ∩ 𝑦 β†’ (𝑧 ∈ 𝐹 ↔ ∩ 𝑦 ∈ 𝐹))
5755, 56imbi12d 344 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = ∩ 𝑦 β†’ ((π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹) ↔ (π‘₯ ∈ ∩ 𝑦 β†’ ∩ 𝑦 ∈ 𝐹)))
5854, 57syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})) β†’ (𝑧 = ∩ 𝑦 β†’ (π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹)))
5958rexlimdva 3155 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ (βˆƒπ‘¦ ∈ ((𝒫 𝐡 ∩ Fin) βˆ– {βˆ…})𝑧 = ∩ 𝑦 β†’ (π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹)))
6020, 59sylbid 239 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ (𝑧 ∈ (fiβ€˜π΅) β†’ (π‘₯ ∈ 𝑧 β†’ 𝑧 ∈ 𝐹)))
6160imp32 419 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ π‘₯ ∈ 𝑧)) β†’ 𝑧 ∈ 𝐹)
6261adantrrr 723 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑧 ∈ 𝐹)
6362adantlr 713 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑧 ∈ 𝐹)
64 elssuni 4940 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ 𝐽 β†’ 𝑦 βŠ† βˆͺ 𝐽)
6564ad2antrl 726 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑦 βŠ† βˆͺ 𝐽)
66 fibas 22471 . . . . . . . . . . . . . . . . . . . . . . 23 (fiβ€˜π΅) ∈ TopBases
67 tgtopon 22465 . . . . . . . . . . . . . . . . . . . . . . 23 ((fiβ€˜π΅) ∈ TopBases β†’ (topGenβ€˜(fiβ€˜π΅)) ∈ (TopOnβ€˜βˆͺ (fiβ€˜π΅)))
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (topGenβ€˜(fiβ€˜π΅)) ∈ (TopOnβ€˜βˆͺ (fiβ€˜π΅))
692, 68eqeltrdi 2841 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜βˆͺ (fiβ€˜π΅)))
70 fiuni 9419 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐡 ∈ V β†’ βˆͺ 𝐡 = βˆͺ (fiβ€˜π΅))
7117, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ βˆͺ 𝐡 = βˆͺ (fiβ€˜π΅))
7213, 71eqtrd 2772 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝑋 = βˆͺ (fiβ€˜π΅))
7372fveq2d 6892 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (TopOnβ€˜π‘‹) = (TopOnβ€˜βˆͺ (fiβ€˜π΅)))
7469, 73eleqtrrd 2836 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
75 toponuni 22407 . . . . . . . . . . . . . . . . . . . 20 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 = βˆͺ 𝐽)
7776ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑋 = βˆͺ 𝐽)
7865, 77sseqtrrd 4022 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑦 βŠ† 𝑋)
7978adantr 481 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑦 βŠ† 𝑋)
80 simprrr 780 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑧 βŠ† 𝑦)
81 filss 23348 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦 βŠ† 𝑋 ∧ 𝑧 βŠ† 𝑦)) β†’ 𝑦 ∈ 𝐹)
8212, 63, 79, 80, 81syl13anc 1372 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) ∧ (𝑧 ∈ (fiβ€˜π΅) ∧ (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑦))) β†’ 𝑦 ∈ 𝐹)
838, 82rexlimddv 3161 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ π‘₯ ∈ 𝑦)) β†’ 𝑦 ∈ 𝐹)
8483expr 457 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) ∧ 𝑦 ∈ 𝐽) β†’ (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))
8584ralrimiva 3146 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))
8685expr 457 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹) β†’ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹)))
8786imdistanda 572 . . . . . . . . . 10 (πœ‘ β†’ ((π‘₯ ∈ 𝑋 ∧ Β¬ π‘₯ ∈ βˆͺ (𝐡 βˆ– 𝐹)) β†’ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
881, 87biimtrid 241 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (𝑋 βˆ– βˆͺ (𝐡 βˆ– 𝐹)) β†’ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
89 flimopn 23470 . . . . . . . . . 10 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐹 ∈ (Filβ€˜π‘‹)) β†’ (π‘₯ ∈ (𝐽 fLim 𝐹) ↔ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘¦ ∈ 𝐽 (π‘₯ ∈ 𝑦 β†’ 𝑦 ∈ 𝐹))))
9074, 11, 89syl2anc 584 . . . . . . . . 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 584 . . . . . 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 520 . . 3 (πœ‘ β†’ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹)))
10317difexd 5328 . . . . 5 (πœ‘ β†’ (𝐡 βˆ– 𝐹) ∈ V)
104103adantr 481 . . . 4 ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ (𝐡 βˆ– 𝐹) ∈ V)
105 sseq1 4006 . . . . . . . 8 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (π‘₯ βŠ† 𝐡 ↔ (𝐡 βˆ– 𝐹) βŠ† 𝐡))
106 unieq 4918 . . . . . . . . 9 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ βˆͺ π‘₯ = βˆͺ (𝐡 βˆ– 𝐹))
107106eqeq2d 2743 . . . . . . . 8 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (𝑋 = βˆͺ π‘₯ ↔ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹)))
108105, 107anbi12d 631 . . . . . . 7 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ ((π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯) ↔ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))))
109108anbi2d 629 . . . . . 6 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ ((πœ‘ ∧ (π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯)) ↔ (πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹)))))
110 pweq 4615 . . . . . . . 8 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ 𝒫 π‘₯ = 𝒫 (𝐡 βˆ– 𝐹))
111110ineq1d 4210 . . . . . . 7 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (𝒫 π‘₯ ∩ Fin) = (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin))
112111rexeqdv 3326 . . . . . 6 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑋 = βˆͺ 𝑦 ↔ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦))
113109, 112imbi12d 344 . . . . 5 (π‘₯ = (𝐡 βˆ– 𝐹) β†’ (((πœ‘ ∧ (π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯)) β†’ βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑋 = βˆͺ 𝑦) ↔ ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)))
114 alexsub.4 . . . . 5 ((πœ‘ ∧ (π‘₯ βŠ† 𝐡 ∧ 𝑋 = βˆͺ π‘₯)) β†’ βˆƒπ‘¦ ∈ (𝒫 π‘₯ ∩ Fin)𝑋 = βˆͺ 𝑦)
115113, 114vtoclg 3556 . . . 4 ((𝐡 βˆ– 𝐹) ∈ V β†’ ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦))
116104, 115mpcom 38 . . 3 ((πœ‘ ∧ ((𝐡 βˆ– 𝐹) βŠ† 𝐡 ∧ 𝑋 = βˆͺ (𝐡 βˆ– 𝐹))) β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)
117102, 116mpdan 685 . 2 (πœ‘ β†’ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)
118 unieq 4918 . . . . . . 7 (𝑦 = βˆ… β†’ βˆͺ 𝑦 = βˆͺ βˆ…)
119 uni0 4938 . . . . . . 7 βˆͺ βˆ… = βˆ…
120118, 119eqtrdi 2788 . . . . . 6 (𝑦 = βˆ… β†’ βˆͺ 𝑦 = βˆ…)
121120neeq2d 3001 . . . . 5 (𝑦 = βˆ… β†’ (𝑋 β‰  βˆͺ 𝑦 ↔ 𝑋 β‰  βˆ…))
122 difssd 4131 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ (𝑋 βˆ– 𝑧) βŠ† 𝑋)
123122ralrimivw 3150 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) βŠ† 𝑋)
124 riinn0 5085 . . . . . . . . . 10 ((βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) βŠ† 𝑋 ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧))
125123, 124sylan 580 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧))
12614ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑋 ∈ V)
127126difexd 5328 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 βˆ– 𝑧) ∈ V)
128127ralrimivw 3150 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) ∈ V)
129 dfiin2g 5034 . . . . . . . . . . 11 (βˆ€π‘§ ∈ 𝑦 (𝑋 βˆ– 𝑧) ∈ V β†’ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧) = ∩ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)})
130128, 129syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧) = ∩ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)})
131 eqid 2732 . . . . . . . . . . . 12 (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧))
132131rnmpt 5952 . . . . . . . . . . 11 ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)}
133132inteqi 4953 . . . . . . . . . 10 ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = ∩ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)}
134130, 133eqtr4di 2790 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)))
135125, 134eqtrd 2772 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)))
13611ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
137 elfpw 9350 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin) ↔ (𝑦 βŠ† (𝐡 βˆ– 𝐹) ∧ 𝑦 ∈ Fin))
138137simplbi 498 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin) β†’ 𝑦 βŠ† (𝐡 βˆ– 𝐹))
139138ad2antlr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 βŠ† (𝐡 βˆ– 𝐹))
140139sselda 3981 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ (𝐡 βˆ– 𝐹))
141140eldifbd 3960 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ Β¬ 𝑧 ∈ 𝐹)
1429ad3antrrr 728 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝐹 ∈ (UFilβ€˜π‘‹))
143139difss2d 4133 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 βŠ† 𝐡)
144143sselda 3981 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 ∈ 𝐡)
145 elssuni 4940 . . . . . . . . . . . . . . 15 (𝑧 ∈ 𝐡 β†’ 𝑧 βŠ† βˆͺ 𝐡)
146144, 145syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 βŠ† βˆͺ 𝐡)
14713ad3antrrr 728 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑋 = βˆͺ 𝐡)
148146, 147sseqtrrd 4022 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ 𝑧 βŠ† 𝑋)
149 ufilb 23401 . . . . . . . . . . . . 13 ((𝐹 ∈ (UFilβ€˜π‘‹) ∧ 𝑧 βŠ† 𝑋) β†’ (Β¬ 𝑧 ∈ 𝐹 ↔ (𝑋 βˆ– 𝑧) ∈ 𝐹))
150142, 148, 149syl2anc 584 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ (Β¬ 𝑧 ∈ 𝐹 ↔ (𝑋 βˆ– 𝑧) ∈ 𝐹))
151141, 150mpbid 231 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) ∧ 𝑧 ∈ 𝑦) β†’ (𝑋 βˆ– 𝑧) ∈ 𝐹)
152151fmpttd 7111 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)):π‘¦βŸΆπΉ)
153152frnd 6722 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) βŠ† 𝐹)
154131, 151dmmptd 6692 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = 𝑦)
155 simpr 485 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 β‰  βˆ…)
156154, 155eqnetrd 3008 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
157 dm0rn0 5922 . . . . . . . . . . 11 (dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = βˆ… ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) = βˆ…)
158157necon3bii 2993 . . . . . . . . . 10 (dom (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ… ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
159156, 158sylib 217 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
160 elinel2 4195 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin) β†’ 𝑦 ∈ Fin)
161160ad2antlr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑦 ∈ Fin)
162 abrexfi 9348 . . . . . . . . . . 11 (𝑦 ∈ Fin β†’ {π‘₯ ∣ βˆƒπ‘§ ∈ 𝑦 π‘₯ = (𝑋 βˆ– 𝑧)} ∈ Fin)
163132, 162eqeltrid 2837 . . . . . . . . . 10 (𝑦 ∈ Fin β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) ∈ Fin)
164161, 163syl 17 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) ∈ Fin)
165 filintn0 23356 . . . . . . . . 9 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ (ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) βŠ† 𝐹 ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ… ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) ∈ Fin)) β†’ ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
166136, 153, 159, 164, 165syl13anc 1372 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 βˆ– 𝑧)) β‰  βˆ…)
167135, 166eqnetrd 3008 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) β‰  βˆ…)
168 disj3 4452 . . . . . . . 8 ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = βˆ… ↔ 𝑋 = (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)))
169168necon3bii 2993 . . . . . . 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 2790 . . . . . . 7 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ βˆͺ 𝑧 ∈ 𝑦 (𝑋 βˆ– (𝑋 βˆ– 𝑧)) = βˆͺ 𝑦)
177171, 176eqtr3id 2786 . . . . . 6 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ (𝑋 βˆ– ∩ 𝑧 ∈ 𝑦 (𝑋 βˆ– 𝑧)) = βˆͺ 𝑦)
178170, 177neeqtrd 3010 . . . . 5 (((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) ∧ 𝑦 β‰  βˆ…) β†’ 𝑋 β‰  βˆͺ 𝑦)
17911adantr 481 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ 𝐹 ∈ (Filβ€˜π‘‹))
180 filtop 23350 . . . . . 6 (𝐹 ∈ (Filβ€˜π‘‹) β†’ 𝑋 ∈ 𝐹)
181 fileln0 23345 . . . . . 6 ((𝐹 ∈ (Filβ€˜π‘‹) ∧ 𝑋 ∈ 𝐹) β†’ 𝑋 β‰  βˆ…)
182179, 180, 181syl2anc2 585 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ 𝑋 β‰  βˆ…)
183121, 178, 182pm2.61ne 3027 . . . 4 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ 𝑋 β‰  βˆͺ 𝑦)
184183neneqd 2945 . . 3 ((πœ‘ ∧ 𝑦 ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)) β†’ Β¬ 𝑋 = βˆͺ 𝑦)
185184nrexdv 3149 . 2 (πœ‘ β†’ Β¬ βˆƒπ‘¦ ∈ (𝒫 (𝐡 βˆ– 𝐹) ∩ Fin)𝑋 = βˆͺ 𝑦)
186117, 185pm2.65i 193 1 Β¬ πœ‘
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {cab 2709   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474   βˆ– 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 6540  (class class class)co 7405  Fincfn 8935  ficfi 9401  topGenctg 17379  TopOnctopon 22403  TopBasesctb 22439  Filcfil 23340  UFilcufil 23394  UFLcufl 23395   fLim cflim 23429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  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 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-1o 8462  df-er 8699  df-en 8936  df-dom 8937  df-fin 8939  df-fi 9402  df-topgen 17385  df-fbas 20933  df-top 22387  df-topon 22404  df-bases 22440  df-ntr 22515  df-nei 22593  df-fil 23341  df-ufil 23396  df-flim 23434
This theorem is referenced by:  alexsub  23540
  Copyright terms: Public domain W3C validator