nrmhmph

Description: Normality is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Assertion	nrmhmph	$⊢ J ≃ K \to (J \in Nrm \to K \in Nrm)$

Proof

Step	Hyp	Ref	Expression
1		hmph	$⊢ J ≃ K \leftrightarrow J Homeo K \neq \emptyset$
2		n0	$⊢ J Homeo K \neq \emptyset \leftrightarrow \exists f f \in (J Homeo K)$
3		hmeocn	$⊢ f \in (J Homeo K) \to f \in (J Cn K)$
4	3	adantl	$⊢ (J \in Nrm \land f \in (J Homeo K)) \to f \in (J Cn K)$
5		cntop2	$⊢ f \in (J Cn K) \to K \in Top$
6	4 5	syl	$⊢ (J \in Nrm \land f \in (J Homeo K)) \to K \in Top$
7		simpll	$⊢ ((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \to J \in Nrm$
8	4	adantr	$⊢ ((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \to f \in (J Cn K)$
9		simprl	$⊢ ((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \to x \in K$
10		cnima	$⊢ (f \in (J Cn K) \land x \in K) \to f^{-1} [x] \in J$
11	8 9 10	syl2anc	$⊢ ((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \to f^{-1} [x] \in J$
12		simprr	$⊢ ((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \to y \in (Clsd (K) \cap 𝒫 x)$
13	12	elin1d	$⊢ ((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \to y \in Clsd (K)$
14		cnclima	$⊢ (f \in (J Cn K) \land y \in Clsd (K)) \to f^{-1} [y] \in Clsd (J)$
15	8 13 14	syl2anc	$⊢ ((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \to f^{-1} [y] \in Clsd (J)$
16	12	elin2d	$⊢ ((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \to y \in 𝒫 x$
17	16	elpwid	$⊢ ((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \to y \subseteq x$
18		imass2	$⊢ y \subseteq x \to f^{-1} [y] \subseteq f^{-1} [x]$
19	17 18	syl	$⊢ ((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \to f^{-1} [y] \subseteq f^{-1} [x]$
20		nrmsep3	$⊢ (J \in Nrm \land (f^{-1} [x] \in J \land f^{-1} [y] \in Clsd (J) \land f^{-1} [y] \subseteq f^{-1} [x])) \to \exists w \in J (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x])$
21	7 11 15 19 20	syl13anc	$⊢ ((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \to \exists w \in J (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x])$
22		simpllr	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to f \in (J Homeo K)$
23		simprl	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to w \in J$
24		hmeoima	$⊢ (f \in (J Homeo K) \land w \in J) \to f [w] \in K$
25	22 23 24	syl2anc	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to f [w] \in K$
26		simprrl	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to f^{-1} [y] \subseteq w$
27		eqid	$⊢ ⋃ J = ⋃ J$
28		eqid	$⊢ ⋃ K = ⋃ K$
29	27 28	hmeof1o	$⊢ f \in (J Homeo K) \to f : ⋃ J \underset{1-1 onto}{⟶} ⋃ K$
30	22 29	syl	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to f : ⋃ J \underset{1-1 onto}{⟶} ⋃ K$
31		f1ofun	$⊢ f : ⋃ J \underset{1-1 onto}{⟶} ⋃ K \to Fun f$
32	30 31	syl	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to Fun f$
33	13	adantr	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to y \in Clsd (K)$
34	28	cldss	$⊢ y \in Clsd (K) \to y \subseteq ⋃ K$
35	33 34	syl	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to y \subseteq ⋃ K$
36		f1ofo	$⊢ f : ⋃ J \underset{1-1 onto}{⟶} ⋃ K \to f : ⋃ J \underset{onto}{⟶} ⋃ K$
37		forn	$⊢ f : ⋃ J \underset{onto}{⟶} ⋃ K \to ran f = ⋃ K$
38	30 36 37	3syl	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to ran f = ⋃ K$
39	35 38	sseqtrrd	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to y \subseteq ran f$
40		funimass1	$⊢ (Fun f \land y \subseteq ran f) \to (f^{-1} [y] \subseteq w \to y \subseteq f [w])$
41	32 39 40	syl2anc	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to (f^{-1} [y] \subseteq w \to y \subseteq f [w])$
42	26 41	mpd	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to y \subseteq f [w]$
43		elssuni	$⊢ w \in J \to w \subseteq ⋃ J$
44	43	ad2antrl	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to w \subseteq ⋃ J$
45	27	hmeocls	$⊢ (f \in (J Homeo K) \land w \subseteq ⋃ J) \to cls (K) (f [w]) = f [cls (J) (w)]$
46	22 44 45	syl2anc	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to cls (K) (f [w]) = f [cls (J) (w)]$
47		simprrr	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to cls (J) (w) \subseteq f^{-1} [x]$
48		nrmtop	$⊢ J \in Nrm \to J \in Top$
49	48	ad3antrrr	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to J \in Top$
50	27	clsss3	$⊢ (J \in Top \land w \subseteq ⋃ J) \to cls (J) (w) \subseteq ⋃ J$
51	49 44 50	syl2anc	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to cls (J) (w) \subseteq ⋃ J$
52		f1odm	$⊢ f : ⋃ J \underset{1-1 onto}{⟶} ⋃ K \to dom f = ⋃ J$
53	30 52	syl	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to dom f = ⋃ J$
54	51 53	sseqtrrd	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to cls (J) (w) \subseteq dom f$
55		funimass3	$⊢ (Fun f \land cls (J) (w) \subseteq dom f) \to (f [cls (J) (w)] \subseteq x \leftrightarrow cls (J) (w) \subseteq f^{-1} [x])$
56	32 54 55	syl2anc	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to (f [cls (J) (w)] \subseteq x \leftrightarrow cls (J) (w) \subseteq f^{-1} [x])$
57	47 56	mpbird	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to f [cls (J) (w)] \subseteq x$
58	46 57	eqsstrd	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to cls (K) (f [w]) \subseteq x$
59		sseq2	$⊢ z = f [w] \to (y \subseteq z \leftrightarrow y \subseteq f [w])$
60		fveq2	$⊢ z = f [w] \to cls (K) (z) = cls (K) (f [w])$
61	60	sseq1d	$⊢ z = f [w] \to (cls (K) (z) \subseteq x \leftrightarrow cls (K) (f [w]) \subseteq x)$
62	59 61	anbi12d	$⊢ z = f [w] \to ((y \subseteq z \land cls (K) (z) \subseteq x) \leftrightarrow (y \subseteq f [w] \land cls (K) (f [w]) \subseteq x))$
63	62	rspcev	$⊢ (f [w] \in K \land (y \subseteq f [w] \land cls (K) (f [w]) \subseteq x)) \to \exists z \in K (y \subseteq z \land cls (K) (z) \subseteq x)$
64	25 42 58 63	syl12anc	$⊢ (((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \land (w \in J \land (f^{-1} [y] \subseteq w \land cls (J) (w) \subseteq f^{-1} [x]))) \to \exists z \in K (y \subseteq z \land cls (K) (z) \subseteq x)$
65	21 64	rexlimddv	$⊢ ((J \in Nrm \land f \in (J Homeo K)) \land (x \in K \land y \in (Clsd (K) \cap 𝒫 x))) \to \exists z \in K (y \subseteq z \land cls (K) (z) \subseteq x)$
66	65	ralrimivva	$⊢ (J \in Nrm \land f \in (J Homeo K)) \to \forall x \in K \forall y \in (Clsd (K) \cap 𝒫 x) \exists z \in K (y \subseteq z \land cls (K) (z) \subseteq x)$
67		isnrm	$⊢ K \in Nrm \leftrightarrow (K \in Top \land \forall x \in K \forall y \in (Clsd (K) \cap 𝒫 x) \exists z \in K (y \subseteq z \land cls (K) (z) \subseteq x))$
68	6 66 67	sylanbrc	$⊢ (J \in Nrm \land f \in (J Homeo K)) \to K \in Nrm$
69	68	expcom	$⊢ f \in (J Homeo K) \to (J \in Nrm \to K \in Nrm)$
70	69	exlimiv	$⊢ \exists f f \in (J Homeo K) \to (J \in Nrm \to K \in Nrm)$
71	2 70	sylbi	$⊢ J Homeo K \neq \emptyset \to (J \in Nrm \to K \in Nrm)$
72	1 71	sylbi	$⊢ J ≃ K \to (J \in Nrm \to K \in Nrm)$

Metamath Proof Explorer

Theorem nrmhmph

Proof