hmeontr

Description: Homeomorphisms preserve interiors. (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Hypothesis	hmeoopn.1	$⊢ X = ⋃ J$
	Assertion	hmeontr	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to int (K) (F [A]) = F [int (J) (A)]$

Proof

Step	Hyp	Ref	Expression
1		hmeoopn.1	$⊢ X = ⋃ J$
2		hmeocn	$⊢ F \in (J Homeo K) \to F \in (J Cn K)$
3	2	adantr	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to F \in (J Cn K)$
4		imassrn	$⊢ F [A] \subseteq ran F$
5		eqid	$⊢ ⋃ K = ⋃ K$
6	1 5	hmeof1o	$⊢ F \in (J Homeo K) \to F : X \underset{1-1 onto}{⟶} ⋃ K$
7	6	adantr	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to F : X \underset{1-1 onto}{⟶} ⋃ K$
8		f1ofo	$⊢ F : X \underset{1-1 onto}{⟶} ⋃ K \to F : X \underset{onto}{⟶} ⋃ K$
9		forn	$⊢ F : X \underset{onto}{⟶} ⋃ K \to ran F = ⋃ K$
10	7 8 9	3syl	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to ran F = ⋃ K$
11	4 10	sseqtrid	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to F [A] \subseteq ⋃ K$
12	5	cnntri	$⊢ (F \in (J Cn K) \land F [A] \subseteq ⋃ K) \to F^{-1} [int (K) (F [A])] \subseteq int (J) (F^{-1} [F [A]])$
13	3 11 12	syl2anc	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to F^{-1} [int (K) (F [A])] \subseteq int (J) (F^{-1} [F [A]])$
14		f1of1	$⊢ F : X \underset{1-1 onto}{⟶} ⋃ K \to F : X \underset{1-1}{⟶} ⋃ K$
15	7 14	syl	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to F : X \underset{1-1}{⟶} ⋃ K$
16		f1imacnv	$⊢ (F : X \underset{1-1}{⟶} ⋃ K \land A \subseteq X) \to F^{-1} [F [A]] = A$
17	15 16	sylancom	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to F^{-1} [F [A]] = A$
18	17	fveq2d	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to int (J) (F^{-1} [F [A]]) = int (J) (A)$
19	13 18	sseqtrd	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to F^{-1} [int (K) (F [A])] \subseteq int (J) (A)$
20		f1ofun	$⊢ F : X \underset{1-1 onto}{⟶} ⋃ K \to Fun F$
21	7 20	syl	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to Fun F$
22		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
23	3 22	syl	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to K \in Top$
24	5	ntrss3	$⊢ (K \in Top \land F [A] \subseteq ⋃ K) \to int (K) (F [A]) \subseteq ⋃ K$
25	23 11 24	syl2anc	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to int (K) (F [A]) \subseteq ⋃ K$
26	25 10	sseqtrrd	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to int (K) (F [A]) \subseteq ran F$
27		funimass1	$⊢ (Fun F \land int (K) (F [A]) \subseteq ran F) \to (F^{-1} [int (K) (F [A])] \subseteq int (J) (A) \to int (K) (F [A]) \subseteq F [int (J) (A)])$
28	21 26 27	syl2anc	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to (F^{-1} [int (K) (F [A])] \subseteq int (J) (A) \to int (K) (F [A]) \subseteq F [int (J) (A)])$
29	19 28	mpd	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to int (K) (F [A]) \subseteq F [int (J) (A)]$
30		hmeocnvcn	$⊢ F \in (J Homeo K) \to F^{-1} \in (K Cn J)$
31	1	cnntri	$⊢ (F^{-1} \in (K Cn J) \land A \subseteq X) \to {F^{-1}}^{-1} [int (J) (A)] \subseteq int (K) ({F^{-1}}^{-1} [A])$
32	30 31	sylan	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to {F^{-1}}^{-1} [int (J) (A)] \subseteq int (K) ({F^{-1}}^{-1} [A])$
33		imacnvcnv	$⊢ {F^{-1}}^{-1} [int (J) (A)] = F [int (J) (A)]$
34		imacnvcnv	$⊢ {F^{-1}}^{-1} [A] = F [A]$
35	34	fveq2i	$⊢ int (K) ({F^{-1}}^{-1} [A]) = int (K) (F [A])$
36	32 33 35	3sstr3g	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to F [int (J) (A)] \subseteq int (K) (F [A])$
37	29 36	eqssd	$⊢ (F \in (J Homeo K) \land A \subseteq X) \to int (K) (F [A]) = F [int (J) (A)]$

Metamath Proof Explorer

Theorem hmeontr

Proof