Theorem fclscf 23919

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 766	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → 𝐽 ∈ (TopOn‘𝑋))
2		simplr 768	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → 𝐾 ∈ (TopOn‘𝑋))
3		fclstopon 23906	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐾 fClus 𝑓) → (𝐾 ∈ (TopOn‘𝑋) ↔ 𝑓 ∈ (Fil‘𝑋)))
4	3	ad2antll 729	. . . . . . . 8 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → (𝐾 ∈ (TopOn‘𝑋) ↔ 𝑓 ∈ (Fil‘𝑋)))
5	2, 4	mpbid 232	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → 𝑓 ∈ (Fil‘𝑋))
6		simprl 770	. . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → 𝐽 ⊆ 𝐾)
7		fclsss1 23916	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓))
8	1, 5, 6, 7	syl3anc 1373	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → (𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓))
9		simprr 772	. . . . . 6 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → 𝑥 ∈ (𝐾 fClus 𝑓))
10	8, 9	sseldd 3950	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → 𝑥 ∈ (𝐽 fClus 𝑓))
11	10	expr 456	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) → (𝑥 ∈ (𝐾 fClus 𝑓) → 𝑥 ∈ (𝐽 fClus 𝑓)))
12	11	ssrdv 3955	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) → (𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓))
13	12	ralrimivw 3130	. 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) → ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓))
14		simpllr 775	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → 𝐾 ∈ (TopOn‘𝑋))
15		toponmax 22820	. . . . . . . . 9 ⊢ (𝐾 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐾)
16		ssid 3972	. . . . . . . . . . 11 ⊢ 𝑋 ⊆ 𝑋
17		eleq2 2818	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑋 → (𝑦 ∈ 𝑢 ↔ 𝑦 ∈ 𝑋))
18		sseq1 3975	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑋 → (𝑢 ⊆ 𝑋 ↔ 𝑋 ⊆ 𝑋))
19	17, 18	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑋 → ((𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋) ↔ (𝑦 ∈ 𝑋 ∧ 𝑋 ⊆ 𝑋)))
20	19	rspcev 3591	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝐾 ∧ (𝑦 ∈ 𝑋 ∧ 𝑋 ⊆ 𝑋)) → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋))
21	16, 20	mpanr2 704	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑦 ∈ 𝑋) → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋))
22	21	ex 412	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝐾 → (𝑦 ∈ 𝑋 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋)))
23	14, 15, 22	3syl 18	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → (𝑦 ∈ 𝑋 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋)))
24		eleq2 2818	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑋))
25		sseq2 3976	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑢 ⊆ 𝑥 ↔ 𝑢 ⊆ 𝑋))
26	25	anbi2d 630	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥) ↔ (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋)))
27	26	rexbidv 3158	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥) ↔ ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋)))
28	24, 27	imbi12d 344	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑦 ∈ 𝑥 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)) ↔ (𝑦 ∈ 𝑋 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋))))
29	23, 28	syl5ibrcom 247	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → (𝑥 = 𝑋 → (𝑦 ∈ 𝑥 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥))))
30		simplll 774	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝐽 ∈ (TopOn‘𝑋))
31		simprl 770	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑥 ∈ 𝐽)
32		simprrr 781	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑦 ∈ 𝑥)
33		supnfcls 23914	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) → ¬ 𝑦 ∈ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
34	30, 31, 32, 33	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → ¬ 𝑦 ∈ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
35		toponss 22821	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝐽) → 𝑥 ⊆ 𝑋)
36	30, 31, 35	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑥 ⊆ 𝑋)
37	36, 32	sseldd 3950	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑦 ∈ 𝑋)
38		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝐾 ∈ (TopOn‘𝑋))
39		toponmax 22820	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽)
40	30, 39	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑋 ∈ 𝐽)
41		difssd 4103	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝑋 ∖ 𝑥) ⊆ 𝑋)
42		simprrl 780	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑥 ≠ 𝑋)
43		pssdifn0 4334	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ⊆ 𝑋 ∧ 𝑥 ≠ 𝑋) → (𝑋 ∖ 𝑥) ≠ ∅)
44	36, 42, 43	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝑋 ∖ 𝑥) ≠ ∅)
45		supfil 23789	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝐽 ∧ (𝑋 ∖ 𝑥) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) ≠ ∅) → {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ∈ (Fil‘𝑋))
46	40, 41, 44, 45	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ∈ (Fil‘𝑋))
47		fclsopn 23908	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ∈ (Fil‘𝑋)) → (𝑦 ∈ (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}) ↔ (𝑦 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅))))
48	38, 46, 47	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝑦 ∈ (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}) ↔ (𝑦 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅))))
49	37, 48	mpbirand 707	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝑦 ∈ (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}) ↔ ∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅)))
50		oveq2 7398	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} → (𝐾 fClus 𝑓) = (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
51		oveq2 7398	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} → (𝐽 fClus 𝑓) = (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
52	50, 51	sseq12d 3983	. . . . . . . . . . . . . 14 ⊢ (𝑓 = {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} → ((𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓) ↔ (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}) ⊆ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦})))
53		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓))
54	52, 53, 46	rspcdva 3592	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}) ⊆ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
55	54	sseld 3948	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝑦 ∈ (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}) → 𝑦 ∈ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦})))
56	49, 55	sylbird 260	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅) → 𝑦 ∈ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦})))
57	34, 56	mtod 198	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → ¬ ∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅))
58		rexanali 3085	. . . . . . . . . . 11 ⊢ (∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ ¬ ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅) ↔ ¬ ∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅))
59		rexnal 3083	. . . . . . . . . . . . . 14 ⊢ (∃𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ¬ (𝑢 ∩ 𝑛) ≠ ∅ ↔ ¬ ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅)
60		sseq2 3976	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → ((𝑋 ∖ 𝑥) ⊆ 𝑦 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑛))
61	60	elrab 3662	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ↔ (𝑛 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑥) ⊆ 𝑛))
62		sslin 4209	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∖ 𝑥) ⊆ 𝑛 → (𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛))
63	61, 62	simplbiim 504	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} → (𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛))
64		ssn0 4370	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛) ∧ (𝑢 ∩ (𝑋 ∖ 𝑥)) ≠ ∅) → (𝑢 ∩ 𝑛) ≠ ∅)
65	64	ex 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛) → ((𝑢 ∩ (𝑋 ∖ 𝑥)) ≠ ∅ → (𝑢 ∩ 𝑛) ≠ ∅))
66	65	necon1bd 2944	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛) → (¬ (𝑢 ∩ 𝑛) ≠ ∅ → (𝑢 ∩ (𝑋 ∖ 𝑥)) = ∅))
67		inssdif0 4340	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∩ 𝑋) ⊆ 𝑥 ↔ (𝑢 ∩ (𝑋 ∖ 𝑥)) = ∅)
68	66, 67	imbitrrdi 252	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛) → (¬ (𝑢 ∩ 𝑛) ≠ ∅ → (𝑢 ∩ 𝑋) ⊆ 𝑥))
69		toponss 22821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝑢 ∈ 𝐾) → 𝑢 ⊆ 𝑋)
70	38, 69	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → 𝑢 ⊆ 𝑋)
71		dfss2 3935	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ⊆ 𝑋 ↔ (𝑢 ∩ 𝑋) = 𝑢)
72	70, 71	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → (𝑢 ∩ 𝑋) = 𝑢)
73	72	sseq1d 3981	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → ((𝑢 ∩ 𝑋) ⊆ 𝑥 ↔ 𝑢 ⊆ 𝑥))
74	73	biimpd 229	. . . . . . . . . . . . . . . . 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 3133	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → (∃𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ¬ (𝑢 ∩ 𝑛) ≠ ∅ → 𝑢 ⊆ 𝑥))
78	59, 77	biimtrrid 243	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → (¬ ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅ → 𝑢 ⊆ 𝑥))
79	78	anim2d 612	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → ((𝑦 ∈ 𝑢 ∧ ¬ ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅) → (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)))
80	79	reximdva 3147	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ ¬ ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅) → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)))
81	58, 80	biimtrrid 243	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (¬ ∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅) → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)))
82	57, 81	mpd 15	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥))
83	82	anassrs 467	. . . . . . . 8 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥)) → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥))
84	83	exp32 420	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → (𝑥 ≠ 𝑋 → (𝑦 ∈ 𝑥 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥))))
85	29, 84	pm2.61dne 3012	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → (𝑦 ∈ 𝑥 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)))
86	85	ralrimiv 3125	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥))
87		topontop 22807	. . . . . 6 ⊢ (𝐾 ∈ (TopOn‘𝑋) → 𝐾 ∈ Top)
88		eltop2 22869	. . . . . 6 ⊢ (𝐾 ∈ Top → (𝑥 ∈ 𝐾 ↔ ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)))
89	14, 87, 88	3syl 18	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → (𝑥 ∈ 𝐾 ↔ ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)))
90	86, 89	mpbird 257	. . . 4 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐾)
91	90	ex 412	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) → (𝑥 ∈ 𝐽 → 𝑥 ∈ 𝐾))
92	91	ssrdv 3955	. 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) → 𝐽 ⊆ 𝐾)
93	13, 92	impbida 800	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) → (𝐽 ⊆ 𝐾 ↔ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ∀wral 3045  ∃wrex 3054  {crab 3408   ∖ cdif 3914   ∩ cin 3916   ⊆ wss 3917  ∅c0 4299  𝒫 cpw 4566  ‘cfv 6514  (class class class)co 7390  Topctop 22787  TopOnctopon 22804  Filcfil 23739   fClus cfcls 23830

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-iin 4961  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-topgen 17413  df-fbas 21268  df-top 22788  df-topon 22805  df-cld 22913  df-ntr 22914  df-cls 22915  df-fil 23740  df-fcls 23835

This theorem is referenced by: (None)