hmeof1o

Description: A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007) (Revised by Mario Carneiro, 30-May-2014)

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

Step	Hyp	Ref	Expression
1		hmeof1o.1	$⊢ X = ⋃ J$
2		hmeof1o.2	$⊢ Y = ⋃ K$
3		hmeocn	$⊢ F \in (J Homeo K) \to F \in (J Cn K)$
4		cntop1	$⊢ F \in (J Cn K) \to J \in Top$
5	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
6	4 5	sylib	$⊢ F \in (J Cn K) \to J \in TopOn (X)$
7		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
8	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (Y)$
9	7 8	sylib	$⊢ F \in (J Cn K) \to K \in TopOn (Y)$
10	6 9	jca	$⊢ F \in (J Cn K) \to (J \in TopOn (X) \land K \in TopOn (Y))$
11	3 10	syl	$⊢ F \in (J Homeo K) \to (J \in TopOn (X) \land K \in TopOn (Y))$
12		hmeof1o2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J Homeo K)) \to F : X \underset{1-1 onto}{⟶} Y$
13	12	3expia	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Homeo K) \to F : X \underset{1-1 onto}{⟶} Y)$
14	11 13	mpcom	$⊢ F \in (J Homeo K) \to F : X \underset{1-1 onto}{⟶} Y$

Metamath Proof Explorer