r0cld

Description: The analogue of the T_1 axiom (singletons are closed) for an R_0 space. In an R_0 space the set of all points topologically indistinguishable from A is closed. (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Hypothesis	kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
	Assertion	r0cld	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to \{z \in X \| \forall o \in J (z \in o \leftrightarrow A \in o)\} \in Clsd (J)$

Proof

Step	Hyp	Ref	Expression
1		kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
2	1	kqffn	$⊢ J \in TopOn (X) \to F Fn X$
3	2	3ad2ant1	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to F Fn X$
4		fncnvima2	$⊢ F Fn X \to F^{-1} [\{F (A)\}] = \{z \in X \| F (z) \in \{F (A)\}\}$
5	3 4	syl	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to F^{-1} [\{F (A)\}] = \{z \in X \| F (z) \in \{F (A)\}\}$
6		fvex	$⊢ F (z) \in V$
7	6	elsn	$⊢ F (z) \in \{F (A)\} \leftrightarrow F (z) = F (A)$
8		simpl1	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \land z \in X) \to J \in TopOn (X)$
9		simpr	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \land z \in X) \to z \in X$
10		simpl3	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \land z \in X) \to A \in X$
11	1	kqfeq	$⊢ (J \in TopOn (X) \land z \in X \land A \in X) \to (F (z) = F (A) \leftrightarrow \forall y \in J (z \in y \leftrightarrow A \in y))$
12		eleq2w	$⊢ y = o \to (z \in y \leftrightarrow z \in o)$
13		eleq2w	$⊢ y = o \to (A \in y \leftrightarrow A \in o)$
14	12 13	bibi12d	$⊢ y = o \to ((z \in y \leftrightarrow A \in y) \leftrightarrow (z \in o \leftrightarrow A \in o))$
15	14	cbvralvw	$⊢ \forall y \in J (z \in y \leftrightarrow A \in y) \leftrightarrow \forall o \in J (z \in o \leftrightarrow A \in o)$
16	11 15	bitrdi	$⊢ (J \in TopOn (X) \land z \in X \land A \in X) \to (F (z) = F (A) \leftrightarrow \forall o \in J (z \in o \leftrightarrow A \in o))$
17	8 9 10 16	syl3anc	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \land z \in X) \to (F (z) = F (A) \leftrightarrow \forall o \in J (z \in o \leftrightarrow A \in o))$
18	7 17	syl5bb	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \land z \in X) \to (F (z) \in \{F (A)\} \leftrightarrow \forall o \in J (z \in o \leftrightarrow A \in o))$
19	18	rabbidva	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to \{z \in X \| F (z) \in \{F (A)\}\} = \{z \in X \| \forall o \in J (z \in o \leftrightarrow A \in o)\}$
20	5 19	eqtrd	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to F^{-1} [\{F (A)\}] = \{z \in X \| \forall o \in J (z \in o \leftrightarrow A \in o)\}$
21	1	kqid	$⊢ J \in TopOn (X) \to F \in (J Cn KQ (J))$
22	21	3ad2ant1	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to F \in (J Cn KQ (J))$
23		simp2	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to KQ (J) \in Fre$
24		simp3	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to A \in X$
25		fnfvelrn	$⊢ (F Fn X \land A \in X) \to F (A) \in ran F$
26	3 24 25	syl2anc	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to F (A) \in ran F$
27	1	kqtopon	$⊢ J \in TopOn (X) \to KQ (J) \in TopOn (ran F)$
28	27	3ad2ant1	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to KQ (J) \in TopOn (ran F)$
29		toponuni	$⊢ KQ (J) \in TopOn (ran F) \to ran F = ⋃ KQ (J)$
30	28 29	syl	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to ran F = ⋃ KQ (J)$
31	26 30	eleqtrd	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to F (A) \in ⋃ KQ (J)$
32		eqid	$⊢ ⋃ KQ (J) = ⋃ KQ (J)$
33	32	t1sncld	$⊢ (KQ (J) \in Fre \land F (A) \in ⋃ KQ (J)) \to \{F (A)\} \in Clsd (KQ (J))$
34	23 31 33	syl2anc	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to \{F (A)\} \in Clsd (KQ (J))$
35		cnclima	$⊢ (F \in (J Cn KQ (J)) \land \{F (A)\} \in Clsd (KQ (J))) \to F^{-1} [\{F (A)\}] \in Clsd (J)$
36	22 34 35	syl2anc	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to F^{-1} [\{F (A)\}] \in Clsd (J)$
37	20 36	eqeltrrd	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre \land A \in X) \to \{z \in X \| \forall o \in J (z \in o \leftrightarrow A \in o)\} \in Clsd (J)$

Metamath Proof Explorer

Theorem r0cld

Proof