fclscf

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)

		Ref	Expression
	Assertion	fclscf	$⊢ (J \in TopOn (X) \land K \in TopOn (X)) \to (J \subseteq K \leftrightarrow \forall f \in Fil (X) K fClus f \subseteq J fClus f)$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land (J \subseteq K \land x \in (K fClus f))) \to J \in TopOn (X)$
2		simplr	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land (J \subseteq K \land x \in (K fClus f))) \to K \in TopOn (X)$
3		fclstopon	$⊢ x \in (K fClus f) \to (K \in TopOn (X) \leftrightarrow f \in Fil (X))$
4	3	ad2antll	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land (J \subseteq K \land x \in (K fClus f))) \to (K \in TopOn (X) \leftrightarrow f \in Fil (X))$
5	2 4	mpbid	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land (J \subseteq K \land x \in (K fClus f))) \to f \in Fil (X)$
6		simprl	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land (J \subseteq K \land x \in (K fClus f))) \to J \subseteq K$
7		fclsss1	$⊢ (J \in TopOn (X) \land f \in Fil (X) \land J \subseteq K) \to K fClus f \subseteq J fClus f$
8	1 5 6 7	syl3anc	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land (J \subseteq K \land x \in (K fClus f))) \to K fClus f \subseteq J fClus f$
9		simprr	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land (J \subseteq K \land x \in (K fClus f))) \to x \in (K fClus f)$
10	8 9	sseldd	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land (J \subseteq K \land x \in (K fClus f))) \to x \in (J fClus f)$
11	10	expr	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land J \subseteq K) \to (x \in (K fClus f) \to x \in (J fClus f))$
12	11	ssrdv	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land J \subseteq K) \to K fClus f \subseteq J fClus f$
13	12	ralrimivw	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land J \subseteq K) \to \forall f \in Fil (X) K fClus f \subseteq J fClus f$
14		simpllr	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land x \in J) \to K \in TopOn (X)$
15		toponmax	$⊢ K \in TopOn (X) \to X \in K$
16		ssid	$⊢ X \subseteq X$
17		eleq2	$⊢ u = X \to (y \in u \leftrightarrow y \in X)$
18		sseq1	$⊢ u = X \to (u \subseteq X \leftrightarrow X \subseteq X)$
19	17 18	anbi12d	$⊢ u = X \to ((y \in u \land u \subseteq X) \leftrightarrow (y \in X \land X \subseteq X))$
20	19	rspcev	$⊢ (X \in K \land (y \in X \land X \subseteq X)) \to \exists u \in K (y \in u \land u \subseteq X)$
21	16 20	mpanr2	$⊢ (X \in K \land y \in X) \to \exists u \in K (y \in u \land u \subseteq X)$
22	21	ex	$⊢ X \in K \to (y \in X \to \exists u \in K (y \in u \land u \subseteq X))$
23	14 15 22	3syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land x \in J) \to (y \in X \to \exists u \in K (y \in u \land u \subseteq X))$
24		eleq2	$⊢ x = X \to (y \in x \leftrightarrow y \in X)$
25		sseq2	$⊢ x = X \to (u \subseteq x \leftrightarrow u \subseteq X)$
26	25	anbi2d	$⊢ x = X \to ((y \in u \land u \subseteq x) \leftrightarrow (y \in u \land u \subseteq X))$
27	26	rexbidv	$⊢ x = X \to (\exists u \in K (y \in u \land u \subseteq x) \leftrightarrow \exists u \in K (y \in u \land u \subseteq X))$
28	24 27	imbi12d	$⊢ x = X \to ((y \in x \to \exists u \in K (y \in u \land u \subseteq x)) \leftrightarrow (y \in X \to \exists u \in K (y \in u \land u \subseteq X)))$
29	23 28	syl5ibrcom	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land x \in J) \to (x = X \to (y \in x \to \exists u \in K (y \in u \land u \subseteq x)))$
30		simplll	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to J \in TopOn (X)$
31		simprl	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to x \in J$
32		simprrr	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to y \in x$
33		supnfcls	$⊢ (J \in TopOn (X) \land x \in J \land y \in x) \to \neg y \in (J fClus \{y \in 𝒫 X \| X ∖ x \subseteq y\})$
34	30 31 32 33	syl3anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to \neg y \in (J fClus \{y \in 𝒫 X \| X ∖ x \subseteq y\})$
35		toponss	$⊢ (J \in TopOn (X) \land x \in J) \to x \subseteq X$
36	30 31 35	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to x \subseteq X$
37	36 32	sseldd	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to y \in X$
38		simpllr	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to K \in TopOn (X)$
39		toponmax	$⊢ J \in TopOn (X) \to X \in J$
40	30 39	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to X \in J$
41		difssd	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to X ∖ x \subseteq X$
42		simprrl	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to x \neq X$
43		pssdifn0	$⊢ (x \subseteq X \land x \neq X) \to X ∖ x \neq \emptyset$
44	36 42 43	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to X ∖ x \neq \emptyset$
45		supfil	$⊢ (X \in J \land X ∖ x \subseteq X \land X ∖ x \neq \emptyset) \to \{y \in 𝒫 X \| X ∖ x \subseteq y\} \in Fil (X)$
46	40 41 44 45	syl3anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to \{y \in 𝒫 X \| X ∖ x \subseteq y\} \in Fil (X)$
47		fclsopn	$⊢ (K \in TopOn (X) \land \{y \in 𝒫 X \| X ∖ x \subseteq y\} \in Fil (X)) \to (y \in (K fClus \{y \in 𝒫 X \| X ∖ x \subseteq y\}) \leftrightarrow (y \in X \land \forall u \in K (y \in u \to \forall n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} u \cap n \neq \emptyset)))$
48	38 46 47	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to (y \in (K fClus \{y \in 𝒫 X \| X ∖ x \subseteq y\}) \leftrightarrow (y \in X \land \forall u \in K (y \in u \to \forall n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} u \cap n \neq \emptyset)))$
49	37 48	mpbirand	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to (y \in (K fClus \{y \in 𝒫 X \| X ∖ x \subseteq y\}) \leftrightarrow \forall u \in K (y \in u \to \forall n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} u \cap n \neq \emptyset))$
50		oveq2	$⊢ f = \{y \in 𝒫 X \| X ∖ x \subseteq y\} \to K fClus f = K fClus \{y \in 𝒫 X \| X ∖ x \subseteq y\}$
51		oveq2	$⊢ f = \{y \in 𝒫 X \| X ∖ x \subseteq y\} \to J fClus f = J fClus \{y \in 𝒫 X \| X ∖ x \subseteq y\}$
52	50 51	sseq12d	$⊢ f = \{y \in 𝒫 X \| X ∖ x \subseteq y\} \to (K fClus f \subseteq J fClus f \leftrightarrow K fClus \{y \in 𝒫 X \| X ∖ x \subseteq y\} \subseteq J fClus \{y \in 𝒫 X \| X ∖ x \subseteq y\})$
53		simplr	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to \forall f \in Fil (X) K fClus f \subseteq J fClus f$
54	52 53 46	rspcdva	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to K fClus \{y \in 𝒫 X \| X ∖ x \subseteq y\} \subseteq J fClus \{y \in 𝒫 X \| X ∖ x \subseteq y\}$
55	54	sseld	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to (y \in (K fClus \{y \in 𝒫 X \| X ∖ x \subseteq y\}) \to y \in (J fClus \{y \in 𝒫 X \| X ∖ x \subseteq y\}))$
56	49 55	sylbird	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to (\forall u \in K (y \in u \to \forall n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} u \cap n \neq \emptyset) \to y \in (J fClus \{y \in 𝒫 X \| X ∖ x \subseteq y\}))$
57	34 56	mtod	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to \neg \forall u \in K (y \in u \to \forall n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} u \cap n \neq \emptyset)$
58		rexanali	$⊢ \exists u \in K (y \in u \land \neg \forall n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} u \cap n \neq \emptyset) \leftrightarrow \neg \forall u \in K (y \in u \to \forall n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} u \cap n \neq \emptyset)$
59		rexnal	$⊢ \exists n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} \neg u \cap n \neq \emptyset \leftrightarrow \neg \forall n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} u \cap n \neq \emptyset$
60		sseq2	$⊢ y = n \to (X ∖ x \subseteq y \leftrightarrow X ∖ x \subseteq n)$
61	60	elrab	$⊢ n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} \leftrightarrow (n \in 𝒫 X \land X ∖ x \subseteq n)$
62		sslin	$⊢ X ∖ x \subseteq n \to u \cap (X ∖ x) \subseteq u \cap n$
63	61 62	simplbiim	$⊢ n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} \to u \cap (X ∖ x) \subseteq u \cap n$
64		ssn0	$⊢ (u \cap (X ∖ x) \subseteq u \cap n \land u \cap (X ∖ x) \neq \emptyset) \to u \cap n \neq \emptyset$
65	64	ex	$⊢ u \cap (X ∖ x) \subseteq u \cap n \to (u \cap (X ∖ x) \neq \emptyset \to u \cap n \neq \emptyset)$
66	65	necon1bd	$⊢ u \cap (X ∖ x) \subseteq u \cap n \to (\neg u \cap n \neq \emptyset \to u \cap (X ∖ x) = \emptyset)$
67		inssdif0	$⊢ u \cap X \subseteq x \leftrightarrow u \cap (X ∖ x) = \emptyset$
68	66 67	syl6ibr	$⊢ u \cap (X ∖ x) \subseteq u \cap n \to (\neg u \cap n \neq \emptyset \to u \cap X \subseteq x)$
69		toponss	$⊢ (K \in TopOn (X) \land u \in K) \to u \subseteq X$
70	38 69	sylan	$⊢ ((((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \land u \in K) \to u \subseteq X$
71		df-ss	$⊢ u \subseteq X \leftrightarrow u \cap X = u$
72	70 71	sylib	$⊢ ((((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \land u \in K) \to u \cap X = u$
73	72	sseq1d	$⊢ ((((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \land u \in K) \to (u \cap X \subseteq x \leftrightarrow u \subseteq x)$
74	73	biimpd	$⊢ ((((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \land u \in K) \to (u \cap X \subseteq x \to u \subseteq x)$
75	68 74	syl9r	$⊢ ((((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \land u \in K) \to (u \cap (X ∖ x) \subseteq u \cap n \to (\neg u \cap n \neq \emptyset \to u \subseteq x))$
76	63 75	syl5	$⊢ ((((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \land u \in K) \to (n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} \to (\neg u \cap n \neq \emptyset \to u \subseteq x))$
77	76	rexlimdv	$⊢ ((((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \land u \in K) \to (\exists n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} \neg u \cap n \neq \emptyset \to u \subseteq x)$
78	59 77	syl5bir	$⊢ ((((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \land u \in K) \to (\neg \forall n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} u \cap n \neq \emptyset \to u \subseteq x)$
79	78	anim2d	$⊢ ((((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \land u \in K) \to ((y \in u \land \neg \forall n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} u \cap n \neq \emptyset) \to (y \in u \land u \subseteq x))$
80	79	reximdva	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to (\exists u \in K (y \in u \land \neg \forall n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} u \cap n \neq \emptyset) \to \exists u \in K (y \in u \land u \subseteq x))$
81	58 80	syl5bir	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to (\neg \forall u \in K (y \in u \to \forall n \in \{y \in 𝒫 X \| X ∖ x \subseteq y\} u \cap n \neq \emptyset) \to \exists u \in K (y \in u \land u \subseteq x))$
82	57 81	mpd	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land (x \in J \land (x \neq X \land y \in x))) \to \exists u \in K (y \in u \land u \subseteq x)$
83	82	anassrs	$⊢ ((((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land x \in J) \land (x \neq X \land y \in x)) \to \exists u \in K (y \in u \land u \subseteq x)$
84	83	exp32	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land x \in J) \to (x \neq X \to (y \in x \to \exists u \in K (y \in u \land u \subseteq x)))$
85	29 84	pm2.61dne	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land x \in J) \to (y \in x \to \exists u \in K (y \in u \land u \subseteq x))$
86	85	ralrimiv	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land x \in J) \to \forall y \in x \exists u \in K (y \in u \land u \subseteq x)$
87		topontop	$⊢ K \in TopOn (X) \to K \in Top$
88		eltop2	$⊢ K \in Top \to (x \in K \leftrightarrow \forall y \in x \exists u \in K (y \in u \land u \subseteq x))$
89	14 87 88	3syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land x \in J) \to (x \in K \leftrightarrow \forall y \in x \exists u \in K (y \in u \land u \subseteq x))$
90	86 89	mpbird	$⊢ (((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \land x \in J) \to x \in K$
91	90	ex	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \to (x \in J \to x \in K)$
92	91	ssrdv	$⊢ ((J \in TopOn (X) \land K \in TopOn (X)) \land \forall f \in Fil (X) K fClus f \subseteq J fClus f) \to J \subseteq K$
93	13 92	impbida	$⊢ (J \in TopOn (X) \land K \in TopOn (X)) \to (J \subseteq K \leftrightarrow \forall f \in Fil (X) K fClus f \subseteq J fClus f)$

Metamath Proof Explorer

Theorem fclscf

Proof