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

Theorem flimfnfcls 21879
Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 21878, this theorem illustrates the duality between convergence and clustering. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
Hypothesis
Ref Expression
flimfnfcls.x 𝑋 = 𝐽
Assertion
Ref Expression
flimfnfcls (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔))))
Distinct variable groups:   𝐴,𝑔   𝑔,𝐹   𝑔,𝐽   𝑔,𝑋

Proof of Theorem flimfnfcls
Dummy variables 𝑜 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 flimfcls 21877 . . . . 5 (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔)
2 flimtop 21816 . . . . . . . . 9 (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ Top)
3 flimfnfcls.x . . . . . . . . . 10 𝑋 = 𝐽
43toptopon 20770 . . . . . . . . 9 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
52, 4sylib 208 . . . . . . . 8 (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ (TopOn‘𝑋))
65ad2antrr 762 . . . . . . 7 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐽 ∈ (TopOn‘𝑋))
7 simplr 807 . . . . . . 7 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝑔 ∈ (Fil‘𝑋))
8 simpr 476 . . . . . . 7 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐹𝑔)
9 flimss2 21823 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑔 ∈ (Fil‘𝑋) ∧ 𝐹𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
106, 7, 8, 9syl3anc 1366 . . . . . 6 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
11 simpll 805 . . . . . 6 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fLim 𝐹))
1210, 11sseldd 3637 . . . . 5 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fLim 𝑔))
131, 12sseldi 3634 . . . 4 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fClus 𝑔))
1413ex 449 . . 3 ((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) → (𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
1514ralrimiva 2995 . 2 (𝐴 ∈ (𝐽 fLim 𝐹) → ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
16 sseq2 3660 . . . . . 6 (𝑔 = 𝐹 → (𝐹𝑔𝐹𝐹))
17 oveq2 6698 . . . . . . 7 (𝑔 = 𝐹 → (𝐽 fClus 𝑔) = (𝐽 fClus 𝐹))
1817eleq2d 2716 . . . . . 6 (𝑔 = 𝐹 → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus 𝐹)))
1916, 18imbi12d 333 . . . . 5 (𝑔 = 𝐹 → ((𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹))))
2019rspcv 3336 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹))))
21 ssid 3657 . . . . . 6 𝐹𝐹
22 id 22 . . . . . 6 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)))
2321, 22mpi 20 . . . . 5 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ (𝐽 fClus 𝐹))
24 fclstop 21862 . . . . . 6 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
253fclselbas 21867 . . . . . 6 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴𝑋)
2624, 25jca 553 . . . . 5 (𝐴 ∈ (𝐽 fClus 𝐹) → (𝐽 ∈ Top ∧ 𝐴𝑋))
2723, 26syl 17 . . . 4 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐽 ∈ Top ∧ 𝐴𝑋))
2820, 27syl6 35 . . 3 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐽 ∈ Top ∧ 𝐴𝑋)))
29 disjdif 4073 . . . . . . . . . . . . . 14 (𝑜 ∩ (𝑋𝑜)) = ∅
30 simpll 805 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ∈ (Fil‘𝑋))
31 simplrl 817 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐽 ∈ Top)
323topopn 20759 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 ∈ Top → 𝑋𝐽)
3331, 32syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑋𝐽)
34 pwexg 4880 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋𝐽 → 𝒫 𝑋 ∈ V)
35 rabexg 4844 . . . . . . . . . . . . . . . . . . . . . 22 (𝒫 𝑋 ∈ V → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V)
3633, 34, 353syl 18 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V)
37 unexg 7001 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V)
3830, 36, 37syl2anc 694 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V)
39 ssfii 8366 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
4038, 39syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
41 filsspw 21702 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
42 ssrab2 3720 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋
4342a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋)
4441, 43unssd 3822 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
4544ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
46 ssun2 3810 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})
47 difss 3770 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋𝑜) ⊆ 𝑋
48 elpw2g 4857 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑋𝐽 → ((𝑋𝑜) ∈ 𝒫 𝑋 ↔ (𝑋𝑜) ⊆ 𝑋))
4933, 48syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ((𝑋𝑜) ∈ 𝒫 𝑋 ↔ (𝑋𝑜) ⊆ 𝑋))
5047, 49mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ 𝒫 𝑋)
51 ssid 3657 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋𝑜) ⊆ (𝑋𝑜)
5251a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ⊆ (𝑋𝑜))
53 sseq2 3660 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑋𝑜) → ((𝑋𝑜) ⊆ 𝑥 ↔ (𝑋𝑜) ⊆ (𝑋𝑜)))
5453elrab 3396 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝑜) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ↔ ((𝑋𝑜) ∈ 𝒫 𝑋 ∧ (𝑋𝑜) ⊆ (𝑋𝑜)))
5550, 52, 54sylanbrc 699 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})
5646, 55sseldi 3634 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))
57 ne0i 3954 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋𝑜) ∈ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅)
5856, 57syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅)
59 sseq2 3660 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝑧 → ((𝑋𝑜) ⊆ 𝑥 ↔ (𝑋𝑜) ⊆ 𝑧))
6059elrab 3396 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ↔ (𝑧 ∈ 𝒫 𝑋 ∧ (𝑋𝑜) ⊆ 𝑧))
6160simprbi 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} → (𝑋𝑜) ⊆ 𝑧)
6261ad2antll 765 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑋𝑜) ⊆ 𝑧)
63 sslin 3872 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝑜) ⊆ 𝑧 → (𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧))
6462, 63syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧))
65 simprrr 822 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ¬ 𝑜𝐹)
6665adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ¬ 𝑜𝐹)
67 inssdif0 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦𝑋) ⊆ 𝑜 ↔ (𝑦 ∩ (𝑋𝑜)) = ∅)
68 simplll 813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝐹 ∈ (Fil‘𝑋))
69 simprl 809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝑦𝐹)
70 filelss 21703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹) → 𝑦𝑋)
7168, 69, 70syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝑦𝑋)
72 df-ss 3621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦𝑋 ↔ (𝑦𝑋) = 𝑦)
7371, 72sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑋) = 𝑦)
7473sseq1d 3665 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦𝑋) ⊆ 𝑜𝑦𝑜))
7530ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝐹 ∈ (Fil‘𝑋))
76 simplrl 817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑦𝐹)
77 elssuni 4499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑜𝐽𝑜 𝐽)
7877, 3syl6sseqr 3685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑜𝐽𝑜𝑋)
7978ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑜𝑋)
8079ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑜𝑋)
81 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑦𝑜)
82 filss 21704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑜𝑋𝑦𝑜)) → 𝑜𝐹)
8375, 76, 80, 81, 82syl13anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑜𝐹)
8483ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑜𝑜𝐹))
8574, 84sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦𝑋) ⊆ 𝑜𝑜𝐹))
8667, 85syl5bir 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦 ∩ (𝑋𝑜)) = ∅ → 𝑜𝐹))
8786necon3bd 2837 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (¬ 𝑜𝐹 → (𝑦 ∩ (𝑋𝑜)) ≠ ∅))
8866, 87mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋𝑜)) ≠ ∅)
89 ssn0 4009 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧) ∧ (𝑦 ∩ (𝑋𝑜)) ≠ ∅) → (𝑦𝑧) ≠ ∅)
9064, 88, 89syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑧) ≠ ∅)
9190ralrimivva 3000 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅)
92 filfbas 21699 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
9330, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ∈ (fBas‘𝑋))
9447a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ⊆ 𝑋)
95 filtop 21706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
9630, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑋𝐹)
97 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑜 = 𝑋 → (𝑜𝐹𝑋𝐹))
9896, 97syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑜 = 𝑋𝑜𝐹))
9998necon3bd 2837 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (¬ 𝑜𝐹𝑜𝑋))
10065, 99mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑜𝑋)
101 pssdifn0 3977 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑜𝑋𝑜𝑋) → (𝑋𝑜) ≠ ∅)
10279, 100, 101syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ≠ ∅)
103 supfil 21746 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝐽 ∧ (𝑋𝑜) ⊆ 𝑋 ∧ (𝑋𝑜) ≠ ∅) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
10433, 94, 102, 103syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
105 filfbas 21699 . . . . . . . . . . . . . . . . . . . . . . . 24 ({𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
106104, 105syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
107 fbunfip 21720 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ↔ ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅))
10893, 106, 107syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ↔ ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅))
10991, 108mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
110 fsubbas 21718 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋𝐹 → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
11196, 110syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
11245, 58, 109, 111mpbir3and 1264 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋))
113 ssfg 21723 . . . . . . . . . . . . . . . . . . . 20 ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
114112, 113syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
11540, 114sstrd 3646 . . . . . . . . . . . . . . . . . 18 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
116115unssad 3823 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
117 fgcl 21729 . . . . . . . . . . . . . . . . . . 19 ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
118112, 117syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
119 sseq2 3660 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → (𝐹𝑔𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
120 oveq2 6698 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → (𝐽 fClus 𝑔) = (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
121120eleq2d 2716 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))))
122119, 121imbi12d 333 . . . . . . . . . . . . . . . . . . 19 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → ((𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))))
123122rspcv 3336 . . . . . . . . . . . . . . . . . 18 ((𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))))
124118, 123syl 17 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))))
125116, 124mpid 44 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))))
126 simpr 476 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
127 simplrl 817 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → 𝑜𝐽)
128 simprrl 821 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐴𝑜)
129128adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → 𝐴𝑜)
130115, 56sseldd 3637 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
131130adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
132 fclsopni 21866 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))) ∧ (𝑜𝐽𝐴𝑜 ∧ (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅)
133126, 127, 129, 131, 132syl13anc 1368 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅)
134133ex 449 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅))
135125, 134syld 47 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅))
136135necon2bd 2839 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ((𝑜 ∩ (𝑋𝑜)) = ∅ → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔))))
13729, 136mpi 20 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
138137anassrs 681 . . . . . . . . . . . 12 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹)) → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
139138expr 642 . . . . . . . . . . 11 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) ∧ 𝐴𝑜) → (¬ 𝑜𝐹 → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔))))
140139con4d 114 . . . . . . . . . 10 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) ∧ 𝐴𝑜) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝑜𝐹))
141140ex 449 . . . . . . . . 9 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) → (𝐴𝑜 → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝑜𝐹)))
142141com23 86 . . . . . . . 8 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴𝑜𝑜𝐹)))
143142ralrimdva 2998 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → ∀𝑜𝐽 (𝐴𝑜𝑜𝐹)))
144 simprr 811 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐴𝑋)
145143, 144jctild 565 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜𝑜𝐹))))
146 simprl 809 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐽 ∈ Top)
147146, 4sylib 208 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
148 simpl 472 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐹 ∈ (Fil‘𝑋))
149 flimopn 21826 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜𝑜𝐹))))
150147, 148, 149syl2anc 694 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜𝑜𝐹))))
151145, 150sylibrd 249 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹)))
152151ex 449 . . . 4 (𝐹 ∈ (Fil‘𝑋) → ((𝐽 ∈ Top ∧ 𝐴𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹))))
153152com23 86 . . 3 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → ((𝐽 ∈ Top ∧ 𝐴𝑋) → 𝐴 ∈ (𝐽 fLim 𝐹))))
15428, 153mpdd 43 . 2 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹)))
15515, 154impbid2 216 1 (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  {crab 2945  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  𝒫 cpw 4191   cuni 4468  cfv 5926  (class class class)co 6690  ficfi 8357  fBascfbas 19782  filGencfg 19783  Topctop 20746  TopOnctopon 20763  Filcfil 21696   fLim cflim 21785   fClus cfcls 21787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-fin 8001  df-fi 8358  df-fbas 19791  df-fg 19792  df-top 20747  df-topon 20764  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-fil 21697  df-flim 21790  df-fcls 21792
This theorem is referenced by:  cnpfcf  21892
  Copyright terms: Public domain W3C validator