Theorem fclscf 23967

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 23954	. . . . . . . . 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 23964	. . . . . . 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 3932	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ (𝐽 ⊆ 𝐾 ∧ 𝑥 ∈ (𝐾 fClus 𝑓))) → 𝑥 ∈ (𝐽 fClus 𝑓))
11	10	expr 456	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) → (𝑥 ∈ (𝐾 fClus 𝑓) → 𝑥 ∈ (𝐽 fClus 𝑓)))
12	11	ssrdv 3937	. . 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 22868	. . . . . . . . 9 ⊢ (𝐾 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐾)
16		ssid 3954	. . . . . . . . . . 11 ⊢ 𝑋 ⊆ 𝑋
17		eleq2 2823	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑋 → (𝑦 ∈ 𝑢 ↔ 𝑦 ∈ 𝑋))
18		sseq1 3957	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑋 → (𝑢 ⊆ 𝑋 ↔ 𝑋 ⊆ 𝑋))
19	17, 18	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑋 → ((𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑋) ↔ (𝑦 ∈ 𝑋 ∧ 𝑋 ⊆ 𝑋)))
20	19	rspcev 3574	. . . . . . . . . . 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 2823	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑋))
25		sseq2 3958	. . . . . . . . . . 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 23962	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) → ¬ 𝑦 ∈ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
34	30, 31, 32, 33	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → ¬ 𝑦 ∈ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
35		toponss 22869	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝐽) → 𝑥 ⊆ 𝑋)
36	30, 31, 35	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑥 ⊆ 𝑋)
37	36, 32	sseldd 3932	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑦 ∈ 𝑋)
38		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝐾 ∈ (TopOn‘𝑋))
39		toponmax 22868	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽)
40	30, 39	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑋 ∈ 𝐽)
41		difssd 4087	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝑋 ∖ 𝑥) ⊆ 𝑋)
42		simprrl 780	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → 𝑥 ≠ 𝑋)
43		pssdifn0 4318	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ⊆ 𝑋 ∧ 𝑥 ≠ 𝑋) → (𝑋 ∖ 𝑥) ≠ ∅)
44	36, 42, 43	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝑋 ∖ 𝑥) ≠ ∅)
45		supfil 23837	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝐽 ∧ (𝑋 ∖ 𝑥) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑥) ≠ ∅) → {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ∈ (Fil‘𝑋))
46	40, 41, 44, 45	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ∈ (Fil‘𝑋))
47		fclsopn 23956	. . . . . . . . . . . . . 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 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} → (𝐾 fClus 𝑓) = (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
51		oveq2 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} → (𝐽 fClus 𝑓) = (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
52	50, 51	sseq12d 3965	. . . . . . . . . . . . . 14 ⊢ (𝑓 = {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} → ((𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓) ↔ (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}) ⊆ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦})))
53		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓))
54	52, 53, 46	rspcdva 3575	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) → (𝐾 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}) ⊆ (𝐽 fClus {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦}))
55	54	sseld 3930	. . . . . . . . . . . 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 3088	. . . . . . . . . . 11 ⊢ (∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ ¬ ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅) ↔ ¬ ∀𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 → ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅))
59		rexnal 3086	. . . . . . . . . . . . . 14 ⊢ (∃𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ¬ (𝑢 ∩ 𝑛) ≠ ∅ ↔ ¬ ∀𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} (𝑢 ∩ 𝑛) ≠ ∅)
60		sseq2 3958	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → ((𝑋 ∖ 𝑥) ⊆ 𝑦 ↔ (𝑋 ∖ 𝑥) ⊆ 𝑛))
61	60	elrab 3644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} ↔ (𝑛 ∈ 𝒫 𝑋 ∧ (𝑋 ∖ 𝑥) ⊆ 𝑛))
62		sslin 4193	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∖ 𝑥) ⊆ 𝑛 → (𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛))
63	61, 62	simplbiim 504	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ {𝑦 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ⊆ 𝑦} → (𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛))
64		ssn0 4354	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛) ∧ (𝑢 ∩ (𝑋 ∖ 𝑥)) ≠ ∅) → (𝑢 ∩ 𝑛) ≠ ∅)
65	64	ex 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛) → ((𝑢 ∩ (𝑋 ∖ 𝑥)) ≠ ∅ → (𝑢 ∩ 𝑛) ≠ ∅))
66	65	necon1bd 2948	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛) → (¬ (𝑢 ∩ 𝑛) ≠ ∅ → (𝑢 ∩ (𝑋 ∖ 𝑥)) = ∅))
67		inssdif0 4324	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∩ 𝑋) ⊆ 𝑥 ↔ (𝑢 ∩ (𝑋 ∖ 𝑥)) = ∅)
68	66, 67	imbitrrdi 252	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∩ (𝑋 ∖ 𝑥)) ⊆ (𝑢 ∩ 𝑛) → (¬ (𝑢 ∩ 𝑛) ≠ ∅ → (𝑢 ∩ 𝑋) ⊆ 𝑥))
69		toponss 22869	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝑢 ∈ 𝐾) → 𝑢 ⊆ 𝑋)
70	38, 69	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → 𝑢 ⊆ 𝑋)
71		dfss2 3917	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ⊆ 𝑋 ↔ (𝑢 ∩ 𝑋) = 𝑢)
72	70, 71	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ (𝑥 ≠ 𝑋 ∧ 𝑦 ∈ 𝑥))) ∧ 𝑢 ∈ 𝐾) → (𝑢 ∩ 𝑋) = 𝑢)
73	72	sseq1d 3963	. . . . . . . . . . . . . . . . . 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 3016	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → (𝑦 ∈ 𝑥 → ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥)))
86	85	ralrimiv 3125	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)) ∧ 𝑥 ∈ 𝐽) → ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝐾 (𝑦 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑥))
87		topontop 22855	. . . . . 6 ⊢ (𝐾 ∈ (TopOn‘𝑋) → 𝐾 ∈ Top)
88		eltop2 22917	. . . . . 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 3937	. 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 1541   ∈ wcel 2113   ≠ wne 2930  ∀wral 3049  ∃wrex 3058  {crab 3397   ∖ cdif 3896   ∩ cin 3898   ⊆ wss 3899  ∅c0 4283  𝒫 cpw 4552  ‘cfv 6490  (class class class)co 7356  Topctop 22835  TopOnctopon 22852  Filcfil 23787   fClus cfcls 23878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-int 4901  df-iun 4946  df-iin 4947  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361  df-topgen 17361  df-fbas 21304  df-top 22836  df-topon 22853  df-cld 22961  df-ntr 22962  df-cls 22963  df-fil 23788  df-fcls 23883

This theorem is referenced by: (None)