Metamath Proof Explorer

Theorem qtopomap

Description: If F is a surjective continuous open map, then it is a quotient map. (An open map is a function that maps open sets to open sets.) (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypotheses qtopomap.4 ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
qtopomap.5 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
qtopomap.6 ⊢ ( 𝜑 → ran 𝐹 = 𝑌 )
qtopomap.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ 𝑥 ) ∈ 𝐾 )
Assertion qtopomap ( 𝜑 → 𝐾 = ( 𝐽 qTop 𝐹 ) )

Proof

Step Hyp Ref Expression
1 qtopomap.4 ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
2 qtopomap.5 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3 qtopomap.6 ⊢ ( 𝜑 → ran 𝐹 = 𝑌 )
4 qtopomap.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ 𝑥 ) ∈ 𝐾 )
5 qtopss ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) → 𝐾 ⊆ ( 𝐽 qTop 𝐹 ) )
6 2 1 3 5 syl3anc ⊢ ( 𝜑 → 𝐾 ⊆ ( 𝐽 qTop 𝐹 ) )
7 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
8 2 7 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
9 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
10 8 9 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
11 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
12 10 1 2 11 syl3anc ⊢ ( 𝜑 → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
13 12 ffnd ⊢ ( 𝜑 → 𝐹 Fn ∪ 𝐽 )
14 df-fo ⊢ ( 𝐹 : ∪ 𝐽 –onto→ 𝑌 ↔ ( 𝐹 Fn ∪ 𝐽 ∧ ran 𝐹 = 𝑌 ) )
15 13 3 14 sylanbrc ⊢ ( 𝜑 → 𝐹 : ∪ 𝐽 –onto→ 𝑌 )
16 elqtop3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐹 : ∪ 𝐽 –onto→ 𝑌 ) → ( 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
17 10 15 16 syl2anc ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
18 foimacnv ⊢ ( ( 𝐹 : ∪ 𝐽 –onto→ 𝑌 ∧ 𝑦 ⊆ 𝑌 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = 𝑦 )
19 15 18 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝑌 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = 𝑦 )
20 19 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = 𝑦 )
21 imaeq2 ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) )
22 21 eleq1d ⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( 𝐹 “ 𝑥 ) ∈ 𝐾 ↔ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ∈ 𝐾 ) )
23 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐽 ( 𝐹 “ 𝑥 ) ∈ 𝐾 )
24 23 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ∀ 𝑥 ∈ 𝐽 ( 𝐹 “ 𝑥 ) ∈ 𝐾 )
25 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
26 22 24 25 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ∈ 𝐾 )
27 20 26 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑦 ∈ 𝐾 )
28 27 ex ⊢ ( 𝜑 → ( ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) → 𝑦 ∈ 𝐾 ) )
29 17 28 sylbid ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐽 qTop 𝐹 ) → 𝑦 ∈ 𝐾 ) )
30 29 ssrdv ⊢ ( 𝜑 → ( 𝐽 qTop 𝐹 ) ⊆ 𝐾 )
31 6 30 eqssd ⊢ ( 𝜑 → 𝐾 = ( 𝐽 qTop 𝐹 ) )