nrmr0reg

Description: A normal R_0 space is also regular. These spaces are usually referred to as normal regular spaces. (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Assertion	nrmr0reg	$⊢ (J \in Nrm \land KQ (J) \in Fre) \to J \in Reg$

Proof

Step	Hyp	Ref	Expression
1		nrmtop	$⊢ J \in Nrm \to J \in Top$
2	1	adantr	$⊢ (J \in Nrm \land KQ (J) \in Fre) \to J \in Top$
3		simpll	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to J \in Nrm$
4		simprl	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to x \in J$
5	2	adantr	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to J \in Top$
6		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
7	5 6	sylib	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to J \in TopOn (⋃ J)$
8		simplr	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to KQ (J) \in Fre$
9		simprr	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to y \in x$
10		elunii	$⊢ (y \in x \land x \in J) \to y \in ⋃ J$
11	9 4 10	syl2anc	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to y \in ⋃ J$
12		eqid	$⊢ (z \in ⋃ J ⟼ \{w \in J \| z \in w\}) = (z \in ⋃ J ⟼ \{w \in J \| z \in w\})$
13	12	r0cld	$⊢ (J \in TopOn (⋃ J) \land KQ (J) \in Fre \land y \in ⋃ J) \to \{a \in ⋃ J \| \forall b \in J (a \in b \leftrightarrow y \in b)\} \in Clsd (J)$
14	7 8 11 13	syl3anc	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to \{a \in ⋃ J \| \forall b \in J (a \in b \leftrightarrow y \in b)\} \in Clsd (J)$
15		simp1rr	$⊢ (((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \land a \in ⋃ J \land \forall b \in J (a \in b \leftrightarrow y \in b)) \to y \in x$
16	4	adantr	$⊢ (((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \land a \in ⋃ J) \to x \in J$
17		elequ2	$⊢ b = x \to (a \in b \leftrightarrow a \in x)$
18		elequ2	$⊢ b = x \to (y \in b \leftrightarrow y \in x)$
19	17 18	bibi12d	$⊢ b = x \to ((a \in b \leftrightarrow y \in b) \leftrightarrow (a \in x \leftrightarrow y \in x))$
20	19	rspcv	$⊢ x \in J \to (\forall b \in J (a \in b \leftrightarrow y \in b) \to (a \in x \leftrightarrow y \in x))$
21	16 20	syl	$⊢ (((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \land a \in ⋃ J) \to (\forall b \in J (a \in b \leftrightarrow y \in b) \to (a \in x \leftrightarrow y \in x))$
22	21	3impia	$⊢ (((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \land a \in ⋃ J \land \forall b \in J (a \in b \leftrightarrow y \in b)) \to (a \in x \leftrightarrow y \in x)$
23	15 22	mpbird	$⊢ (((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \land a \in ⋃ J \land \forall b \in J (a \in b \leftrightarrow y \in b)) \to a \in x$
24	23	rabssdv	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to \{a \in ⋃ J \| \forall b \in J (a \in b \leftrightarrow y \in b)\} \subseteq x$
25		nrmsep3	$⊢ (J \in Nrm \land (x \in J \land \{a \in ⋃ J \| \forall b \in J (a \in b \leftrightarrow y \in b)\} \in Clsd (J) \land \{a \in ⋃ J \| \forall b \in J (a \in b \leftrightarrow y \in b)\} \subseteq x)) \to \exists z \in J (\{a \in ⋃ J \| \forall b \in J (a \in b \leftrightarrow y \in b)\} \subseteq z \land cls (J) (z) \subseteq x)$
26	3 4 14 24 25	syl13anc	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to \exists z \in J (\{a \in ⋃ J \| \forall b \in J (a \in b \leftrightarrow y \in b)\} \subseteq z \land cls (J) (z) \subseteq x)$
27		elequ1	$⊢ a = y \to (a \in b \leftrightarrow y \in b)$
28	27	bibi1d	$⊢ a = y \to ((a \in b \leftrightarrow y \in b) \leftrightarrow (y \in b \leftrightarrow y \in b))$
29	28	ralbidv	$⊢ a = y \to (\forall b \in J (a \in b \leftrightarrow y \in b) \leftrightarrow \forall b \in J (y \in b \leftrightarrow y \in b))$
30		biidd	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to (y \in b \leftrightarrow y \in b)$
31	30	ralrimivw	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to \forall b \in J (y \in b \leftrightarrow y \in b)$
32	29 11 31	elrabd	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to y \in \{a \in ⋃ J \| \forall b \in J (a \in b \leftrightarrow y \in b)\}$
33		ssel	$⊢ \{a \in ⋃ J \| \forall b \in J (a \in b \leftrightarrow y \in b)\} \subseteq z \to (y \in \{a \in ⋃ J \| \forall b \in J (a \in b \leftrightarrow y \in b)\} \to y \in z)$
34	32 33	syl5com	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to (\{a \in ⋃ J \| \forall b \in J (a \in b \leftrightarrow y \in b)\} \subseteq z \to y \in z)$
35	34	anim1d	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to ((\{a \in ⋃ J \| \forall b \in J (a \in b \leftrightarrow y \in b)\} \subseteq z \land cls (J) (z) \subseteq x) \to (y \in z \land cls (J) (z) \subseteq x))$
36	35	reximdv	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to (\exists z \in J (\{a \in ⋃ J \| \forall b \in J (a \in b \leftrightarrow y \in b)\} \subseteq z \land cls (J) (z) \subseteq x) \to \exists z \in J (y \in z \land cls (J) (z) \subseteq x))$
37	26 36	mpd	$⊢ ((J \in Nrm \land KQ (J) \in Fre) \land (x \in J \land y \in x)) \to \exists z \in J (y \in z \land cls (J) (z) \subseteq x)$
38	37	ralrimivva	$⊢ (J \in Nrm \land KQ (J) \in Fre) \to \forall x \in J \forall y \in x \exists z \in J (y \in z \land cls (J) (z) \subseteq x)$
39		isreg	$⊢ J \in Reg \leftrightarrow (J \in Top \land \forall x \in J \forall y \in x \exists z \in J (y \in z \land cls (J) (z) \subseteq x))$
40	2 38 39	sylanbrc	$⊢ (J \in Nrm \land KQ (J) \in Fre) \to J \in Reg$

Metamath Proof Explorer

Theorem nrmr0reg

Proof