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

Theorem flimfnfcls 24036
Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 24035, 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 24034 . . . . 5 (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔)
2 flimtop 23973 . . . . . . . . 9 (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ Top)
3 flimfnfcls.x . . . . . . . . . 10 𝑋 = 𝐽
43toptopon 22923 . . . . . . . . 9 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
52, 4sylib 218 . . . . . . . 8 (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ (TopOn‘𝑋))
65ad2antrr 726 . . . . . . 7 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐽 ∈ (TopOn‘𝑋))
7 simplr 769 . . . . . . 7 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝑔 ∈ (Fil‘𝑋))
8 simpr 484 . . . . . . 7 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐹𝑔)
9 flimss2 23980 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑔 ∈ (Fil‘𝑋) ∧ 𝐹𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
106, 7, 8, 9syl3anc 1373 . . . . . 6 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
11 simpll 767 . . . . . 6 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fLim 𝐹))
1210, 11sseldd 3984 . . . . 5 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fLim 𝑔))
131, 12sselid 3981 . . . 4 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fClus 𝑔))
1413ex 412 . . 3 ((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) → (𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
1514ralrimiva 3146 . 2 (𝐴 ∈ (𝐽 fLim 𝐹) → ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
16 sseq2 4010 . . . . . 6 (𝑔 = 𝐹 → (𝐹𝑔𝐹𝐹))
17 oveq2 7439 . . . . . . 7 (𝑔 = 𝐹 → (𝐽 fClus 𝑔) = (𝐽 fClus 𝐹))
1817eleq2d 2827 . . . . . 6 (𝑔 = 𝐹 → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus 𝐹)))
1916, 18imbi12d 344 . . . . 5 (𝑔 = 𝐹 → ((𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹))))
2019rspcv 3618 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹))))
21 ssid 4006 . . . . . 6 𝐹𝐹
22 id 22 . . . . . 6 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)))
2321, 22mpi 20 . . . . 5 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ (𝐽 fClus 𝐹))
24 fclstop 24019 . . . . . 6 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
253fclselbas 24024 . . . . . 6 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴𝑋)
2624, 25jca 511 . . . . 5 (𝐴 ∈ (𝐽 fClus 𝐹) → (𝐽 ∈ Top ∧ 𝐴𝑋))
2723, 26syl 17 . . . 4 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐽 ∈ Top ∧ 𝐴𝑋))
2820, 27syl6 35 . . 3 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐽 ∈ Top ∧ 𝐴𝑋)))
29 disjdif 4472 . . . . . . . . . . . . . 14 (𝑜 ∩ (𝑋𝑜)) = ∅
30 simpll 767 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ∈ (Fil‘𝑋))
31 simplrl 777 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐽 ∈ Top)
323topopn 22912 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 ∈ Top → 𝑋𝐽)
3331, 32syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑋𝐽)
34 pwexg 5378 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋𝐽 → 𝒫 𝑋 ∈ V)
35 rabexg 5337 . . . . . . . . . . . . . . . . . . . . . 22 (𝒫 𝑋 ∈ V → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V)
3633, 34, 353syl 18 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V)
37 unexg 7763 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V)
3830, 36, 37syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V)
39 ssfii 9459 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
4038, 39syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
41 filsspw 23859 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
42 ssrab2 4080 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋
4342a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋)
4441, 43unssd 4192 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
4544ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
46 ssun2 4179 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})
47 sseq2 4010 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑋𝑜) → ((𝑋𝑜) ⊆ 𝑥 ↔ (𝑋𝑜) ⊆ (𝑋𝑜)))
48 difss 4136 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋𝑜) ⊆ 𝑋
49 elpw2g 5333 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑋𝐽 → ((𝑋𝑜) ∈ 𝒫 𝑋 ↔ (𝑋𝑜) ⊆ 𝑋))
5033, 49syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ((𝑋𝑜) ∈ 𝒫 𝑋 ↔ (𝑋𝑜) ⊆ 𝑋))
5148, 50mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ 𝒫 𝑋)
52 ssid 4006 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋𝑜) ⊆ (𝑋𝑜)
5352a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ⊆ (𝑋𝑜))
5447, 51, 53elrabd 3694 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})
5546, 54sselid 3981 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))
5655ne0d 4342 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅)
57 sseq2 4010 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝑧 → ((𝑋𝑜) ⊆ 𝑥 ↔ (𝑋𝑜) ⊆ 𝑧))
5857elrab 3692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ↔ (𝑧 ∈ 𝒫 𝑋 ∧ (𝑋𝑜) ⊆ 𝑧))
5958simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} → (𝑋𝑜) ⊆ 𝑧)
6059ad2antll 729 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑋𝑜) ⊆ 𝑧)
61 sslin 4243 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝑜) ⊆ 𝑧 → (𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧))
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧))
63 simprrr 782 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ¬ 𝑜𝐹)
6463adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ¬ 𝑜𝐹)
65 inssdif0 4374 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦𝑋) ⊆ 𝑜 ↔ (𝑦 ∩ (𝑋𝑜)) = ∅)
66 simplll 775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝐹 ∈ (Fil‘𝑋))
67 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝑦𝐹)
68 filelss 23860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹) → 𝑦𝑋)
6966, 67, 68syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝑦𝑋)
70 dfss2 3969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦𝑋 ↔ (𝑦𝑋) = 𝑦)
7169, 70sylib 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑋) = 𝑦)
7271sseq1d 4015 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦𝑋) ⊆ 𝑜𝑦𝑜))
7330ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝐹 ∈ (Fil‘𝑋))
74 simplrl 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑦𝐹)
75 elssuni 4937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑜𝐽𝑜 𝐽)
7675, 3sseqtrrdi 4025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑜𝐽𝑜𝑋)
7776ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑜𝑋)
7877ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑜𝑋)
79 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑦𝑜)
80 filss 23861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑜𝑋𝑦𝑜)) → 𝑜𝐹)
8173, 74, 78, 79, 80syl13anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑜𝐹)
8281ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑜𝑜𝐹))
8372, 82sylbid 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦𝑋) ⊆ 𝑜𝑜𝐹))
8465, 83biimtrrid 243 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦 ∩ (𝑋𝑜)) = ∅ → 𝑜𝐹))
8584necon3bd 2954 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (¬ 𝑜𝐹 → (𝑦 ∩ (𝑋𝑜)) ≠ ∅))
8664, 85mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋𝑜)) ≠ ∅)
87 ssn0 4404 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧) ∧ (𝑦 ∩ (𝑋𝑜)) ≠ ∅) → (𝑦𝑧) ≠ ∅)
8862, 86, 87syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑧) ≠ ∅)
8988ralrimivva 3202 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅)
90 filfbas 23856 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
9130, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ∈ (fBas‘𝑋))
9248a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ⊆ 𝑋)
93 filtop 23863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
9430, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑋𝐹)
95 eleq1 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑜 = 𝑋 → (𝑜𝐹𝑋𝐹))
9694, 95syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑜 = 𝑋𝑜𝐹))
9796necon3bd 2954 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (¬ 𝑜𝐹𝑜𝑋))
9863, 97mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑜𝑋)
99 pssdifn0 4368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑜𝑋𝑜𝑋) → (𝑋𝑜) ≠ ∅)
10077, 98, 99syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ≠ ∅)
101 supfil 23903 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝐽 ∧ (𝑋𝑜) ⊆ 𝑋 ∧ (𝑋𝑜) ≠ ∅) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
10233, 92, 100, 101syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
103 filfbas 23856 . . . . . . . . . . . . . . . . . . . . . . . 24 ({𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
105 fbunfip 23877 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ↔ ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅))
10691, 104, 105syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ↔ ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅))
10789, 106mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
108 fsubbas 23875 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋𝐹 → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
10994, 108syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
11045, 56, 107, 109mpbir3and 1343 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋))
111 ssfg 23880 . . . . . . . . . . . . . . . . . . . 20 ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
112110, 111syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
11340, 112sstrd 3994 . . . . . . . . . . . . . . . . . 18 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
114113unssad 4193 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
115 fgcl 23886 . . . . . . . . . . . . . . . . . . 19 ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
116110, 115syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
117 sseq2 4010 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → (𝐹𝑔𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
118 oveq2 7439 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → (𝐽 fClus 𝑔) = (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
119118eleq2d 2827 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))))
120117, 119imbi12d 344 . . . . . . . . . . . . . . . . . . 19 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → ((𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))))
121120rspcv 3618 . . . . . . . . . . . . . . . . . 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 484 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
125 simplrl 777 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → 𝑜𝐽)
126 simprrl 781 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐴𝑜)
127126adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → 𝐴𝑜)
128113, 55sseldd 3984 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
129128adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
130 fclsopni 24023 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))) ∧ (𝑜𝐽𝐴𝑜 ∧ (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅)
131124, 125, 127, 129, 130syl13anc 1374 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅)
132131ex 412 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅))
133123, 132syld 47 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅))
134133necon2bd 2956 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ((𝑜 ∩ (𝑋𝑜)) = ∅ → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔))))
13529, 134mpi 20 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
136135anassrs 467 . . . . . . . . . . . 12 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹)) → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
137136expr 456 . . . . . . . . . . 11 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) ∧ 𝐴𝑜) → (¬ 𝑜𝐹 → ¬ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔))))
138137con4d 115 . . . . . . . . . 10 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) ∧ 𝐴𝑜) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝑜𝐹))
139138ex 412 . . . . . . . . 9 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) → (𝐴𝑜 → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝑜𝐹)))
140139com23 86 . . . . . . . 8 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ 𝑜𝐽) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴𝑜𝑜𝐹)))
141140ralrimdva 3154 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → ∀𝑜𝐽 (𝐴𝑜𝑜𝐹)))
142 simprr 773 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐴𝑋)
143141, 142jctild 525 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜𝑜𝐹))))
144 simprl 771 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐽 ∈ Top)
145144, 4sylib 218 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
146 simpl 482 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → 𝐹 ∈ (Fil‘𝑋))
147 flimopn 23983 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜𝑜𝐹))))
148145, 146, 147syl2anc 584 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴𝑋 ∧ ∀𝑜𝐽 (𝐴𝑜𝑜𝐹))))
149143, 148sylibrd 259 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹)))
150149ex 412 . . . 4 (𝐹 ∈ (Fil‘𝑋) → ((𝐽 ∈ Top ∧ 𝐴𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹))))
151150com23 86 . . 3 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → ((𝐽 ∈ Top ∧ 𝐴𝑋) → 𝐴 ∈ (𝐽 fLim 𝐹))))
15228, 151mpdd 43 . 2 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → 𝐴 ∈ (𝐽 fLim 𝐹)))
15315, 152impbid2 226 1 (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wral 3061  {crab 3436  Vcvv 3480  cdif 3948  cun 3949  cin 3950  wss 3951  c0 4333  𝒫 cpw 4600   cuni 4907  cfv 6561  (class class class)co 7431  ficfi 9450  fBascfbas 21352  filGencfg 21353  Topctop 22899  TopOnctopon 22916  Filcfil 23853   fLim cflim 23942   fClus cfcls 23944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1o 8506  df-2o 8507  df-en 8986  df-fin 8989  df-fi 9451  df-fbas 21361  df-fg 21362  df-top 22900  df-topon 22917  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-fil 23854  df-flim 23947  df-fcls 23949
This theorem is referenced by:  cnpfcf  24049
  Copyright terms: Public domain W3C validator