reghmph

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

		Ref	Expression
	Assertion	reghmph	$⊢ J ≃ K \to (J \in Reg \to K \in Reg)$

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 Reg \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 Reg \land f \in (J Homeo K)) \to K \in Top$
7		simpll	$⊢ ((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \to J \in Reg$
8	4	adantr	$⊢ ((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \to f \in (J Cn K)$
9		simprl	$⊢ ((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in 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 Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \to f^{-1} [x] \in J$
12		eqid	$⊢ ⋃ J = ⋃ J$
13		eqid	$⊢ ⋃ K = ⋃ K$
14	12 13	hmeof1o	$⊢ f \in (J Homeo K) \to f : ⋃ J \underset{1-1 onto}{⟶} ⋃ K$
15	14	ad2antlr	$⊢ ((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \to f : ⋃ J \underset{1-1 onto}{⟶} ⋃ K$
16		f1ocnv	$⊢ f : ⋃ J \underset{1-1 onto}{⟶} ⋃ K \to f^{-1} : ⋃ K \underset{1-1 onto}{⟶} ⋃ J$
17		f1ofn	$⊢ f^{-1} : ⋃ K \underset{1-1 onto}{⟶} ⋃ J \to f^{-1} Fn ⋃ K$
18	15 16 17	3syl	$⊢ ((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \to f^{-1} Fn ⋃ K$
19		elssuni	$⊢ x \in K \to x \subseteq ⋃ K$
20	19	ad2antrl	$⊢ ((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \to x \subseteq ⋃ K$
21		simprr	$⊢ ((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \to y \in x$
22		fnfvima	$⊢ (f^{-1} Fn ⋃ K \land x \subseteq ⋃ K \land y \in x) \to f^{-1} (y) \in f^{-1} [x]$
23	18 20 21 22	syl3anc	$⊢ ((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \to f^{-1} (y) \in f^{-1} [x]$
24		regsep	$⊢ (J \in Reg \land f^{-1} [x] \in J \land f^{-1} (y) \in f^{-1} [x]) \to \exists w \in J (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x])$
25	7 11 23 24	syl3anc	$⊢ ((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \to \exists w \in J (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x])$
26		simpllr	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to f \in (J Homeo K)$
27		simprl	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to w \in J$
28		hmeoima	$⊢ (f \in (J Homeo K) \land w \in J) \to f [w] \in K$
29	26 27 28	syl2anc	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to f [w] \in K$
30	20 21	sseldd	$⊢ ((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \to y \in ⋃ K$
31	30	adantr	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to y \in ⋃ K$
32		simprrl	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to f^{-1} (y) \in w$
33	18	adantr	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to f^{-1} Fn ⋃ K$
34		elpreima	$⊢ f^{-1} Fn ⋃ K \to (y \in {f^{-1}}^{-1} [w] \leftrightarrow (y \in ⋃ K \land f^{-1} (y) \in w))$
35	33 34	syl	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to (y \in {f^{-1}}^{-1} [w] \leftrightarrow (y \in ⋃ K \land f^{-1} (y) \in w))$
36	31 32 35	mpbir2and	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to y \in {f^{-1}}^{-1} [w]$
37		imacnvcnv	$⊢ {f^{-1}}^{-1} [w] = f [w]$
38	36 37	eleqtrdi	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to y \in f [w]$
39		elssuni	$⊢ w \in J \to w \subseteq ⋃ J$
40	39	ad2antrl	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to w \subseteq ⋃ J$
41	12	hmeocls	$⊢ (f \in (J Homeo K) \land w \subseteq ⋃ J) \to cls (K) (f [w]) = f [cls (J) (w)]$
42	26 40 41	syl2anc	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to cls (K) (f [w]) = f [cls (J) (w)]$
43		simprrr	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to cls (J) (w) \subseteq f^{-1} [x]$
44	15	adantr	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to f : ⋃ J \underset{1-1 onto}{⟶} ⋃ K$
45		f1ofun	$⊢ f : ⋃ J \underset{1-1 onto}{⟶} ⋃ K \to Fun f$
46	44 45	syl	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to Fun f$
47	7	adantr	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to J \in Reg$
48		regtop	$⊢ J \in Reg \to J \in Top$
49	47 48	syl	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to J \in Top$
50	12	clsss3	$⊢ (J \in Top \land w \subseteq ⋃ J) \to cls (J) (w) \subseteq ⋃ J$
51	49 40 50	syl2anc	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in 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	44 52	syl	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to dom f = ⋃ J$
54	51 53	sseqtrrd	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in 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	46 54 55	syl2anc	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in 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	43 56	mpbird	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to f [cls (J) (w)] \subseteq x$
58	42 57	eqsstrd	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to cls (K) (f [w]) \subseteq x$
59		eleq2	$⊢ z = f [w] \to (y \in z \leftrightarrow y \in 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 \in z \land cls (K) (z) \subseteq x) \leftrightarrow (y \in f [w] \land cls (K) (f [w]) \subseteq x))$
63	62	rspcev	$⊢ (f [w] \in K \land (y \in f [w] \land cls (K) (f [w]) \subseteq x)) \to \exists z \in K (y \in z \land cls (K) (z) \subseteq x)$
64	29 38 58 63	syl12anc	$⊢ (((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \land (w \in J \land (f^{-1} (y) \in w \land cls (J) (w) \subseteq f^{-1} [x]))) \to \exists z \in K (y \in z \land cls (K) (z) \subseteq x)$
65	25 64	rexlimddv	$⊢ ((J \in Reg \land f \in (J Homeo K)) \land (x \in K \land y \in x)) \to \exists z \in K (y \in z \land cls (K) (z) \subseteq x)$
66	65	ralrimivva	$⊢ (J \in Reg \land f \in (J Homeo K)) \to \forall x \in K \forall y \in x \exists z \in K (y \in z \land cls (K) (z) \subseteq x)$
67		isreg	$⊢ K \in Reg \leftrightarrow (K \in Top \land \forall x \in K \forall y \in x \exists z \in K (y \in z \land cls (K) (z) \subseteq x))$
68	6 66 67	sylanbrc	$⊢ (J \in Reg \land f \in (J Homeo K)) \to K \in Reg$
69	68	expcom	$⊢ f \in (J Homeo K) \to (J \in Reg \to K \in Reg)$
70	69	exlimiv	$⊢ \exists f f \in (J Homeo K) \to (J \in Reg \to K \in Reg)$
71	2 70	sylbi	$⊢ J Homeo K \neq \emptyset \to (J \in Reg \to K \in Reg)$
72	1 71	sylbi	$⊢ J ≃ K \to (J \in Reg \to K \in Reg)$

Metamath Proof Explorer

Theorem reghmph

Proof