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

Theorem flimfnfcls 22552
Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 22551, 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 22550 . . . . 5 (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔)
2 flimtop 22489 . . . . . . . . 9 (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ Top)
3 flimfnfcls.x . . . . . . . . . 10 𝑋 = 𝐽
43toptopon 21441 . . . . . . . . 9 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
52, 4sylib 219 . . . . . . . 8 (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ (TopOn‘𝑋))
65ad2antrr 722 . . . . . . 7 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐽 ∈ (TopOn‘𝑋))
7 simplr 765 . . . . . . 7 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝑔 ∈ (Fil‘𝑋))
8 simpr 485 . . . . . . 7 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐹𝑔)
9 flimss2 22496 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑔 ∈ (Fil‘𝑋) ∧ 𝐹𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
106, 7, 8, 9syl3anc 1365 . . . . . 6 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
11 simpll 763 . . . . . 6 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fLim 𝐹))
1210, 11sseldd 3972 . . . . 5 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fLim 𝑔))
131, 12sseldi 3969 . . . 4 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fClus 𝑔))
1413ex 413 . . 3 ((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) → (𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
1514ralrimiva 3187 . 2 (𝐴 ∈ (𝐽 fLim 𝐹) → ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
16 sseq2 3997 . . . . . 6 (𝑔 = 𝐹 → (𝐹𝑔𝐹𝐹))
17 oveq2 7156 . . . . . . 7 (𝑔 = 𝐹 → (𝐽 fClus 𝑔) = (𝐽 fClus 𝐹))
1817eleq2d 2903 . . . . . 6 (𝑔 = 𝐹 → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus 𝐹)))
1916, 18imbi12d 346 . . . . 5 (𝑔 = 𝐹 → ((𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹))))
2019rspcv 3622 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹))))
21 ssid 3993 . . . . . 6 𝐹𝐹
22 id 22 . . . . . 6 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)))
2321, 22mpi 20 . . . . 5 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ (𝐽 fClus 𝐹))
24 fclstop 22535 . . . . . 6 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
253fclselbas 22540 . . . . . 6 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴𝑋)
2624, 25jca 512 . . . . 5 (𝐴 ∈ (𝐽 fClus 𝐹) → (𝐽 ∈ Top ∧ 𝐴𝑋))
2723, 26syl 17 . . . 4 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐽 ∈ Top ∧ 𝐴𝑋))
2820, 27syl6 35 . . 3 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐽 ∈ Top ∧ 𝐴𝑋)))
29 disjdif 4424 . . . . . . . . . . . . . 14 (𝑜 ∩ (𝑋𝑜)) = ∅
30 simpll 763 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ∈ (Fil‘𝑋))
31 simplrl 773 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐽 ∈ Top)
323topopn 21430 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 ∈ Top → 𝑋𝐽)
3331, 32syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑋𝐽)
34 pwexg 5276 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋𝐽 → 𝒫 𝑋 ∈ V)
35 rabexg 5231 . . . . . . . . . . . . . . . . . . . . . 22 (𝒫 𝑋 ∈ V → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V)
3633, 34, 353syl 18 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V)
37 unexg 7461 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V)
3830, 36, 37syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V)
39 ssfii 8872 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
4038, 39syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
41 filsspw 22375 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
42 ssrab2 4060 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋
4342a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋)
4441, 43unssd 4166 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
4544ad2antrr 722 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
46 ssun2 4153 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})
47 sseq2 3997 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑋𝑜) → ((𝑋𝑜) ⊆ 𝑥 ↔ (𝑋𝑜) ⊆ (𝑋𝑜)))
48 difss 4112 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋𝑜) ⊆ 𝑋
49 elpw2g 5244 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑋𝐽 → ((𝑋𝑜) ∈ 𝒫 𝑋 ↔ (𝑋𝑜) ⊆ 𝑋))
5033, 49syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ((𝑋𝑜) ∈ 𝒫 𝑋 ↔ (𝑋𝑜) ⊆ 𝑋))
5148, 50mpbiri 259 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ 𝒫 𝑋)
52 ssid 3993 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋𝑜) ⊆ (𝑋𝑜)
5352a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ⊆ (𝑋𝑜))
5447, 51, 53elrabd 3686 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})
5546, 54sseldi 3969 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))
5655ne0d 4305 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅)
57 sseq2 3997 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝑧 → ((𝑋𝑜) ⊆ 𝑥 ↔ (𝑋𝑜) ⊆ 𝑧))
5857elrab 3684 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ↔ (𝑧 ∈ 𝒫 𝑋 ∧ (𝑋𝑜) ⊆ 𝑧))
5958simprbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} → (𝑋𝑜) ⊆ 𝑧)
6059ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑋𝑜) ⊆ 𝑧)
61 sslin 4215 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝑜) ⊆ 𝑧 → (𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧))
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧))
63 simprrr 778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ¬ 𝑜𝐹)
6463adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ¬ 𝑜𝐹)
65 inssdif0 4333 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦𝑋) ⊆ 𝑜 ↔ (𝑦 ∩ (𝑋𝑜)) = ∅)
66 simplll 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝐹 ∈ (Fil‘𝑋))
67 simprl 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝑦𝐹)
68 filelss 22376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹) → 𝑦𝑋)
6966, 67, 68syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝑦𝑋)
70 df-ss 3956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦𝑋 ↔ (𝑦𝑋) = 𝑦)
7169, 70sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑋) = 𝑦)
7271sseq1d 4002 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦𝑋) ⊆ 𝑜𝑦𝑜))
7330ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝐹 ∈ (Fil‘𝑋))
74 simplrl 773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑦𝐹)
75 elssuni 4866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑜𝐽𝑜 𝐽)
7675, 3sseqtrrdi 4022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑜𝐽𝑜𝑋)
7776ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑜𝑋)
7877ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑜𝑋)
79 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑦𝑜)
80 filss 22377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑜𝑋𝑦𝑜)) → 𝑜𝐹)
8173, 74, 78, 79, 80syl13anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑜𝐹)
8281ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑜𝑜𝐹))
8372, 82sylbid 241 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦𝑋) ⊆ 𝑜𝑜𝐹))
8465, 83syl5bir 244 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦 ∩ (𝑋𝑜)) = ∅ → 𝑜𝐹))
8584necon3bd 3035 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (¬ 𝑜𝐹 → (𝑦 ∩ (𝑋𝑜)) ≠ ∅))
8664, 85mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋𝑜)) ≠ ∅)
87 ssn0 4358 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧) ∧ (𝑦 ∩ (𝑋𝑜)) ≠ ∅) → (𝑦𝑧) ≠ ∅)
8862, 86, 87syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑧) ≠ ∅)
8988ralrimivva 3196 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅)
90 filfbas 22372 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
9130, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ∈ (fBas‘𝑋))
9248a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ⊆ 𝑋)
93 filtop 22379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
9430, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑋𝐹)
95 eleq1 2905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑜 = 𝑋 → (𝑜𝐹𝑋𝐹))
9694, 95syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑜 = 𝑋𝑜𝐹))
9796necon3bd 3035 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (¬ 𝑜𝐹𝑜𝑋))
9863, 97mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑜𝑋)
99 pssdifn0 4329 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑜𝑋𝑜𝑋) → (𝑋𝑜) ≠ ∅)
10077, 98, 99syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ≠ ∅)
101 supfil 22419 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝐽 ∧ (𝑋𝑜) ⊆ 𝑋 ∧ (𝑋𝑜) ≠ ∅) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
10233, 92, 100, 101syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
103 filfbas 22372 . . . . . . . . . . . . . . . . . . . . . . . 24 ({𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
105 fbunfip 22393 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ↔ ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅))
10691, 104, 105syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ↔ ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅))
10789, 106mpbird 258 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
108 fsubbas 22391 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋𝐹 → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
10994, 108syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
11045, 56, 107, 109mpbir3and 1336 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋))
111 ssfg 22396 . . . . . . . . . . . . . . . . . . . 20 ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
112110, 111syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
11340, 112sstrd 3981 . . . . . . . . . . . . . . . . . 18 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
114113unssad 4167 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
115 fgcl 22402 . . . . . . . . . . . . . . . . . . 19 ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
116110, 115syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
117 sseq2 3997 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → (𝐹𝑔𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
118 oveq2 7156 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → (𝐽 fClus 𝑔) = (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
119118eleq2d 2903 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))))
120117, 119imbi12d 346 . . . . . . . . . . . . . . . . . . 19 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → ((𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))))
121120rspcv 3622 . . . . . . . . . . . . . . . . . 18 ((𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))))
122116, 121syl 17 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))))
123114, 122mpid 44 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))))
124 simpr 485 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
125 simplrl 773 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → 𝑜𝐽)
126 simprrl 777 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐴𝑜)
127126adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → 𝐴𝑜)
128113, 55sseldd 3972 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
129128adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
130 fclsopni 22539 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))) ∧ (𝑜𝐽𝐴𝑜 ∧ (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅)
131124, 125, 127, 129, 130syl13anc 1366 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅)
132131ex 413 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅))
133123, 132syld 47 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅))
134133necon2bd 3037 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ((𝑜 ∩ (𝑋𝑜)) = ∅ → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔))))
13529, 134mpi 20 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
136135anassrs 468 . . . . . . . . . . . 12 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹)) → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
137136expr 457 . . . . . . . . . . 11 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) ∧ 𝐴𝑜) → (¬ 𝑜𝐹 → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔))))
138137con4d 115 . . . . . . . . . 10 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) ∧ 𝐴𝑜) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝑜𝐹))
139138ex 413 . . . . . . . . 9 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) → (𝐴𝑜 → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝑜𝐹)))
140139com23 86 . . . . . . . 8 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴𝑜𝑜𝐹)))
141140ralrimdva 3194 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → ∀𝑜𝐽 (𝐴𝑜𝑜𝐹)))
142 simprr 769 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐴𝑋)
143141, 142jctild 526 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜𝑜𝐹))))
144 simprl 767 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐽 ∈ Top)
145144, 4sylib 219 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
146 simpl 483 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐹 ∈ (Fil‘𝑋))
147 flimopn 22499 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜𝑜𝐹))))
148145, 146, 147syl2anc 584 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜𝑜𝐹))))
149143, 148sylibrd 260 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹)))
150149ex 413 . . . 4 (𝐹 ∈ (Fil‘𝑋) → ((𝐽 ∈ Top ∧ 𝐴𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹))))
151150com23 86 . . 3 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → ((𝐽 ∈ Top ∧ 𝐴𝑋) → 𝐴 ∈ (𝐽 fLim 𝐹))))
15228, 151mpdd 43 . 2 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹)))
15315, 152impbid2 227 1 (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2107  wne 3021  wral 3143  {crab 3147  Vcvv 3500  cdif 3937  cun 3938  cin 3939  wss 3940  c0 4295  𝒫 cpw 4542   cuni 4837  cfv 6352  (class class class)co 7148  ficfi 8863  fBascfbas 20449  filGencfg 20450  Topctop 21417  TopOnctopon 21434  Filcfil 22369   fLim cflim 22458   fClus cfcls 22460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-iin 4920  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-oadd 8097  df-er 8279  df-en 8499  df-fin 8502  df-fi 8864  df-fbas 20458  df-fg 20459  df-top 21418  df-topon 21435  df-cld 21543  df-ntr 21544  df-cls 21545  df-nei 21622  df-fil 22370  df-flim 22463  df-fcls 22465
This theorem is referenced by:  cnpfcf  22565
  Copyright terms: Public domain W3C validator