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 𝐹 ) )