Metamath Proof Explorer

Theorem flimfnfcls

Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim , this theorem illustrates the duality between convergence and clustering. (Contributed by Jeff Hankins, 12-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Hypothesis flimfnfcls.x ⊢ 𝑋 = ∪ 𝐽
Assertion flimfnfcls ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) ) )

Proof

Step Hyp Ref Expression
1 flimfnfcls.x ⊢ 𝑋 = ∪ 𝐽
2 flimfcls ⊢ ( 𝐽 fLim 𝑔 ) ⊆ ( 𝐽 fClus 𝑔 )
3 flimtop ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐽 ∈ Top )
4 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5 3 4 sylib ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6 5 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐹 ⊆ 𝑔 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
7 simplr ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐹 ⊆ 𝑔 ) → 𝑔 ∈ ( Fil ‘ 𝑋 ) )
8 simpr ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐹 ⊆ 𝑔 ) → 𝐹 ⊆ 𝑔 )
9 flimss2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝑔 ) → ( 𝐽 fLim 𝐹 ) ⊆ ( 𝐽 fLim 𝑔 ) )
10 6 7 8 9 syl3anc ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐹 ⊆ 𝑔 ) → ( 𝐽 fLim 𝐹 ) ⊆ ( 𝐽 fLim 𝑔 ) )
11 simpll ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐹 ⊆ 𝑔 ) → 𝐴 ∈ ( 𝐽 fLim 𝐹 ) )
12 10 11 sseldd ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐹 ⊆ 𝑔 ) → 𝐴 ∈ ( 𝐽 fLim 𝑔 ) )
13 2 12 sselid ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐹 ⊆ 𝑔 ) → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) )
14 13 ex ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) )
15 14 ralrimiva ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) )
16 sseq2 ⊢ ( 𝑔 = 𝐹 → ( 𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ 𝐹 ) )
17 oveq2 ⊢ ( 𝑔 = 𝐹 → ( 𝐽 fClus 𝑔 ) = ( 𝐽 fClus 𝐹 ) )
18 17 eleq2d ⊢ ( 𝑔 = 𝐹 → ( 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ↔ 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) )
19 16 18 imbi12d ⊢ ( 𝑔 = 𝐹 → ( ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) ↔ ( 𝐹 ⊆ 𝐹 → 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) ) )
20 19 rspcv ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → ( 𝐹 ⊆ 𝐹 → 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) ) )
21 ssid ⊢ 𝐹 ⊆ 𝐹
22 id ⊢ ( ( 𝐹 ⊆ 𝐹 → 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( 𝐹 ⊆ 𝐹 → 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) )
23 21 22 mpi ⊢ ( ( 𝐹 ⊆ 𝐹 → 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝐴 ∈ ( 𝐽 fClus 𝐹 ) )
24 fclstop ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐽 ∈ Top )
25 1 fclselbas ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐴 ∈ 𝑋 )
26 24 25 jca ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) )
27 23 26 syl ⊢ ( ( 𝐹 ⊆ 𝐹 → 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) → ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) )
28 20 27 syl6 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) )
29 disjdif ⊢ ( 𝑜 ∩ ( 𝑋 ∖ 𝑜 ) ) = ∅
30 simpll ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
31 simplrl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → 𝐽 ∈ Top )
32 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
33 31 32 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → 𝑋 ∈ 𝐽 )
34 pwexg ⊢ ( 𝑋 ∈ 𝐽 → 𝒫 𝑋 ∈ V )
35 rabexg ⊢ ( 𝒫 𝑋 ∈ V → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ∈ V )
36 33 34 35 3syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ∈ V )
37 unexg ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ∈ V ) → ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ∈ V )
38 30 36 37 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ∈ V )
39 ssfii ⊢ ( ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ∈ V → ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ⊆ ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) )
40 38 39 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ⊆ ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) )
41 filsspw ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 )
42 ssrab2 ⊢ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ⊆ 𝒫 𝑋
43 42 a1i ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ⊆ 𝒫 𝑋 )
44 41 43 unssd ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ⊆ 𝒫 𝑋 )
45 44 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ⊆ 𝒫 𝑋 )
46 ssun2 ⊢ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ⊆ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } )
47 sseq2 ⊢ ( 𝑥 = ( 𝑋 ∖ 𝑜 ) → ( ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 ↔ ( 𝑋 ∖ 𝑜 ) ⊆ ( 𝑋 ∖ 𝑜 ) ) )
48 difss ⊢ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑋
49 elpw2g ⊢ ( 𝑋 ∈ 𝐽 → ( ( 𝑋 ∖ 𝑜 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑋 ) )
50 33 49 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( ( 𝑋 ∖ 𝑜 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑋 ) )
51 48 50 mpbiri ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝑋 ∖ 𝑜 ) ∈ 𝒫 𝑋 )
52 ssid ⊢ ( 𝑋 ∖ 𝑜 ) ⊆ ( 𝑋 ∖ 𝑜 )
53 52 a1i ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝑋 ∖ 𝑜 ) ⊆ ( 𝑋 ∖ 𝑜 ) )
54 47 51 53 elrabd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝑋 ∖ 𝑜 ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } )
55 46 54 sselid ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝑋 ∖ 𝑜 ) ∈ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) )
56 55 ne0d ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ≠ ∅ )
57 sseq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 ↔ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑧 ) )
58 57 elrab ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ↔ ( 𝑧 ∈ 𝒫 𝑋 ∧ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑧 ) )
59 58 simprbi ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } → ( 𝑋 ∖ 𝑜 ) ⊆ 𝑧 )
60 59 ad2antll ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) → ( 𝑋 ∖ 𝑜 ) ⊆ 𝑧 )
61 sslin ⊢ ( ( 𝑋 ∖ 𝑜 ) ⊆ 𝑧 → ( 𝑦 ∩ ( 𝑋 ∖ 𝑜 ) ) ⊆ ( 𝑦 ∩ 𝑧 ) )
62 60 61 syl ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) → ( 𝑦 ∩ ( 𝑋 ∖ 𝑜 ) ) ⊆ ( 𝑦 ∩ 𝑧 ) )
63 simprrr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ¬ 𝑜 ∈ 𝐹 )
64 63 adantr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) → ¬ 𝑜 ∈ 𝐹 )
65 inssdif0 ⊢ ( ( 𝑦 ∩ 𝑋 ) ⊆ 𝑜 ↔ ( 𝑦 ∩ ( 𝑋 ∖ 𝑜 ) ) = ∅ )
66 simplll ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
67 simprl ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) → 𝑦 ∈ 𝐹 )
68 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → 𝑦 ⊆ 𝑋 )
69 66 67 68 syl2anc ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) → 𝑦 ⊆ 𝑋 )
70 df-ss ⊢ ( 𝑦 ⊆ 𝑋 ↔ ( 𝑦 ∩ 𝑋 ) = 𝑦 )
71 69 70 sylib ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) → ( 𝑦 ∩ 𝑋 ) = 𝑦 )
72 71 sseq1d ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) → ( ( 𝑦 ∩ 𝑋 ) ⊆ 𝑜 ↔ 𝑦 ⊆ 𝑜 ) )
73 30 ad2antrr ⊢ ( ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ∧ 𝑦 ⊆ 𝑜 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
74 simplrl ⊢ ( ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ∧ 𝑦 ⊆ 𝑜 ) → 𝑦 ∈ 𝐹 )
75 elssuni ⊢ ( 𝑜 ∈ 𝐽 → 𝑜 ⊆ ∪ 𝐽 )
76 75 1 sseqtrrdi ⊢ ( 𝑜 ∈ 𝐽 → 𝑜 ⊆ 𝑋 )
77 76 ad2antrl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → 𝑜 ⊆ 𝑋 )
78 77 ad2antrr ⊢ ( ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ∧ 𝑦 ⊆ 𝑜 ) → 𝑜 ⊆ 𝑋 )
79 simpr ⊢ ( ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ∧ 𝑦 ⊆ 𝑜 ) → 𝑦 ⊆ 𝑜 )
80 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑜 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑜 ) ) → 𝑜 ∈ 𝐹 )
81 73 74 78 79 80 syl13anc ⊢ ( ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ∧ 𝑦 ⊆ 𝑜 ) → 𝑜 ∈ 𝐹 )
82 81 ex ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) → ( 𝑦 ⊆ 𝑜 → 𝑜 ∈ 𝐹 ) )
83 72 82 sylbid ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) → ( ( 𝑦 ∩ 𝑋 ) ⊆ 𝑜 → 𝑜 ∈ 𝐹 ) )
84 65 83 syl5bir ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) → ( ( 𝑦 ∩ ( 𝑋 ∖ 𝑜 ) ) = ∅ → 𝑜 ∈ 𝐹 ) )
85 84 necon3bd ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) → ( ¬ 𝑜 ∈ 𝐹 → ( 𝑦 ∩ ( 𝑋 ∖ 𝑜 ) ) ≠ ∅ ) )
86 64 85 mpd ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) → ( 𝑦 ∩ ( 𝑋 ∖ 𝑜 ) ) ≠ ∅ )
87 ssn0 ⊢ ( ( ( 𝑦 ∩ ( 𝑋 ∖ 𝑜 ) ) ⊆ ( 𝑦 ∩ 𝑧 ) ∧ ( 𝑦 ∩ ( 𝑋 ∖ 𝑜 ) ) ≠ ∅ ) → ( 𝑦 ∩ 𝑧 ) ≠ ∅ )
88 62 86 87 syl2anc ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) → ( 𝑦 ∩ 𝑧 ) ≠ ∅ )
89 88 ralrimivva ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ∀ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ( 𝑦 ∩ 𝑧 ) ≠ ∅ )
90 filfbas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
91 30 90 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
92 48 a1i ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝑋 ∖ 𝑜 ) ⊆ 𝑋 )
93 filtop ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
94 30 93 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → 𝑋 ∈ 𝐹 )
95 eleq1 ⊢ ( 𝑜 = 𝑋 → ( 𝑜 ∈ 𝐹 ↔ 𝑋 ∈ 𝐹 ) )
96 94 95 syl5ibrcom ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝑜 = 𝑋 → 𝑜 ∈ 𝐹 ) )
97 96 necon3bd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( ¬ 𝑜 ∈ 𝐹 → 𝑜 ≠ 𝑋 ) )
98 63 97 mpd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → 𝑜 ≠ 𝑋 )
99 pssdifn0 ⊢ ( ( 𝑜 ⊆ 𝑋 ∧ 𝑜 ≠ 𝑋 ) → ( 𝑋 ∖ 𝑜 ) ≠ ∅ )
100 77 98 99 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝑋 ∖ 𝑜 ) ≠ ∅ )
101 supfil ⊢ ( ( 𝑋 ∈ 𝐽 ∧ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑜 ) ≠ ∅ ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ∈ ( Fil ‘ 𝑋 ) )
102 33 92 100 101 syl3anc ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ∈ ( Fil ‘ 𝑋 ) )
103 filfbas ⊢ ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ∈ ( Fil ‘ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ∈ ( fBas ‘ 𝑋 ) )
104 102 103 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ∈ ( fBas ‘ 𝑋 ) )
105 fbunfip ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ∈ ( fBas ‘ 𝑋 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ↔ ∀ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ( 𝑦 ∩ 𝑧 ) ≠ ∅ ) )
106 91 104 105 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ↔ ∀ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ( 𝑦 ∩ 𝑧 ) ≠ ∅ ) )
107 89 106 mpbird ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) )
108 fsubbas ⊢ ( 𝑋 ∈ 𝐹 → ( ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ⊆ 𝒫 𝑋 ∧ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) )
109 94 108 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ⊆ 𝒫 𝑋 ∧ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) )
110 45 56 107 109 mpbir3and ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) )
111 ssfg ⊢ ( ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) )
112 110 111 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) )
113 40 112 sstrd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) )
114 113 unssad ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) )
115 fgcl ⊢ ( ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ∈ ( Fil ‘ 𝑋 ) )
116 110 115 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ∈ ( Fil ‘ 𝑋 ) )
117 sseq2 ⊢ ( 𝑔 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) → ( 𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) )
118 oveq2 ⊢ ( 𝑔 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) → ( 𝐽 fClus 𝑔 ) = ( 𝐽 fClus ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) )
119 118 eleq2d ⊢ ( 𝑔 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ↔ 𝐴 ∈ ( 𝐽 fClus ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) ) )
120 117 119 imbi12d ⊢ ( 𝑔 = ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) → ( ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) ↔ ( 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) → 𝐴 ∈ ( 𝐽 fClus ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) ) ) )
121 120 rspcv ⊢ ( ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ∈ ( Fil ‘ 𝑋 ) → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → ( 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) → 𝐴 ∈ ( 𝐽 fClus ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) ) ) )
122 116 121 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → ( 𝐹 ⊆ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) → 𝐴 ∈ ( 𝐽 fClus ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) ) ) )
123 114 122 mpid ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → 𝐴 ∈ ( 𝐽 fClus ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) ) )
124 simpr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ 𝐴 ∈ ( 𝐽 fClus ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) ) → 𝐴 ∈ ( 𝐽 fClus ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) )
125 simplrl ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ 𝐴 ∈ ( 𝐽 fClus ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) ) → 𝑜 ∈ 𝐽 )
126 simprrl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → 𝐴 ∈ 𝑜 )
127 126 adantr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ 𝐴 ∈ ( 𝐽 fClus ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) ) → 𝐴 ∈ 𝑜 )
128 113 55 sseldd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝑋 ∖ 𝑜 ) ∈ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) )
129 128 adantr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ 𝐴 ∈ ( 𝐽 fClus ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) ) → ( 𝑋 ∖ 𝑜 ) ∈ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) )
130 fclsopni ⊢ ( ( 𝐴 ∈ ( 𝐽 fClus ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ∧ ( 𝑋 ∖ 𝑜 ) ∈ ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) ) → ( 𝑜 ∩ ( 𝑋 ∖ 𝑜 ) ) ≠ ∅ )
131 124 125 127 129 130 syl13anc ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) ∧ 𝐴 ∈ ( 𝐽 fClus ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) ) → ( 𝑜 ∩ ( 𝑋 ∖ 𝑜 ) ) ≠ ∅ )
132 131 ex ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( 𝐴 ∈ ( 𝐽 fClus ( 𝑋 filGen ( fi ‘ ( 𝐹 ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑥 } ) ) ) ) → ( 𝑜 ∩ ( 𝑋 ∖ 𝑜 ) ) ≠ ∅ ) )
133 123 132 syld ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → ( 𝑜 ∩ ( 𝑋 ∖ 𝑜 ) ) ≠ ∅ ) )
134 133 necon2bd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ( ( 𝑜 ∩ ( 𝑋 ∖ 𝑜 ) ) = ∅ → ¬ ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) ) )
135 29 134 mpi ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) ) → ¬ ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) )
136 135 anassrs ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ 𝑜 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑜 ∧ ¬ 𝑜 ∈ 𝐹 ) ) → ¬ ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) )
137 136 expr ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝐴 ∈ 𝑜 ) → ( ¬ 𝑜 ∈ 𝐹 → ¬ ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) ) )
138 137 con4d ⊢ ( ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝐴 ∈ 𝑜 ) → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → 𝑜 ∈ 𝐹 ) )
139 138 ex ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝐴 ∈ 𝑜 → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → 𝑜 ∈ 𝐹 ) ) )
140 139 com23 ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) ∧ 𝑜 ∈ 𝐽 ) → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → ( 𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹 ) ) )
141 140 ralrimdva ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹 ) ) )
142 simprr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
143 141 142 jctild ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹 ) ) ) )
144 simprl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) → 𝐽 ∈ Top )
145 144 4 sylib ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
146 simpl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
147 flimopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹 ) ) ) )
148 145 146 147 syl2anc ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝑜 ∈ 𝐹 ) ) ) )
149 143 148 sylibrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) ) → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) )
150 149 ex ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ) )
151 150 com23 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) ) )
152 28 151 mpdd ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) → 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ) )
153 15 152 impbid2 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑔 → 𝐴 ∈ ( 𝐽 fClus 𝑔 ) ) ) )