cmphaushmeo

Description: A continuous bijection from a compact space to a Hausdorff space is a homeomorphism. (Contributed by Mario Carneiro, 17-Feb-2015)

	Ref	Expression
Hypotheses	cmphaushmeo.1	$⊢ X = ⋃ J$
	cmphaushmeo.2	$⊢ Y = ⋃ K$
Assertion	cmphaushmeo	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to (F \in (J Homeo K) \leftrightarrow F : X \underset{1-1 onto}{⟶} Y)$

Proof

Step	Hyp	Ref	Expression
1		cmphaushmeo.1	$⊢ X = ⋃ J$
2		cmphaushmeo.2	$⊢ Y = ⋃ K$
3	1 2	hmeof1o	$⊢ F \in (J Homeo K) \to F : X \underset{1-1 onto}{⟶} Y$
4		f1ocnv	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F^{-1} : Y \underset{1-1 onto}{⟶} X$
5		f1of	$⊢ F^{-1} : Y \underset{1-1 onto}{⟶} X \to F^{-1} : Y ⟶ X$
6	4 5	syl	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F^{-1} : Y ⟶ X$
7	6	a1i	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to (F : X \underset{1-1 onto}{⟶} Y \to F^{-1} : Y ⟶ X)$
8		f1orel	$⊢ F : X \underset{1-1 onto}{⟶} Y \to Rel F$
9	8	ad2antll	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land (x \in Clsd (J) \land F : X \underset{1-1 onto}{⟶} Y)) \to Rel F$
10		dfrel2	$⊢ Rel F \leftrightarrow {F^{-1}}^{-1} = F$
11	9 10	sylib	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land (x \in Clsd (J) \land F : X \underset{1-1 onto}{⟶} Y)) \to {F^{-1}}^{-1} = F$
12	11	imaeq1d	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land (x \in Clsd (J) \land F : X \underset{1-1 onto}{⟶} Y)) \to {F^{-1}}^{-1} [x] = F [x]$
13		simp2	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to K \in Haus$
14	13	adantr	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land (x \in Clsd (J) \land F : X \underset{1-1 onto}{⟶} Y)) \to K \in Haus$
15		imassrn	$⊢ F [x] \subseteq ran F$
16		f1ofo	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F : X \underset{onto}{⟶} Y$
17	16	ad2antll	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land (x \in Clsd (J) \land F : X \underset{1-1 onto}{⟶} Y)) \to F : X \underset{onto}{⟶} Y$
18		forn	$⊢ F : X \underset{onto}{⟶} Y \to ran F = Y$
19	17 18	syl	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land (x \in Clsd (J) \land F : X \underset{1-1 onto}{⟶} Y)) \to ran F = Y$
20	15 19	sseqtrid	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land (x \in Clsd (J) \land F : X \underset{1-1 onto}{⟶} Y)) \to F [x] \subseteq Y$
21		simpl3	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land (x \in Clsd (J) \land F : X \underset{1-1 onto}{⟶} Y)) \to F \in (J Cn K)$
22		simp1	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to J \in Comp$
23	22	adantr	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land (x \in Clsd (J) \land F : X \underset{1-1 onto}{⟶} Y)) \to J \in Comp$
24		simprl	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land (x \in Clsd (J) \land F : X \underset{1-1 onto}{⟶} Y)) \to x \in Clsd (J)$
25		cmpcld	$⊢ (J \in Comp \land x \in Clsd (J)) \to J ↾_{𝑡} x \in Comp$
26	23 24 25	syl2anc	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land (x \in Clsd (J) \land F : X \underset{1-1 onto}{⟶} Y)) \to J ↾_{𝑡} x \in Comp$
27		imacmp	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} x \in Comp) \to K ↾_{𝑡} F [x] \in Comp$
28	21 26 27	syl2anc	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land (x \in Clsd (J) \land F : X \underset{1-1 onto}{⟶} Y)) \to K ↾_{𝑡} F [x] \in Comp$
29	2	hauscmp	$⊢ (K \in Haus \land F [x] \subseteq Y \land K ↾_{𝑡} F [x] \in Comp) \to F [x] \in Clsd (K)$
30	14 20 28 29	syl3anc	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land (x \in Clsd (J) \land F : X \underset{1-1 onto}{⟶} Y)) \to F [x] \in Clsd (K)$
31	12 30	eqeltrd	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land (x \in Clsd (J) \land F : X \underset{1-1 onto}{⟶} Y)) \to {F^{-1}}^{-1} [x] \in Clsd (K)$
32	31	expr	$⊢ ((J \in Comp \land K \in Haus \land F \in (J Cn K)) \land x \in Clsd (J)) \to (F : X \underset{1-1 onto}{⟶} Y \to {F^{-1}}^{-1} [x] \in Clsd (K))$
33	32	ralrimdva	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to (F : X \underset{1-1 onto}{⟶} Y \to \forall x \in Clsd (J) {F^{-1}}^{-1} [x] \in Clsd (K))$
34	7 33	jcad	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to (F : X \underset{1-1 onto}{⟶} Y \to (F^{-1} : Y ⟶ X \land \forall x \in Clsd (J) {F^{-1}}^{-1} [x] \in Clsd (K)))$
35		haustop	$⊢ K \in Haus \to K \in Top$
36	13 35	syl	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to K \in Top$
37	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (Y)$
38	36 37	sylib	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to K \in TopOn (Y)$
39		cmptop	$⊢ J \in Comp \to J \in Top$
40	22 39	syl	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to J \in Top$
41	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
42	40 41	sylib	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to J \in TopOn (X)$
43		iscncl	$⊢ (K \in TopOn (Y) \land J \in TopOn (X)) \to (F^{-1} \in (K Cn J) \leftrightarrow (F^{-1} : Y ⟶ X \land \forall x \in Clsd (J) {F^{-1}}^{-1} [x] \in Clsd (K)))$
44	38 42 43	syl2anc	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to (F^{-1} \in (K Cn J) \leftrightarrow (F^{-1} : Y ⟶ X \land \forall x \in Clsd (J) {F^{-1}}^{-1} [x] \in Clsd (K)))$
45	34 44	sylibrd	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to (F : X \underset{1-1 onto}{⟶} Y \to F^{-1} \in (K Cn J))$
46		simp3	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to F \in (J Cn K)$
47	45 46	jctild	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to (F : X \underset{1-1 onto}{⟶} Y \to (F \in (J Cn K) \land F^{-1} \in (K Cn J)))$
48		ishmeo	$⊢ F \in (J Homeo K) \leftrightarrow (F \in (J Cn K) \land F^{-1} \in (K Cn J))$
49	47 48	imbitrrdi	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to (F : X \underset{1-1 onto}{⟶} Y \to F \in (J Homeo K))$
50	3 49	impbid2	$⊢ (J \in Comp \land K \in Haus \land F \in (J Cn K)) \to (F \in (J Homeo K) \leftrightarrow F : X \underset{1-1 onto}{⟶} Y)$

Metamath Proof Explorer

Theorem cmphaushmeo

Proof