Theorem fclscf 24008

Description: Characterization of fineness of topologies in terms of cluster points. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)

Assertion

Ref	Expression
fclscf	⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) → (𝐽 ⊆ 𝐾 ↔ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)))

Distinct variable groups:   𝑓,𝐽   𝑓,𝐾   𝑓,𝑋

Proof of Theorem fclscf

Dummy variables 𝑛 𝑢 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 772	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → 𝐽 ∈ (TopOn‘𝑋))
2		simplr 774	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → 𝐾 ∈ (TopOn‘𝑋))
3		fclstopon 23995	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐾 fClus 𝑓) → (𝐾 ∈ (TopOn‘𝑋) ↔ 𝑓 ∈ (Fil‘𝑋)))
4	3	ad2antll 735	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → (𝐾 ∈ (TopOn‘𝑋) ↔ 𝑓 ∈ (Fil‘𝑋)))
5	2, 4	mpbid 233	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → 𝑓 ∈ (Fil‘𝑋))
6		simprl 776	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → 𝐽 ⊆ 𝐾)
7		fclsss1 24005	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓))
8	1, 5, 6, 7	syl3anc 1379	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → (𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓))
9		simprr 778	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → 𝑥 ∈ (𝐾 fClus 𝑓))
10	8, 9	sseldd 3916	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → 𝑥 ∈ (𝐽 fClus 𝑓))
11	10	expr 457	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) → (𝑥 ∈ (𝐾 fClus 𝑓) → 𝑥 ∈ (𝐽 fClus 𝑓)))
12	11	ssrdv 3921	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) → (𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓))
13	12	ralrimivw 3135	. 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) → ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓))
14		simpllr 781	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → 𝐾 ∈ (TopOn‘𝑋))
15		toponmax 22909	. . . . . . . . 9 ⊢ (𝐾 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐾)
16		ssid 3937	. . . . . . . . . . 11 ⊢ 𝑋 ⊆ 𝑋
17		eleq2 2828	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑋 → (𝑦 ∈ 𝑢 ↔ 𝑦 ∈ 𝑋))
18		sseq1 3940	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑋 → (𝑢 ⊆ 𝑋 ↔ 𝑋 ⊆ 𝑋))
19	17, 18	anbi12d 638	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑋 → ((𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋) ↔ (𝑦 ∈ 𝑋 ∧ 𝑋 ⊆ 𝑋)))
20	19	rspcev 3560	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝐾 ∧ (𝑦 ∈ 𝑋 ∧ 𝑋 ⊆ 𝑋)) → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋))
21	16, 20	mpanr2 710	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑦 ∈ 𝑋) → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋))
22	21	ex 413	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝐾 → (𝑦 ∈ 𝑋 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋)))
23	14, 15, 22	3syl 18	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → (𝑦 ∈ 𝑋 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋)))
24		eleq2 2828	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑋))
25		sseq2 3941	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑢 ⊆ 𝑥 ↔ 𝑢 ⊆ 𝑋))
26	25	anbi2d 636	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥) ↔ (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋)))
27	26	rexbidv 3163	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥) ↔ ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋)))
28	24, 27	imbi12d 345	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑦 ∈ 𝑥 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)) ↔ (𝑦 ∈ 𝑋 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋))))
29	23, 28	syl5ibrcom 248	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → (𝑥 = 𝑋 → (𝑦 ∈ 𝑥 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥))))
30		simplll 780	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝐽 ∈ (TopOn‘𝑋))
31		simprl 776	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑥 ∈ 𝐽)
32		simprrr 787	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑦 ∈ 𝑥)
33		supnfcls 24003	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) → ¬ 𝑦 ∈ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
34	30, 31, 32, 33	syl3anc 1379	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → ¬ 𝑦 ∈ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
35		toponss 22910	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝐽) → 𝑥 ⊆ 𝑋)
36	30, 31, 35	syl2anc 590	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑥 ⊆ 𝑋)
37	36, 32	sseldd 3916	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑦 ∈ 𝑋)
38		simpllr 781	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝐾 ∈ (TopOn‘𝑋))
39		toponmax 22909	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽)
40	30, 39	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑋 ∈ 𝐽)
41		difssd 4067	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝑋 ∖ 𝑥) ⊆ 𝑋)
42		simprrl 786	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑥 ≠ 𝑋)
43		pssdifn0 4296	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ⊆ 𝑋 ∧ 𝑥 ≠ 𝑋) → (𝑋 ∖ 𝑥) ≠ ∅)
44	36, 42, 43	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝑋 ∖ 𝑥) ≠ ∅)
45		supfil 23878	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝐽 ∧ (𝑋 ∖ 𝑥) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) ≠ ∅) → {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ∈ (Fil‘𝑋))
46	40, 41, 44, 45	syl3anc 1379	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ∈ (Fil‘𝑋))
47		fclsopn 23997	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ∈ (Fil‘𝑋)) → (𝑦 ∈ (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}) ↔ (𝑦 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅))))
48	38, 46, 47	syl2anc 590	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝑦 ∈ (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}) ↔ (𝑦 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅))))
49	37, 48	mpbirand 713	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝑦 ∈ (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}) ↔ ∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅)))
50		oveq2 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} → (𝐾 fClus 𝑓) = (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
51		oveq2 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} → (𝐽 fClus 𝑓) = (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
52	50, 51	sseq12d 3948	. . . . . . . . . . . . . 14 ⊢ (𝑓 = {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} → ((𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓) ↔ (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}) ⊆ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦})))
53		simplr 774	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓))
54	52, 53, 46	rspcdva 3561	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}) ⊆ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
55	54	sseld 3914	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝑦 ∈ (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}) → 𝑦 ∈ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦})))
56	49, 55	sylbird 261	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅) → 𝑦 ∈ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦})))
57	34, 56	mtod 199	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → ¬ ∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅))
58		rexanali 3093	. . . . . . . . . . 11 ⊢ (∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ ¬ ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅) ↔ ¬ ∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅))
59		rexnal 3091	. . . . . . . . . . . . . 14 ⊢ (∃𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ¬ (𝑢 ∩ 𝑛) ≠ ∅ ↔ ¬ ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅)
60		sseq2 3941	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → ((𝑋 ∖ 𝑥) ⊆ 𝑦 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑛))
61	60	elrab 3629	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ↔ (𝑛 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑥) ⊆ 𝑛))
62		sslin 4171	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∖ 𝑥) ⊆ 𝑛 → (𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛))
63	61, 62	simplbiim 509	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} → (𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛))
64		ssn0 4332	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛) ∧ (𝑢 ∩ (𝑋 ∖ 𝑥)) ≠ ∅) → (𝑢 ∩ 𝑛) ≠ ∅)
65	64	ex 413	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛) → ((𝑢 ∩ (𝑋 ∖ 𝑥)) ≠ ∅ → (𝑢 ∩ 𝑛) ≠ ∅))
66	65	necon1bd 2952	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛) → (¬ (𝑢 ∩ 𝑛) ≠ ∅ → (𝑢 ∩ (𝑋 ∖ 𝑥)) = ∅))
67		inssdif0 4302	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∩ 𝑋) ⊆ 𝑥 ↔ (𝑢 ∩ (𝑋 ∖ 𝑥)) = ∅)
68	66, 67	imbitrrdi 253	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛) → (¬ (𝑢 ∩ 𝑛) ≠ ∅ → (𝑢 ∩ 𝑋) ⊆ 𝑥))
69		toponss 22910	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝑢 ∈ 𝐾) → 𝑢 ⊆ 𝑋)
70	38, 69	sylan 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → 𝑢 ⊆ 𝑋)
71		dfss2 3901	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ⊆ 𝑋 ↔ (𝑢 ∩ 𝑋) = 𝑢)
72	70, 71	sylib 219	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → (𝑢 ∩ 𝑋) = 𝑢)
73	72	sseq1d 3946	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → ((𝑢 ∩ 𝑋) ⊆ 𝑥 ↔ 𝑢 ⊆ 𝑥))
74	73	biimpd 230	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → ((𝑢 ∩ 𝑋) ⊆ 𝑥 → 𝑢 ⊆ 𝑥))
75	68, 74	syl9r 78	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → ((𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛) → (¬ (𝑢 ∩ 𝑛) ≠ ∅ → 𝑢 ⊆ 𝑥)))
76	63, 75	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → (𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} → (¬ (𝑢 ∩ 𝑛) ≠ ∅ → 𝑢 ⊆ 𝑥)))
77	76	rexlimdv 3138	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → (∃𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ¬ (𝑢 ∩ 𝑛) ≠ ∅ → 𝑢 ⊆ 𝑥))
78	59, 77	biimtrrid 244	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → (¬ ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅ → 𝑢 ⊆ 𝑥))
79	78	anim2d 618	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → ((𝑦 ∈ 𝑢 ∧ ¬ ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅) → (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)))
80	79	reximdva 3152	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ ¬ ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅) → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)))
81	58, 80	biimtrrid 244	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (¬ ∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅) → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)))
82	57, 81	mpd 15	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥))
83	82	anassrs 468	. . . . . . . 8 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥)) → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥))
84	83	exp32 421	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → (𝑥 ≠ 𝑋 → (𝑦 ∈ 𝑥 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥))))
85	29, 84	pm2.61dne 3020	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → (𝑦 ∈ 𝑥 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)))
86	85	ralrimiv 3130	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥))
87		topontop 22896	. . . . . 6 ⊢ (𝐾 ∈ (TopOn‘𝑋) → 𝐾 ∈ Top)
88		eltop2 22958	. . . . . 6 ⊢ (𝐾 ∈ Top → (𝑥 ∈ 𝐾 ↔ ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)))
89	14, 87, 88	3syl 18	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → (𝑥 ∈ 𝐾 ↔ ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)))
90	86, 89	mpbird 258	. . . 4 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐾)
91	90	ex 413	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) → (𝑥 ∈ 𝐽 → 𝑥 ∈ 𝐾))
92	91	ssrdv 3921	. 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) → 𝐽 ⊆ 𝐾)
93	13, 92	impbida 806	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) → (𝐽 ⊆ 𝐾 ↔ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ≠ wne 2934  ∀wral 3053  ∃wrex 3063  {crab 3391   ∖ cdif 3880   ∩ cin 3882   ⊆ wss 3883  ∅c0 4261  𝒫 cpw 4529  ‘cfv 6485  (class class class)co 7356  Topctop 22876  TopOnctopon 22893  Filcfil 23828   fClus cfcls 23919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-iin 4924  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-topgen 17397  df-fbas 21344  df-top 22877  df-topon 22894  df-cld 23002  df-ntr 23003  df-cls 23004  df-fil 23829  df-fcls 23924

This theorem is referenced by: (None)