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

Theorem flimfnfcls 22111
Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 22110, 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 22109 . . . . 5 (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔)
2 flimtop 22048 . . . . . . . . 9 (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ Top)
3 flimfnfcls.x . . . . . . . . . 10 𝑋 = 𝐽
43toptopon 21001 . . . . . . . . 9 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
52, 4sylib 209 . . . . . . . 8 (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ (TopOn‘𝑋))
65ad2antrr 717 . . . . . . 7 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐽 ∈ (TopOn‘𝑋))
7 simplr 785 . . . . . . 7 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝑔 ∈ (Fil‘𝑋))
8 simpr 477 . . . . . . 7 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐹𝑔)
9 flimss2 22055 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑔 ∈ (Fil‘𝑋) ∧ 𝐹𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
106, 7, 8, 9syl3anc 1490 . . . . . 6 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
11 simpll 783 . . . . . 6 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fLim 𝐹))
1210, 11sseldd 3762 . . . . 5 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fLim 𝑔))
131, 12sseldi 3759 . . . 4 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fClus 𝑔))
1413ex 401 . . 3 ((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) → (𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
1514ralrimiva 3113 . 2 (𝐴 ∈ (𝐽 fLim 𝐹) → ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
16 sseq2 3787 . . . . . 6 (𝑔 = 𝐹 → (𝐹𝑔𝐹𝐹))
17 oveq2 6850 . . . . . . 7 (𝑔 = 𝐹 → (𝐽 fClus 𝑔) = (𝐽 fClus 𝐹))
1817eleq2d 2830 . . . . . 6 (𝑔 = 𝐹 → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus 𝐹)))
1916, 18imbi12d 335 . . . . 5 (𝑔 = 𝐹 → ((𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹))))
2019rspcv 3457 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹))))
21 ssid 3783 . . . . . 6 𝐹𝐹
22 id 22 . . . . . 6 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)))
2321, 22mpi 20 . . . . 5 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ (𝐽 fClus 𝐹))
24 fclstop 22094 . . . . . 6 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
253fclselbas 22099 . . . . . 6 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴𝑋)
2624, 25jca 507 . . . . 5 (𝐴 ∈ (𝐽 fClus 𝐹) → (𝐽 ∈ Top ∧ 𝐴𝑋))
2723, 26syl 17 . . . 4 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐽 ∈ Top ∧ 𝐴𝑋))
2820, 27syl6 35 . . 3 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐽 ∈ Top ∧ 𝐴𝑋)))
29 disjdif 4200 . . . . . . . . . . . . . 14 (𝑜 ∩ (𝑋𝑜)) = ∅
30 simpll 783 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ∈ (Fil‘𝑋))
31 simplrl 795 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐽 ∈ Top)
323topopn 20990 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 ∈ Top → 𝑋𝐽)
3331, 32syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑋𝐽)
34 pwexg 5014 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋𝐽 → 𝒫 𝑋 ∈ V)
35 rabexg 4972 . . . . . . . . . . . . . . . . . . . . . 22 (𝒫 𝑋 ∈ V → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V)
3633, 34, 353syl 18 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V)
37 unexg 7157 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V)
3830, 36, 37syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V)
39 ssfii 8532 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
4038, 39syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
41 filsspw 21934 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
42 ssrab2 3847 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋
4342a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋)
4441, 43unssd 3951 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
4544ad2antrr 717 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
46 ssun2 3939 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})
47 difss 3899 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋𝑜) ⊆ 𝑋
48 elpw2g 4985 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑋𝐽 → ((𝑋𝑜) ∈ 𝒫 𝑋 ↔ (𝑋𝑜) ⊆ 𝑋))
4933, 48syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ((𝑋𝑜) ∈ 𝒫 𝑋 ↔ (𝑋𝑜) ⊆ 𝑋))
5047, 49mpbiri 249 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ 𝒫 𝑋)
51 ssid 3783 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋𝑜) ⊆ (𝑋𝑜)
5251a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ⊆ (𝑋𝑜))
53 sseq2 3787 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑋𝑜) → ((𝑋𝑜) ⊆ 𝑥 ↔ (𝑋𝑜) ⊆ (𝑋𝑜)))
5453elrab 3519 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑋𝑜) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ↔ ((𝑋𝑜) ∈ 𝒫 𝑋 ∧ (𝑋𝑜) ⊆ (𝑋𝑜)))
5550, 52, 54sylanbrc 578 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})
5646, 55sseldi 3759 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))
5756ne0d 4086 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅)
58 sseq2 3787 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝑧 → ((𝑋𝑜) ⊆ 𝑥 ↔ (𝑋𝑜) ⊆ 𝑧))
5958elrab 3519 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ↔ (𝑧 ∈ 𝒫 𝑋 ∧ (𝑋𝑜) ⊆ 𝑧))
6059simprbi 490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} → (𝑋𝑜) ⊆ 𝑧)
6160ad2antll 720 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑋𝑜) ⊆ 𝑧)
62 sslin 3998 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝑜) ⊆ 𝑧 → (𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧))
6361, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧))
64 simprrr 800 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ¬ 𝑜𝐹)
6564adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ¬ 𝑜𝐹)
66 inssdif0 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦𝑋) ⊆ 𝑜 ↔ (𝑦 ∩ (𝑋𝑜)) = ∅)
67 simplll 791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝐹 ∈ (Fil‘𝑋))
68 simprl 787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝑦𝐹)
69 filelss 21935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹) → 𝑦𝑋)
7067, 68, 69syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝑦𝑋)
71 df-ss 3746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦𝑋 ↔ (𝑦𝑋) = 𝑦)
7270, 71sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑋) = 𝑦)
7372sseq1d 3792 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦𝑋) ⊆ 𝑜𝑦𝑜))
7430ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝐹 ∈ (Fil‘𝑋))
75 simplrl 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑦𝐹)
76 elssuni 4625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑜𝐽𝑜 𝐽)
7776, 3syl6sseqr 3812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑜𝐽𝑜𝑋)
7877ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑜𝑋)
7978ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑜𝑋)
80 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑦𝑜)
81 filss 21936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑜𝑋𝑦𝑜)) → 𝑜𝐹)
8274, 75, 79, 80, 81syl13anc 1491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑜𝐹)
8382ex 401 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑜𝑜𝐹))
8473, 83sylbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦𝑋) ⊆ 𝑜𝑜𝐹))
8566, 84syl5bir 234 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦 ∩ (𝑋𝑜)) = ∅ → 𝑜𝐹))
8685necon3bd 2951 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (¬ 𝑜𝐹 → (𝑦 ∩ (𝑋𝑜)) ≠ ∅))
8765, 86mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋𝑜)) ≠ ∅)
88 ssn0 4138 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧) ∧ (𝑦 ∩ (𝑋𝑜)) ≠ ∅) → (𝑦𝑧) ≠ ∅)
8963, 87, 88syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑧) ≠ ∅)
9089ralrimivva 3118 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅)
91 filfbas 21931 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
9230, 91syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ∈ (fBas‘𝑋))
9347a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ⊆ 𝑋)
94 filtop 21938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
9530, 94syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑋𝐹)
96 eleq1 2832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑜 = 𝑋 → (𝑜𝐹𝑋𝐹))
9795, 96syl5ibrcom 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑜 = 𝑋𝑜𝐹))
9897necon3bd 2951 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (¬ 𝑜𝐹𝑜𝑋))
9964, 98mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑜𝑋)
100 pssdifn0 4108 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑜𝑋𝑜𝑋) → (𝑋𝑜) ≠ ∅)
10178, 99, 100syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ≠ ∅)
102 supfil 21978 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝐽 ∧ (𝑋𝑜) ⊆ 𝑋 ∧ (𝑋𝑜) ≠ ∅) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
10333, 93, 101, 102syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
104 filfbas 21931 . . . . . . . . . . . . . . . . . . . . . . . 24 ({𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
105103, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
106 fbunfip 21952 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ↔ ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅))
10792, 105, 106syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ↔ ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅))
10890, 107mpbird 248 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
109 fsubbas 21950 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋𝐹 → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
11095, 109syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
11145, 57, 108, 110mpbir3and 1442 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋))
112 ssfg 21955 . . . . . . . . . . . . . . . . . . . 20 ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
113111, 112syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
11440, 113sstrd 3771 . . . . . . . . . . . . . . . . . 18 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
115114unssad 3952 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
116 fgcl 21961 . . . . . . . . . . . . . . . . . . 19 ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
117111, 116syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
118 sseq2 3787 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → (𝐹𝑔𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
119 oveq2 6850 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → (𝐽 fClus 𝑔) = (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
120119eleq2d 2830 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))))
121118, 120imbi12d 335 . . . . . . . . . . . . . . . . . . 19 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → ((𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))))
122121rspcv 3457 . . . . . . . . . . . . . . . . . 18 ((𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))))
123117, 122syl 17 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))))
124115, 123mpid 44 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))))
125 simpr 477 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
126 simplrl 795 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → 𝑜𝐽)
127 simprrl 799 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐴𝑜)
128127adantr 472 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → 𝐴𝑜)
129114, 56sseldd 3762 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
130129adantr 472 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
131 fclsopni 22098 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))) ∧ (𝑜𝐽𝐴𝑜 ∧ (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅)
132125, 126, 128, 130, 131syl13anc 1491 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅)
133132ex 401 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅))
134124, 133syld 47 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅))
135134necon2bd 2953 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ((𝑜 ∩ (𝑋𝑜)) = ∅ → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔))))
13629, 135mpi 20 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
137136anassrs 459 . . . . . . . . . . . 12 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹)) → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
138137expr 448 . . . . . . . . . . 11 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) ∧ 𝐴𝑜) → (¬ 𝑜𝐹 → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔))))
139138con4d 115 . . . . . . . . . 10 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) ∧ 𝐴𝑜) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝑜𝐹))
140139ex 401 . . . . . . . . 9 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) → (𝐴𝑜 → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝑜𝐹)))
141140com23 86 . . . . . . . 8 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴𝑜𝑜𝐹)))
142141ralrimdva 3116 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → ∀𝑜𝐽 (𝐴𝑜𝑜𝐹)))
143 simprr 789 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐴𝑋)
144142, 143jctild 521 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜𝑜𝐹))))
145 simprl 787 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐽 ∈ Top)
146145, 4sylib 209 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
147 simpl 474 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐹 ∈ (Fil‘𝑋))
148 flimopn 22058 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜𝑜𝐹))))
149146, 147, 148syl2anc 579 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜𝑜𝐹))))
150144, 149sylibrd 250 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹)))
151150ex 401 . . . 4 (𝐹 ∈ (Fil‘𝑋) → ((𝐽 ∈ Top ∧ 𝐴𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹))))
152151com23 86 . . 3 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → ((𝐽 ∈ Top ∧ 𝐴𝑋) → 𝐴 ∈ (𝐽 fLim 𝐹))))
15328, 152mpdd 43 . 2 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹)))
15415, 153impbid2 217 1 (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  {crab 3059  Vcvv 3350  cdif 3729  cun 3730  cin 3731  wss 3732  c0 4079  𝒫 cpw 4315   cuni 4594  cfv 6068  (class class class)co 6842  ficfi 8523  fBascfbas 20007  filGencfg 20008  Topctop 20977  TopOnctopon 20994  Filcfil 21928   fLim cflim 22017   fClus cfcls 22019
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-en 8161  df-fin 8164  df-fi 8524  df-fbas 20016  df-fg 20017  df-top 20978  df-topon 20995  df-cld 21103  df-ntr 21104  df-cls 21105  df-nei 21182  df-fil 21929  df-flim 22022  df-fcls 22024
This theorem is referenced by:  cnpfcf  22124
  Copyright terms: Public domain W3C validator