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 20 difexd ( 𝜑 → ( 𝐵𝐹 ) ∈ V )
106 105 adantr ( ( 𝜑 ∧ ( ( 𝐵𝐹 ) ⊆ 𝐵𝑋 = ( 𝐵𝐹 ) ) ) → ( 𝐵𝐹 ) ∈ V )
107 sseq1 ( 𝑥 = ( 𝐵𝐹 ) → ( 𝑥𝐵 ↔ ( 𝐵𝐹 ) ⊆ 𝐵 ) )
108 unieq ( 𝑥 = ( 𝐵𝐹 ) → 𝑥 = ( 𝐵𝐹 ) )
109 108 eqeq2d ( 𝑥 = ( 𝐵𝐹 ) → ( 𝑋 = 𝑥𝑋 = ( 𝐵𝐹 ) ) )
110 107 109 anbi12d ( 𝑥 = ( 𝐵𝐹 ) → ( ( 𝑥𝐵𝑋 = 𝑥 ) ↔ ( ( 𝐵𝐹 ) ⊆ 𝐵𝑋 = ( 𝐵𝐹 ) ) ) )
111 110 anbi2d ( 𝑥 = ( 𝐵𝐹 ) → ( ( 𝜑 ∧ ( 𝑥𝐵𝑋 = 𝑥 ) ) ↔ ( 𝜑 ∧ ( ( 𝐵𝐹 ) ⊆ 𝐵𝑋 = ( 𝐵𝐹 ) ) ) ) )
112 pweq ( 𝑥 = ( 𝐵𝐹 ) → 𝒫 𝑥 = 𝒫 ( 𝐵𝐹 ) )
113 112 ineq1d ( 𝑥 = ( 𝐵𝐹 ) → ( 𝒫 𝑥 ∩ Fin ) = ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) )
114 113 rexeqdv ( 𝑥 = ( 𝐵𝐹 ) → ( ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ↔ ∃ 𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) 𝑋 = 𝑦 ) )
115 111 114 imbi12d ( 𝑥 = ( 𝐵𝐹 ) → ( ( ( 𝜑 ∧ ( 𝑥𝐵𝑋 = 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ↔ ( ( 𝜑 ∧ ( ( 𝐵𝐹 ) ⊆ 𝐵𝑋 = ( 𝐵𝐹 ) ) ) → ∃ 𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) 𝑋 = 𝑦 ) ) )
116 115 4 vtoclg ( ( 𝐵𝐹 ) ∈ V → ( ( 𝜑 ∧ ( ( 𝐵𝐹 ) ⊆ 𝐵𝑋 = ( 𝐵𝐹 ) ) ) → ∃ 𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) 𝑋 = 𝑦 ) )
117 106 116 mpcom ( ( 𝜑 ∧ ( ( 𝐵𝐹 ) ⊆ 𝐵𝑋 = ( 𝐵𝐹 ) ) ) → ∃ 𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) 𝑋 = 𝑦 )
118 104 117 mpdan ( 𝜑 → ∃ 𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) 𝑋 = 𝑦 )
119 unieq ( 𝑦 = ∅ → 𝑦 = ∅ )
120 uni0 ∅ = ∅
121 119 120 eqtrdi ( 𝑦 = ∅ → 𝑦 = ∅ )
122 121 neeq2d ( 𝑦 = ∅ → ( 𝑋 𝑦𝑋 ≠ ∅ ) )
123 difssd ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) → ( 𝑋𝑧 ) ⊆ 𝑋 )
124 123 ralrimivw ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) → ∀ 𝑧𝑦 ( 𝑋𝑧 ) ⊆ 𝑋 )
125 riinn0 ( ( ∀ 𝑧𝑦 ( 𝑋𝑧 ) ⊆ 𝑋𝑦 ≠ ∅ ) → ( 𝑋 𝑧𝑦 ( 𝑋𝑧 ) ) = 𝑧𝑦 ( 𝑋𝑧 ) )
126 124 125 sylan ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ( 𝑋 𝑧𝑦 ( 𝑋𝑧 ) ) = 𝑧𝑦 ( 𝑋𝑧 ) )
127 17 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑋 ∈ V )
128 127 difexd ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ( 𝑋𝑧 ) ∈ V )
129 128 ralrimivw ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ∀ 𝑧𝑦 ( 𝑋𝑧 ) ∈ V )
130 dfiin2g ( ∀ 𝑧𝑦 ( 𝑋𝑧 ) ∈ V → 𝑧𝑦 ( 𝑋𝑧 ) = { 𝑥 ∣ ∃ 𝑧𝑦 𝑥 = ( 𝑋𝑧 ) } )
131 129 130 syl ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑧𝑦 ( 𝑋𝑧 ) = { 𝑥 ∣ ∃ 𝑧𝑦 𝑥 = ( 𝑋𝑧 ) } )
132 eqid ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) = ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) )
133 132 rnmpt ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) = { 𝑥 ∣ ∃ 𝑧𝑦 𝑥 = ( 𝑋𝑧 ) }
134 133 inteqi ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) = { 𝑥 ∣ ∃ 𝑧𝑦 𝑥 = ( 𝑋𝑧 ) }
135 131 134 eqtr4di ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑧𝑦 ( 𝑋𝑧 ) = ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) )
136 126 135 eqtrd ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ( 𝑋 𝑧𝑦 ( 𝑋𝑧 ) ) = ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) )
137 15 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
138 elfpw ( 𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ↔ ( 𝑦 ⊆ ( 𝐵𝐹 ) ∧ 𝑦 ∈ Fin ) )
139 138 simplbi ( 𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) → 𝑦 ⊆ ( 𝐵𝐹 ) )
140 139 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑦 ⊆ ( 𝐵𝐹 ) )
141 140 sselda ( ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧𝑦 ) → 𝑧 ∈ ( 𝐵𝐹 ) )
142 141 eldifbd ( ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧𝑦 ) → ¬ 𝑧𝐹 )
143 5 ad3antrrr ( ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧𝑦 ) → 𝐹 ∈ ( UFil ‘ 𝑋 ) )
144 140 difss2d ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑦𝐵 )
145 144 sselda ( ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧𝑦 ) → 𝑧𝐵 )
146 elssuni ( 𝑧𝐵𝑧 𝐵 )
147 145 146 syl ( ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧𝑦 ) → 𝑧 𝐵 )
148 2 ad3antrrr ( ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧𝑦 ) → 𝑋 = 𝐵 )
149 147 148 sseqtrrd ( ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧𝑦 ) → 𝑧𝑋 )
150 ufilb ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑧𝑋 ) → ( ¬ 𝑧𝐹 ↔ ( 𝑋𝑧 ) ∈ 𝐹 ) )
151 143 149 150 syl2anc ( ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧𝑦 ) → ( ¬ 𝑧𝐹 ↔ ( 𝑋𝑧 ) ∈ 𝐹 ) )
152 142 151 mpbid ( ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧𝑦 ) → ( 𝑋𝑧 ) ∈ 𝐹 )
153 152 fmpttd ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) : 𝑦𝐹 )
154 153 frnd ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) ⊆ 𝐹 )
155 132 152 dmmptd ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → dom ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) = 𝑦 )
156 simpr ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑦 ≠ ∅ )
157 155 156 eqnetrd ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → dom ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) ≠ ∅ )
158 dm0rn0 ( dom ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) = ∅ ↔ ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) = ∅ )
159 158 necon3bii ( dom ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) ≠ ∅ ↔ ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) ≠ ∅ )
160 157 159 sylib ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) ≠ ∅ )
161 elinel2 ( 𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) → 𝑦 ∈ Fin )
162 161 ad2antlr ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑦 ∈ Fin )
163 abrexfi ( 𝑦 ∈ Fin → { 𝑥 ∣ ∃ 𝑧𝑦 𝑥 = ( 𝑋𝑧 ) } ∈ Fin )
164 133 163 eqeltrid ( 𝑦 ∈ Fin → ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) ∈ Fin )
165 162 164 syl ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) ∈ Fin )
166 filintn0 ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) ⊆ 𝐹 ∧ ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) ≠ ∅ ∧ ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) ∈ Fin ) ) → ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) ≠ ∅ )
167 137 154 160 165 166 syl13anc ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ran ( 𝑧𝑦 ↦ ( 𝑋𝑧 ) ) ≠ ∅ )
168 136 167 eqnetrd ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ( 𝑋 𝑧𝑦 ( 𝑋𝑧 ) ) ≠ ∅ )
169 disj3 ( ( 𝑋 𝑧𝑦 ( 𝑋𝑧 ) ) = ∅ ↔ 𝑋 = ( 𝑋 𝑧𝑦 ( 𝑋𝑧 ) ) )
170 169 necon3bii ( ( 𝑋 𝑧𝑦 ( 𝑋𝑧 ) ) ≠ ∅ ↔ 𝑋 ≠ ( 𝑋 𝑧𝑦 ( 𝑋𝑧 ) ) )
171 168 170 sylib ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑋 ≠ ( 𝑋 𝑧𝑦 ( 𝑋𝑧 ) ) )
172 iundif2 𝑧𝑦 ( 𝑋 ∖ ( 𝑋𝑧 ) ) = ( 𝑋 𝑧𝑦 ( 𝑋𝑧 ) )
173 dfss4 ( 𝑧𝑋 ↔ ( 𝑋 ∖ ( 𝑋𝑧 ) ) = 𝑧 )
174 149 173 sylib ( ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧𝑦 ) → ( 𝑋 ∖ ( 𝑋𝑧 ) ) = 𝑧 )
175 174 iuneq2dv ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑧𝑦 ( 𝑋 ∖ ( 𝑋𝑧 ) ) = 𝑧𝑦 𝑧 )
176 uniiun 𝑦 = 𝑧𝑦 𝑧
177 175 176 eqtr4di ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑧𝑦 ( 𝑋 ∖ ( 𝑋𝑧 ) ) = 𝑦 )
178 172 177 eqtr3id ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → ( 𝑋 𝑧𝑦 ( 𝑋𝑧 ) ) = 𝑦 )
179 171 178 neeqtrd ( ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) ∧ 𝑦 ≠ ∅ ) → 𝑋 𝑦 )
180 15 adantr ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
181 filtop ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋𝐹 )
182 fileln0 ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑋𝐹 ) → 𝑋 ≠ ∅ )
183 180 181 182 syl2anc2 ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) → 𝑋 ≠ ∅ )
184 122 179 183 pm2.61ne ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) → 𝑋 𝑦 )
185 184 neneqd ( ( 𝜑𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) ) → ¬ 𝑋 = 𝑦 )
186 185 nrexdv ( 𝜑 → ¬ ∃ 𝑦 ∈ ( 𝒫 ( 𝐵𝐹 ) ∩ Fin ) 𝑋 = 𝑦 )
187 118 186 pm2.65i ¬ 𝜑