hmeoimaf1o

Description: The function mapping open sets to their images under a homeomorphism is a bijection of topologies. (Contributed by Mario Carneiro, 10-Sep-2015)

		Ref	Expression
	Hypothesis	hmeoimaf1o.1	$⊢ G = (x \in J ⟼ F [x])$
	Assertion	hmeoimaf1o	$⊢ F \in (J Homeo K) \to G : J \underset{1-1 onto}{⟶} K$

Proof

Step	Hyp	Ref	Expression
1		hmeoimaf1o.1	$⊢ G = (x \in J ⟼ F [x])$
2		hmeoima	$⊢ (F \in (J Homeo K) \land x \in J) \to F [x] \in K$
3		hmeocn	$⊢ F \in (J Homeo K) \to F \in (J Cn K)$
4		cnima	$⊢ (F \in (J Cn K) \land y \in K) \to F^{-1} [y] \in J$
5	3 4	sylan	$⊢ (F \in (J Homeo K) \land y \in K) \to F^{-1} [y] \in J$
6		eqid	$⊢ ⋃ J = ⋃ J$
7		eqid	$⊢ ⋃ K = ⋃ K$
8	6 7	hmeof1o	$⊢ F \in (J Homeo K) \to F : ⋃ J \underset{1-1 onto}{⟶} ⋃ K$
9	8	adantr	$⊢ (F \in (J Homeo K) \land (x \in J \land y \in K)) \to F : ⋃ J \underset{1-1 onto}{⟶} ⋃ K$
10		f1of1	$⊢ F : ⋃ J \underset{1-1 onto}{⟶} ⋃ K \to F : ⋃ J \underset{1-1}{⟶} ⋃ K$
11	9 10	syl	$⊢ (F \in (J Homeo K) \land (x \in J \land y \in K)) \to F : ⋃ J \underset{1-1}{⟶} ⋃ K$
12		elssuni	$⊢ x \in J \to x \subseteq ⋃ J$
13	12	ad2antrl	$⊢ (F \in (J Homeo K) \land (x \in J \land y \in K)) \to x \subseteq ⋃ J$
14		cnvimass	$⊢ F^{-1} [y] \subseteq dom F$
15		f1dm	$⊢ F : ⋃ J \underset{1-1}{⟶} ⋃ K \to dom F = ⋃ J$
16	11 15	syl	$⊢ (F \in (J Homeo K) \land (x \in J \land y \in K)) \to dom F = ⋃ J$
17	14 16	sseqtrid	$⊢ (F \in (J Homeo K) \land (x \in J \land y \in K)) \to F^{-1} [y] \subseteq ⋃ J$
18		f1imaeq	$⊢ (F : ⋃ J \underset{1-1}{⟶} ⋃ K \land (x \subseteq ⋃ J \land F^{-1} [y] \subseteq ⋃ J)) \to (F [x] = F [F^{-1} [y]] \leftrightarrow x = F^{-1} [y])$
19	11 13 17 18	syl12anc	$⊢ (F \in (J Homeo K) \land (x \in J \land y \in K)) \to (F [x] = F [F^{-1} [y]] \leftrightarrow x = F^{-1} [y])$
20		f1ofo	$⊢ F : ⋃ J \underset{1-1 onto}{⟶} ⋃ K \to F : ⋃ J \underset{onto}{⟶} ⋃ K$
21	9 20	syl	$⊢ (F \in (J Homeo K) \land (x \in J \land y \in K)) \to F : ⋃ J \underset{onto}{⟶} ⋃ K$
22		elssuni	$⊢ y \in K \to y \subseteq ⋃ K$
23	22	ad2antll	$⊢ (F \in (J Homeo K) \land (x \in J \land y \in K)) \to y \subseteq ⋃ K$
24		foimacnv	$⊢ (F : ⋃ J \underset{onto}{⟶} ⋃ K \land y \subseteq ⋃ K) \to F [F^{-1} [y]] = y$
25	21 23 24	syl2anc	$⊢ (F \in (J Homeo K) \land (x \in J \land y \in K)) \to F [F^{-1} [y]] = y$
26	25	eqeq2d	$⊢ (F \in (J Homeo K) \land (x \in J \land y \in K)) \to (F [x] = F [F^{-1} [y]] \leftrightarrow F [x] = y)$
27		eqcom	$⊢ F [x] = y \leftrightarrow y = F [x]$
28	26 27	bitrdi	$⊢ (F \in (J Homeo K) \land (x \in J \land y \in K)) \to (F [x] = F [F^{-1} [y]] \leftrightarrow y = F [x])$
29	19 28	bitr3d	$⊢ (F \in (J Homeo K) \land (x \in J \land y \in K)) \to (x = F^{-1} [y] \leftrightarrow y = F [x])$
30	1 2 5 29	f1o2d	$⊢ F \in (J Homeo K) \to G : J \underset{1-1 onto}{⟶} K$

Metamath Proof Explorer

Theorem hmeoimaf1o

Proof