Metamath Proof Explorer

Theorem qtopf1

Description: If a quotient map is injective, then it is a homeomorphism. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypotheses qtopf1.1 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
qtopf1.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 –1-1→ 𝑌 )
Assertion qtopf1 ( 𝜑 → 𝐹 ∈ ( 𝐽 Homeo ( 𝐽 qTop 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 qtopf1.1 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 qtopf1.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 –1-1→ 𝑌 )
3 f1fn ⊢ ( 𝐹 : 𝑋 –1-1→ 𝑌 → 𝐹 Fn 𝑋 )
4 2 3 syl ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
5 qtopid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )
6 1 4 5 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )
7 f1f1orn ⊢ ( 𝐹 : 𝑋 –1-1→ 𝑌 → 𝐹 : 𝑋 –1-1-onto→ ran 𝐹 )
8 f1ocnv ⊢ ( 𝐹 : 𝑋 –1-1-onto→ ran 𝐹 → ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝑋 )
9 f1of ⊢ ( ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝑋 → ◡ 𝐹 : ran 𝐹 ⟶ 𝑋 )
10 2 7 8 9 4syl ⊢ ( 𝜑 → ◡ 𝐹 : ran 𝐹 ⟶ 𝑋 )
11 imacnvcnv ⊢ ( ◡ ◡ 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑥 )
12 imassrn ⊢ ( 𝐹 “ 𝑥 ) ⊆ ran 𝐹
13 12 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ 𝑥 ) ⊆ ran 𝐹 )
14 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝐹 : 𝑋 –1-1→ 𝑌 )
15 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ⊆ 𝑋 )
16 1 15 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ⊆ 𝑋 )
17 f1imacnv ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝑥 ⊆ 𝑋 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) = 𝑥 )
18 14 16 17 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) = 𝑥 )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝐽 )
20 18 19 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) ∈ 𝐽 )
21 dffn4 ⊢ ( 𝐹 Fn 𝑋 ↔ 𝐹 : 𝑋 –onto→ ran 𝐹 )
22 4 21 sylib ⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ ran 𝐹 )
23 elqtop3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ ran 𝐹 ) → ( ( 𝐹 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝐹 “ 𝑥 ) ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) ∈ 𝐽 ) ) )
24 1 22 23 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝐹 “ 𝑥 ) ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) ∈ 𝐽 ) ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝐹 “ 𝑥 ) ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑥 ) ) ∈ 𝐽 ) ) )
26 13 20 25 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) )
27 11 26 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( ◡ ◡ 𝐹 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) )
28 27 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐽 ( ◡ ◡ 𝐹 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) )
29 qtoptopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ ran 𝐹 ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ ran 𝐹 ) )
30 1 22 29 syl2anc ⊢ ( 𝜑 → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ ran 𝐹 ) )
31 iscn ⊢ ( ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ ran 𝐹 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( ◡ 𝐹 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐽 ) ↔ ( ◡ 𝐹 : ran 𝐹 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( ◡ ◡ 𝐹 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ) ) )
32 30 1 31 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐽 ) ↔ ( ◡ 𝐹 : ran 𝐹 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( ◡ ◡ 𝐹 “ 𝑥 ) ∈ ( 𝐽 qTop 𝐹 ) ) ) )
33 10 28 32 mpbir2and ⊢ ( 𝜑 → ◡ 𝐹 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐽 ) )
34 ishmeo ⊢ ( 𝐹 ∈ ( 𝐽 Homeo ( 𝐽 qTop 𝐹 ) ) ↔ ( 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) ∧ ◡ 𝐹 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐽 ) ) )
35 6 33 34 sylanbrc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Homeo ( 𝐽 qTop 𝐹 ) ) )