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

Theorem flimfnfcls 24052
Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 24051, 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 24050 . . . . 5 (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔)
2 flimtop 23989 . . . . . . . . 9 (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ Top)
3 flimfnfcls.x . . . . . . . . . 10 𝑋 = 𝐽
43toptopon 22939 . . . . . . . . 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 23996 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑔 ∈ (Fil‘𝑋) ∧ 𝐹𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
106, 7, 8, 9syl3anc 1370 . . . . . 6 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → (𝐽 fLim 𝐹) ⊆ (𝐽 fLim 𝑔))
11 simpll 767 . . . . . 6 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fLim 𝐹))
1210, 11sseldd 3996 . . . . 5 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fLim 𝑔))
131, 12sselid 3993 . . . 4 (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) ∧ 𝐹𝑔) → 𝐴 ∈ (𝐽 fClus 𝑔))
1413ex 412 . . 3 ((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑔 ∈ (Fil‘𝑋)) → (𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
1514ralrimiva 3144 . 2 (𝐴 ∈ (𝐽 fLim 𝐹) → ∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)))
16 sseq2 4022 . . . . . 6 (𝑔 = 𝐹 → (𝐹𝑔𝐹𝐹))
17 oveq2 7439 . . . . . . 7 (𝑔 = 𝐹 → (𝐽 fClus 𝑔) = (𝐽 fClus 𝐹))
1817eleq2d 2825 . . . . . 6 (𝑔 = 𝐹 → (𝐴 ∈ (𝐽 fClus 𝑔) ↔ 𝐴 ∈ (𝐽 fClus 𝐹)))
1916, 18imbi12d 344 . . . . 5 (𝑔 = 𝐹 → ((𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) ↔ (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹))))
2019rspcv 3618 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹))))
21 ssid 4018 . . . . . 6 𝐹𝐹
22 id 22 . . . . . 6 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)))
2321, 22mpi 20 . . . . 5 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ (𝐽 fClus 𝐹))
24 fclstop 24035 . . . . . 6 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
253fclselbas 24040 . . . . . 6 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴𝑋)
2624, 25jca 511 . . . . 5 (𝐴 ∈ (𝐽 fClus 𝐹) → (𝐽 ∈ Top ∧ 𝐴𝑋))
2723, 26syl 17 . . . 4 ((𝐹𝐹𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐽 ∈ Top ∧ 𝐴𝑋))
2820, 27syl6 35 . . 3 (𝐹 ∈ (Fil‘𝑋) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝐽 ∈ Top ∧ 𝐴𝑋)))
29 disjdif 4478 . . . . . . . . . . . . . 14 (𝑜 ∩ (𝑋𝑜)) = ∅
30 simpll 767 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ∈ (Fil‘𝑋))
31 simplrl 777 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐽 ∈ Top)
323topopn 22928 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 ∈ Top → 𝑋𝐽)
3331, 32syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑋𝐽)
34 pwexg 5384 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋𝐽 → 𝒫 𝑋 ∈ V)
35 rabexg 5343 . . . . . . . . . . . . . . . . . . . . . 22 (𝒫 𝑋 ∈ V → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V)
3633, 34, 353syl 18 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V)
37 unexg 7762 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (Fil‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ V) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V)
3830, 36, 37syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V)
39 ssfii 9457 . . . . . . . . . . . . . . . . . . . 20 ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ∈ V → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
4038, 39syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
41 filsspw 23875 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
42 ssrab2 4090 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋
4342a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ 𝒫 𝑋)
4441, 43unssd 4202 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
4544ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋)
46 ssun2 4189 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ⊆ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})
47 sseq2 4022 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝑋𝑜) → ((𝑋𝑜) ⊆ 𝑥 ↔ (𝑋𝑜) ⊆ (𝑋𝑜)))
48 difss 4146 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋𝑜) ⊆ 𝑋
49 elpw2g 5339 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑋𝐽 → ((𝑋𝑜) ∈ 𝒫 𝑋 ↔ (𝑋𝑜) ⊆ 𝑋))
5033, 49syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ((𝑋𝑜) ∈ 𝒫 𝑋 ↔ (𝑋𝑜) ⊆ 𝑋))
5148, 50mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ 𝒫 𝑋)
52 ssid 4018 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋𝑜) ⊆ (𝑋𝑜)
5352a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ⊆ (𝑋𝑜))
5447, 51, 53elrabd 3697 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})
5546, 54sselid 3993 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))
5655ne0d 4348 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅)
57 sseq2 4022 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝑧 → ((𝑋𝑜) ⊆ 𝑥 ↔ (𝑋𝑜) ⊆ 𝑧))
5857elrab 3695 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ↔ (𝑧 ∈ 𝒫 𝑋 ∧ (𝑋𝑜) ⊆ 𝑧))
5958simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} → (𝑋𝑜) ⊆ 𝑧)
6059ad2antll 729 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑋𝑜) ⊆ 𝑧)
61 sslin 4251 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝑜) ⊆ 𝑧 → (𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧))
6260, 61syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧))
63 simprrr 782 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ¬ 𝑜𝐹)
6463adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ¬ 𝑜𝐹)
65 inssdif0 4380 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦𝑋) ⊆ 𝑜 ↔ (𝑦 ∩ (𝑋𝑜)) = ∅)
66 simplll 775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝐹 ∈ (Fil‘𝑋))
67 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝑦𝐹)
68 filelss 23876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹) → 𝑦𝑋)
6966, 67, 68syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → 𝑦𝑋)
70 dfss2 3981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦𝑋 ↔ (𝑦𝑋) = 𝑦)
7169, 70sylib 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑋) = 𝑦)
7271sseq1d 4027 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦𝑋) ⊆ 𝑜𝑦𝑜))
7330ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝐹 ∈ (Fil‘𝑋))
74 simplrl 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑦𝐹)
75 elssuni 4942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑜𝐽𝑜 𝐽)
7675, 3sseqtrrdi 4047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑜𝐽𝑜𝑋)
7776ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑜𝑋)
7877ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑜𝑋)
79 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑦𝑜)
80 filss 23877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑜𝑋𝑦𝑜)) → 𝑜𝐹)
8173, 74, 78, 79, 80syl13anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∧ 𝑦𝑜) → 𝑜𝐹)
8281ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑜𝑜𝐹))
8372, 82sylbid 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦𝑋) ⊆ 𝑜𝑜𝐹))
8465, 83biimtrrid 243 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → ((𝑦 ∩ (𝑋𝑜)) = ∅ → 𝑜𝐹))
8584necon3bd 2952 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (¬ 𝑜𝐹 → (𝑦 ∩ (𝑋𝑜)) ≠ ∅))
8664, 85mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦 ∩ (𝑋𝑜)) ≠ ∅)
87 ssn0 4410 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∩ (𝑋𝑜)) ⊆ (𝑦𝑧) ∧ (𝑦 ∩ (𝑋𝑜)) ≠ ∅) → (𝑦𝑧) ≠ ∅)
8862, 86, 87syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ (𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) → (𝑦𝑧) ≠ ∅)
8988ralrimivva 3200 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅)
90 filfbas 23872 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
9130, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ∈ (fBas‘𝑋))
9248a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ⊆ 𝑋)
93 filtop 23879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
9430, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑋𝐹)
95 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑜 = 𝑋 → (𝑜𝐹𝑋𝐹))
9694, 95syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑜 = 𝑋𝑜𝐹))
9796necon3bd 2952 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (¬ 𝑜𝐹𝑜𝑋))
9863, 97mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝑜𝑋)
99 pssdifn0 4374 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑜𝑋𝑜𝑋) → (𝑋𝑜) ≠ ∅)
10077, 98, 99syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ≠ ∅)
101 supfil 23919 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋𝐽 ∧ (𝑋𝑜) ⊆ 𝑋 ∧ (𝑋𝑜) ≠ ∅) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
10233, 92, 100, 101syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋))
103 filfbas 23872 . . . . . . . . . . . . . . . . . . . . . . . 24 ({𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (Fil‘𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋))
105 fbunfip 23893 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ↔ ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅))
10691, 104, 105syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ↔ ∀𝑦𝐹𝑧 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥} (𝑦𝑧) ≠ ∅))
10789, 106mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))
108 fsubbas 23891 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋𝐹 → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
10994, 108syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
11045, 56, 107, 109mpbir3and 1341 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋))
111 ssfg 23896 . . . . . . . . . . . . . . . . . . . 20 ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
112110, 111syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
11340, 112sstrd 4006 . . . . . . . . . . . . . . . . . 18 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
114113unssad 4203 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
115 fgcl 23902 . . . . . . . . . . . . . . . . . . 19 ((fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
116110, 115syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) ∈ (Fil‘𝑋))
117 sseq2 4022 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → (𝐹𝑔𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
118 oveq2 7439 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))) → (𝐽 fClus 𝑔) = (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))))
119118eleq2d 2825 . . . . . . . . . . . . . . . . . . . 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 3996 . . . . . . . . . . . . . . . . . . 19 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
129128adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))
130 fclsopni 24039 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))) ∧ (𝑜𝐽𝐴𝑜 ∧ (𝑋𝑜) ∈ (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅)
131124, 125, 127, 129, 130syl13anc 1371 . . . . . . . . . . . . . . . . 17 ((((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) ∧ 𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥}))))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅)
132131ex 412 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (𝐴 ∈ (𝐽 fClus (𝑋filGen(fi‘(𝐹 ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋𝑜) ⊆ 𝑥})))) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅))
133123, 132syld 47 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝐽 ∈ Top ∧ 𝐴𝑋)) ∧ (𝑜𝐽 ∧ (𝐴𝑜 ∧ ¬ 𝑜𝐹))) → (∀𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fClus 𝑔)) → (𝑜 ∩ (𝑋𝑜)) ≠ ∅))
134133necon2bd 2954 . . . . . . . . . . . . . 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 3152 . . . . . . 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 23999 . . . . . . 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 1086   = wceq 1537  wcel 2106  wne 2938  wral 3059  {crab 3433  Vcvv 3478  cdif 3960  cun 3961  cin 3962  wss 3963  c0 4339  𝒫 cpw 4605   cuni 4912  cfv 6563  (class class class)co 7431  ficfi 9448  fBascfbas 21370  filGencfg 21371  Topctop 22915  TopOnctopon 22932  Filcfil 23869   fLim cflim 23958   fClus cfcls 23960
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1o 8505  df-2o 8506  df-en 8985  df-fin 8988  df-fi 9449  df-fbas 21379  df-fg 21380  df-top 22916  df-topon 22933  df-cld 23043  df-ntr 23044  df-cls 23045  df-nei 23122  df-fil 23870  df-flim 23963  df-fcls 23965
This theorem is referenced by:  cnpfcf  24065
  Copyright terms: Public domain W3C validator