Metamath Proof Explorer

Theorem alexsublem

Description: Lemma for alexsub . (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses alexsub.1 ⊢ ( 𝜑 → 𝑋 ∈ UFL )
alexsub.2 ⊢ ( 𝜑 → 𝑋 = ∪ 𝐵 )
alexsub.3 ⊢ ( 𝜑 → 𝐽 = ( topGen ‘ ( fi ‘ 𝐵 ) ) )
alexsub.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 )
alexsub.5 ⊢ ( 𝜑 → 𝐹 ∈ ( UFil ‘ 𝑋 ) )
alexsub.6 ⊢ ( 𝜑 → ( 𝐽 fLim 𝐹 ) = ∅ )
Assertion alexsublem ¬ 𝜑

Proof

Step Hyp Ref Expression
1 alexsub.1 ⊢ ( 𝜑 → 𝑋 ∈ UFL )
2 alexsub.2 ⊢ ( 𝜑 → 𝑋 = ∪ 𝐵 )
3 alexsub.3 ⊢ ( 𝜑 → 𝐽 = ( topGen ‘ ( fi ‘ 𝐵 ) ) )
4 alexsub.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 )
5 alexsub.5 ⊢ ( 𝜑 → 𝐹 ∈ ( UFil ‘ 𝑋 ) )
6 alexsub.6 ⊢ ( 𝜑 → ( 𝐽 fLim 𝐹 ) = ∅ )
7 eldif ⊢ ( 𝑥 ∈ ( 𝑋 ∖ ∪ ( 𝐵 ∖ 𝐹 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) )
8 3 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↔ 𝑦 ∈ ( topGen ‘ ( fi ‘ 𝐵 ) ) ) )
9 8 anbi1d ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ↔ ( 𝑦 ∈ ( topGen ‘ ( fi ‘ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) ) )
10 9 biimpa ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → ( 𝑦 ∈ ( topGen ‘ ( fi ‘ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) )
11 10 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → ( 𝑦 ∈ ( topGen ‘ ( fi ‘ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) )
12 tg2 ⊢ ( ( 𝑦 ∈ ( topGen ‘ ( fi ‘ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → ∃ 𝑧 ∈ ( fi ‘ 𝐵 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) )
13 11 12 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → ∃ 𝑧 ∈ ( fi ‘ 𝐵 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) )
14 ufilfil ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
15 5 14 syl ⊢ ( 𝜑 → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
16 15 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) ∧ ( 𝑧 ∈ ( fi ‘ 𝐵 ) ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
17 5 elfvexd ⊢ ( 𝜑 → 𝑋 ∈ V )
18 2 17 eqeltrrd ⊢ ( 𝜑 → ∪ 𝐵 ∈ V )
19 uniexb ⊢ ( 𝐵 ∈ V ↔ ∪ 𝐵 ∈ V )
20 18 19 sylibr ⊢ ( 𝜑 → 𝐵 ∈ V )
21 elfi2 ⊢ ( 𝐵 ∈ V → ( 𝑧 ∈ ( fi ‘ 𝐵 ) ↔ ∃ 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) 𝑧 = ∩ 𝑦 ) )
22 20 21 syl ⊢ ( 𝜑 → ( 𝑧 ∈ ( fi ‘ 𝐵 ) ↔ ∃ 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) 𝑧 = ∩ 𝑦 ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) → ( 𝑧 ∈ ( fi ‘ 𝐵 ) ↔ ∃ 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) 𝑧 = ∩ 𝑦 ) )
24 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
25 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ∧ 𝑧 ∈ 𝑦 ) ) → ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) )
26 intss1 ⊢ ( 𝑧 ∈ 𝑦 → ∩ 𝑦 ⊆ 𝑧 )
27 26 adantl ⊢ ( ( ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ∧ 𝑧 ∈ 𝑦 ) → ∩ 𝑦 ⊆ 𝑧 )
28 simplr ⊢ ( ( ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ∧ 𝑧 ∈ 𝑦 ) → 𝑥 ∈ ∩ 𝑦 )
29 27 28 sseldd ⊢ ( ( ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ∧ 𝑧 ∈ 𝑦 ) → 𝑥 ∈ 𝑧 )
30 29 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ∧ 𝑧 ∈ 𝑦 ) ) ∧ ¬ 𝑧 ∈ 𝐹 ) → 𝑥 ∈ 𝑧 )
31 eldifsn ⊢ ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ↔ ( 𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑦 ≠ ∅ ) )
32 31 simplbi ⊢ ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) → 𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) )
33 32 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ) → 𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) )
34 elfpw ⊢ ( 𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) ↔ ( 𝑦 ⊆ 𝐵 ∧ 𝑦 ∈ Fin ) )
35 34 simplbi ⊢ ( 𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑦 ⊆ 𝐵 )
36 33 35 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ) → 𝑦 ⊆ 𝐵 )
37 36 sselda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ 𝐵 )
38 37 anasss ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ∧ 𝑧 ∈ 𝑦 ) ) → 𝑧 ∈ 𝐵 )
39 38 anim1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ∧ 𝑧 ∈ 𝑦 ) ) ∧ ¬ 𝑧 ∈ 𝐹 ) → ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ∈ 𝐹 ) )
40 eldif ⊢ ( 𝑧 ∈ ( 𝐵 ∖ 𝐹 ) ↔ ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ∈ 𝐹 ) )
41 39 40 sylibr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ∧ 𝑧 ∈ 𝑦 ) ) ∧ ¬ 𝑧 ∈ 𝐹 ) → 𝑧 ∈ ( 𝐵 ∖ 𝐹 ) )
42 elunii ⊢ ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ∈ ( 𝐵 ∖ 𝐹 ) ) → 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) )
43 30 41 42 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ∧ 𝑧 ∈ 𝑦 ) ) ∧ ¬ 𝑧 ∈ 𝐹 ) → 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) )
44 43 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ∧ 𝑧 ∈ 𝑦 ) ) → ( ¬ 𝑧 ∈ 𝐹 → 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) )
45 25 44 mt3d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ∧ 𝑧 ∈ 𝑦 ) ) → 𝑧 ∈ 𝐹 )
46 45 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ) → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐹 ) )
47 46 ssrdv ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ) → 𝑦 ⊆ 𝐹 )
48 eldifsni ⊢ ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) → 𝑦 ≠ ∅ )
49 48 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ) → 𝑦 ≠ ∅ )
50 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑦 ∈ Fin )
51 33 50 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ) → 𝑦 ∈ Fin )
52 elfir ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑦 ⊆ 𝐹 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin ) ) → ∩ 𝑦 ∈ ( fi ‘ 𝐹 ) )
53 24 47 49 51 52 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ) → ∩ 𝑦 ∈ ( fi ‘ 𝐹 ) )
54 filfi ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( fi ‘ 𝐹 ) = 𝐹 )
55 24 54 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ) → ( fi ‘ 𝐹 ) = 𝐹 )
56 53 55 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ∧ 𝑥 ∈ ∩ 𝑦 ) ) → ∩ 𝑦 ∈ 𝐹 )
57 56 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑥 ∈ ∩ 𝑦 → ∩ 𝑦 ∈ 𝐹 ) )
58 eleq2 ⊢ ( 𝑧 = ∩ 𝑦 → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ∩ 𝑦 ) )
59 eleq1 ⊢ ( 𝑧 = ∩ 𝑦 → ( 𝑧 ∈ 𝐹 ↔ ∩ 𝑦 ∈ 𝐹 ) )
60 58 59 imbi12d ⊢ ( 𝑧 = ∩ 𝑦 → ( ( 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹 ) ↔ ( 𝑥 ∈ ∩ 𝑦 → ∩ 𝑦 ∈ 𝐹 ) ) )
61 57 60 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑧 = ∩ 𝑦 → ( 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹 ) ) )
62 61 rexlimdva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) → ( ∃ 𝑦 ∈ ( ( 𝒫 𝐵 ∩ Fin ) ∖ { ∅ } ) 𝑧 = ∩ 𝑦 → ( 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹 ) ) )
63 23 62 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) → ( 𝑧 ∈ ( fi ‘ 𝐵 ) → ( 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹 ) ) )
64 63 imp32 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑧 ∈ ( fi ‘ 𝐵 ) ∧ 𝑥 ∈ 𝑧 ) ) → 𝑧 ∈ 𝐹 )
65 64 adantrrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑧 ∈ ( fi ‘ 𝐵 ) ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) → 𝑧 ∈ 𝐹 )
66 65 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) ∧ ( 𝑧 ∈ ( fi ‘ 𝐵 ) ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) → 𝑧 ∈ 𝐹 )
67 elssuni ⊢ ( 𝑦 ∈ 𝐽 → 𝑦 ⊆ ∪ 𝐽 )
68 67 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → 𝑦 ⊆ ∪ 𝐽 )
69 fibas ⊢ ( fi ‘ 𝐵 ) ∈ TopBases
70 tgtopon ⊢ ( ( fi ‘ 𝐵 ) ∈ TopBases → ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) ) )
71 69 70 ax-mp ⊢ ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) )
72 3 71 eqeltrdi ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) ) )
73 fiuni ⊢ ( 𝐵 ∈ V → ∪ 𝐵 = ∪ ( fi ‘ 𝐵 ) )
74 20 73 syl ⊢ ( 𝜑 → ∪ 𝐵 = ∪ ( fi ‘ 𝐵 ) )
75 2 74 eqtrd ⊢ ( 𝜑 → 𝑋 = ∪ ( fi ‘ 𝐵 ) )
76 75 fveq2d ⊢ ( 𝜑 → ( TopOn ‘ 𝑋 ) = ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) ) )
77 72 76 eleqtrrd ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
78 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
79 77 78 syl ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
80 79 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → 𝑋 = ∪ 𝐽 )
81 68 80 sseqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → 𝑦 ⊆ 𝑋 )
82 81 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) ∧ ( 𝑧 ∈ ( fi ‘ 𝐵 ) ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) → 𝑦 ⊆ 𝑋 )
83 simprrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) ∧ ( 𝑧 ∈ ( fi ‘ 𝐵 ) ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) → 𝑧 ⊆ 𝑦 )
84 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑦 ) ) → 𝑦 ∈ 𝐹 )
85 16 66 82 83 84 syl13anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) ∧ ( 𝑧 ∈ ( fi ‘ 𝐵 ) ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) → 𝑦 ∈ 𝐹 )
86 13 85 rexlimddv ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → 𝑦 ∈ 𝐹 )
87 86 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) )
88 87 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) ) → ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) )
89 88 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) → ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) ) )
90 89 imdistanda ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ ( 𝐵 ∖ 𝐹 ) ) → ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) ) ) )
91 7 90 syl5bi ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 ∖ ∪ ( 𝐵 ∖ 𝐹 ) ) → ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) ) ) )
92 flimopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) ) ) )
93 77 15 92 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) ) ) )
94 91 93 sylibrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 ∖ ∪ ( 𝐵 ∖ 𝐹 ) ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) )
95 94 ssrdv ⊢ ( 𝜑 → ( 𝑋 ∖ ∪ ( 𝐵 ∖ 𝐹 ) ) ⊆ ( 𝐽 fLim 𝐹 ) )
96 sseq0 ⊢ ( ( ( 𝑋 ∖ ∪ ( 𝐵 ∖ 𝐹 ) ) ⊆ ( 𝐽 fLim 𝐹 ) ∧ ( 𝐽 fLim 𝐹 ) = ∅ ) → ( 𝑋 ∖ ∪ ( 𝐵 ∖ 𝐹 ) ) = ∅ )
97 95 6 96 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∖ ∪ ( 𝐵 ∖ 𝐹 ) ) = ∅ )
98 ssdif0 ⊢ ( 𝑋 ⊆ ∪ ( 𝐵 ∖ 𝐹 ) ↔ ( 𝑋 ∖ ∪ ( 𝐵 ∖ 𝐹 ) ) = ∅ )
99 97 98 sylibr ⊢ ( 𝜑 → 𝑋 ⊆ ∪ ( 𝐵 ∖ 𝐹 ) )
100 difss ⊢ ( 𝐵 ∖ 𝐹 ) ⊆ 𝐵
101 100 unissi ⊢ ∪ ( 𝐵 ∖ 𝐹 ) ⊆ ∪ 𝐵
102 101 2 sseqtrrid ⊢ ( 𝜑 → ∪ ( 𝐵 ∖ 𝐹 ) ⊆ 𝑋 )
103 99 102 eqssd ⊢ ( 𝜑 → 𝑋 = ∪ ( 𝐵 ∖ 𝐹 ) )
104 103 100 jctil ⊢ ( 𝜑 → ( ( 𝐵 ∖ 𝐹 ) ⊆ 𝐵 ∧ 𝑋 = ∪ ( 𝐵 ∖ 𝐹 ) ) )
105 difexg ⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ 𝐹 ) ∈ V )
106 20 105 syl ⊢ ( 𝜑 → ( 𝐵 ∖ 𝐹 ) ∈ V )
107 106 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐵 ∖ 𝐹 ) ⊆ 𝐵 ∧ 𝑋 = ∪ ( 𝐵 ∖ 𝐹 ) ) ) → ( 𝐵 ∖ 𝐹 ) ∈ V )
108 sseq1 ⊢ ( 𝑥 = ( 𝐵 ∖ 𝐹 ) → ( 𝑥 ⊆ 𝐵 ↔ ( 𝐵 ∖ 𝐹 ) ⊆ 𝐵 ) )
109 unieq ⊢ ( 𝑥 = ( 𝐵 ∖ 𝐹 ) → ∪ 𝑥 = ∪ ( 𝐵 ∖ 𝐹 ) )
110 109 eqeq2d ⊢ ( 𝑥 = ( 𝐵 ∖ 𝐹 ) → ( 𝑋 = ∪ 𝑥 ↔ 𝑋 = ∪ ( 𝐵 ∖ 𝐹 ) ) )
111 108 110 anbi12d ⊢ ( 𝑥 = ( 𝐵 ∖ 𝐹 ) → ( ( 𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥 ) ↔ ( ( 𝐵 ∖ 𝐹 ) ⊆ 𝐵 ∧ 𝑋 = ∪ ( 𝐵 ∖ 𝐹 ) ) ) )
112 111 anbi2d ⊢ ( 𝑥 = ( 𝐵 ∖ 𝐹 ) → ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥 ) ) ↔ ( 𝜑 ∧ ( ( 𝐵 ∖ 𝐹 ) ⊆ 𝐵 ∧ 𝑋 = ∪ ( 𝐵 ∖ 𝐹 ) ) ) ) )
113 pweq ⊢ ( 𝑥 = ( 𝐵 ∖ 𝐹 ) → 𝒫 𝑥 = 𝒫 ( 𝐵 ∖ 𝐹 ) )
114 113 ineq1d ⊢ ( 𝑥 = ( 𝐵 ∖ 𝐹 ) → ( 𝒫 𝑥 ∩ Fin ) = ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) )
115 114 rexeqdv ⊢ ( 𝑥 = ( 𝐵 ∖ 𝐹 ) → ( ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 ↔ ∃ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) 𝑋 = ∪ 𝑦 ) )
116 112 115 imbi12d ⊢ ( 𝑥 = ( 𝐵 ∖ 𝐹 ) → ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 ) ↔ ( ( 𝜑 ∧ ( ( 𝐵 ∖ 𝐹 ) ⊆ 𝐵 ∧ 𝑋 = ∪ ( 𝐵 ∖ 𝐹 ) ) ) → ∃ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) 𝑋 = ∪ 𝑦 ) ) )
117 116 4 vtoclg ⊢ ( ( 𝐵 ∖ 𝐹 ) ∈ V → ( ( 𝜑 ∧ ( ( 𝐵 ∖ 𝐹 ) ⊆ 𝐵 ∧ 𝑋 = ∪ ( 𝐵 ∖ 𝐹 ) ) ) → ∃ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) 𝑋 = ∪ 𝑦 ) )
118 107 117 mpcom ⊢ ( ( 𝜑 ∧ ( ( 𝐵 ∖ 𝐹 ) ⊆ 𝐵 ∧ 𝑋 = ∪ ( 𝐵 ∖ 𝐹 ) ) ) → ∃ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) 𝑋 = ∪ 𝑦 )
119 104 118 mpdan ⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) 𝑋 = ∪ 𝑦 )
120 unieq ⊢ ( 𝑦 = ∅ → ∪ 𝑦 = ∪ ∅ )
121 uni0 ⊢ ∪ ∅ = ∅
122 120 121 eqtrdi ⊢ ( 𝑦 = ∅ → ∪ 𝑦 = ∅ )
123 122 neeq2d ⊢ ( 𝑦 = ∅ → ( 𝑋 ≠ ∪ 𝑦 ↔ 𝑋 ≠ ∅ ) )
124 difssd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) → ( 𝑋 ∖ 𝑧 ) ⊆ 𝑋 )
125 124 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) → ∀ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) ⊆ 𝑋 )
126 riinn0 ⊢ ( ( ∀ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) ⊆ 𝑋 ∧ 𝑦 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) ) = ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) )
127 125 126 sylan ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) ) = ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) )
128 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑋 ∈ V )
129 difexg ⊢ ( 𝑋 ∈ V → ( 𝑋 ∖ 𝑧 ) ∈ V )
130 128 129 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ( 𝑋 ∖ 𝑧 ) ∈ V )
131 130 ralrimivw ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ∀ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) ∈ V )
132 dfiin2g ⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) ∈ V → ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) = ∩ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑦 𝑥 = ( 𝑋 ∖ 𝑧 ) } )
133 131 132 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) = ∩ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑦 𝑥 = ( 𝑋 ∖ 𝑧 ) } )
134 eqid ⊢ ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) = ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) )
135 134 rnmpt ⊢ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) = { 𝑥 ∣ ∃ 𝑧 ∈ 𝑦 𝑥 = ( 𝑋 ∖ 𝑧 ) }
136 135 inteqi ⊢ ∩ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) = ∩ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑦 𝑥 = ( 𝑋 ∖ 𝑧 ) }
137 133 136 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) = ∩ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) )
138 127 137 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) ) = ∩ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) )
139 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
140 elfpw ⊢ ( 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ↔ ( 𝑦 ⊆ ( 𝐵 ∖ 𝐹 ) ∧ 𝑦 ∈ Fin ) )
141 140 simplbi ⊢ ( 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) → 𝑦 ⊆ ( 𝐵 ∖ 𝐹 ) )
142 141 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑦 ⊆ ( 𝐵 ∖ 𝐹 ) )
143 142 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ ( 𝐵 ∖ 𝐹 ) )
144 143 eldifbd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝐹 )
145 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ 𝑦 ) → 𝐹 ∈ ( UFil ‘ 𝑋 ) )
146 142 difss2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑦 ⊆ 𝐵 )
147 146 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ 𝐵 )
148 elssuni ⊢ ( 𝑧 ∈ 𝐵 → 𝑧 ⊆ ∪ 𝐵 )
149 147 148 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ⊆ ∪ 𝐵 )
150 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ 𝑦 ) → 𝑋 = ∪ 𝐵 )
151 149 150 sseqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ⊆ 𝑋 )
152 ufilb ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ) → ( ¬ 𝑧 ∈ 𝐹 ↔ ( 𝑋 ∖ 𝑧 ) ∈ 𝐹 ) )
153 145 151 152 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ 𝑦 ) → ( ¬ 𝑧 ∈ 𝐹 ↔ ( 𝑋 ∖ 𝑧 ) ∈ 𝐹 ) )
154 144 153 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ 𝑦 ) → ( 𝑋 ∖ 𝑧 ) ∈ 𝐹 )
155 154 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) : 𝑦 ⟶ 𝐹 )
156 155 frnd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) ⊆ 𝐹 )
157 134 154 dmmptd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → dom ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) = 𝑦 )
158 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑦 ≠ ∅ )
159 157 158 eqnetrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → dom ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) ≠ ∅ )
160 dm0rn0 ⊢ ( dom ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) = ∅ ↔ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) = ∅ )
161 160 necon3bii ⊢ ( dom ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) ≠ ∅ ↔ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) ≠ ∅ )
162 159 161 sylib ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) ≠ ∅ )
163 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) → 𝑦 ∈ Fin )
164 163 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑦 ∈ Fin )
165 abrexfi ⊢ ( 𝑦 ∈ Fin → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑦 𝑥 = ( 𝑋 ∖ 𝑧 ) } ∈ Fin )
166 135 165 eqeltrid ⊢ ( 𝑦 ∈ Fin → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) ∈ Fin )
167 164 166 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) ∈ Fin )
168 filintn0 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) ⊆ 𝐹 ∧ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) ≠ ∅ ∧ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) ∈ Fin ) ) → ∩ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) ≠ ∅ )
169 139 156 162 167 168 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ∩ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑋 ∖ 𝑧 ) ) ≠ ∅ )
170 138 169 eqnetrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ( 𝑋 ∩ ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) ) ≠ ∅ )
171 disj3 ⊢ ( ( 𝑋 ∩ ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) ) = ∅ ↔ 𝑋 = ( 𝑋 ∖ ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) ) )
172 171 necon3bii ⊢ ( ( 𝑋 ∩ ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) ) ≠ ∅ ↔ 𝑋 ≠ ( 𝑋 ∖ ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) ) )
173 170 172 sylib ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑋 ≠ ( 𝑋 ∖ ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) ) )
174 iundif2 ⊢ ∪ 𝑧 ∈ 𝑦 ( 𝑋 ∖ ( 𝑋 ∖ 𝑧 ) ) = ( 𝑋 ∖ ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) )
175 dfss4 ⊢ ( 𝑧 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝑧 ) ) = 𝑧 )
176 151 175 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ 𝑦 ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝑧 ) ) = 𝑧 )
177 176 iuneq2dv ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ∪ 𝑧 ∈ 𝑦 ( 𝑋 ∖ ( 𝑋 ∖ 𝑧 ) ) = ∪ 𝑧 ∈ 𝑦 𝑧 )
178 uniiun ⊢ ∪ 𝑦 = ∪ 𝑧 ∈ 𝑦 𝑧
179 177 178 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ∪ 𝑧 ∈ 𝑦 ( 𝑋 ∖ ( 𝑋 ∖ 𝑧 ) ) = ∪ 𝑦 )
180 174 179 eqtr3id ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ( 𝑋 ∖ ∩ 𝑧 ∈ 𝑦 ( 𝑋 ∖ 𝑧 ) ) = ∪ 𝑦 )
181 173 180 neeqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑋 ≠ ∪ 𝑦 )
182 15 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
183 filtop ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
184 fileln0 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑋 ∈ 𝐹 ) → 𝑋 ≠ ∅ )
185 182 183 184 syl2anc2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) → 𝑋 ≠ ∅ )
186 123 181 185 pm2.61ne ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) → 𝑋 ≠ ∪ 𝑦 )
187 186 neneqd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) ) → ¬ 𝑋 = ∪ 𝑦 )
188 187 nrexdv ⊢ ( 𝜑 → ¬ ∃ 𝑦 ∈ ( 𝒫 ( 𝐵 ∖ 𝐹 ) ∩ Fin ) 𝑋 = ∪ 𝑦 )
189 119 188 pm2.65i ⊢ ¬ 𝜑