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 ⊢ φ → K ∈ TopOn ⁡ Y
qtopomap.5 ⊢ φ → F ∈ J Cn K
qtopomap.6 ⊢ φ → ran ⁡ F = Y
qtopomap.7 ⊢ φ ∧ x ∈ J → F x ∈ K
Assertion qtopomap ⊢ φ → K = J qTop F

Proof

Step Hyp Ref Expression
1 qtopomap.4 ⊢ φ → K ∈ TopOn ⁡ Y
2 qtopomap.5 ⊢ φ → F ∈ J Cn K
3 qtopomap.6 ⊢ φ → ran ⁡ F = Y
4 qtopomap.7 ⊢ φ ∧ x ∈ J → F x ∈ K
5 qtopss ⊢ F ∈ J Cn K ∧ K ∈ TopOn ⁡ Y ∧ ran ⁡ F = Y → K ⊆ J qTop F
6 2 1 3 5 syl3anc ⊢ φ → K ⊆ J qTop F
7 cntop1 ⊢ F ∈ J Cn K → J ∈ Top
8 2 7 syl ⊢ φ → J ∈ Top
9 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
10 8 9 sylib ⊢ φ → J ∈ TopOn ⁡ ⋃ J
11 cnf2 ⊢ J ∈ TopOn ⁡ ⋃ J ∧ K ∈ TopOn ⁡ Y ∧ F ∈ J Cn K → F : ⋃ J ⟶ Y
12 10 1 2 11 syl3anc ⊢ φ → F : ⋃ J ⟶ Y
13 12 ffnd ⊢ φ → F Fn ⋃ J
14 df-fo ⊢ F : ⋃ J ⟶ onto Y ↔ F Fn ⋃ J ∧ ran ⁡ F = Y
15 13 3 14 sylanbrc ⊢ φ → F : ⋃ J ⟶ onto Y
16 elqtop3 ⊢ J ∈ TopOn ⁡ ⋃ J ∧ F : ⋃ J ⟶ onto Y → y ∈ J qTop F ↔ y ⊆ Y ∧ F -1 y ∈ J
17 10 15 16 syl2anc ⊢ φ → y ∈ J qTop F ↔ y ⊆ Y ∧ F -1 y ∈ J
18 foimacnv ⊢ F : ⋃ J ⟶ onto Y ∧ y ⊆ Y → F F -1 y = y
19 15 18 sylan ⊢ φ ∧ y ⊆ Y → F F -1 y = y
20 19 adantrr ⊢ φ ∧ y ⊆ Y ∧ F -1 y ∈ J → F F -1 y = y
21 imaeq2 ⊢ x = F -1 y → F x = F F -1 y
22 21 eleq1d ⊢ x = F -1 y → F x ∈ K ↔ F F -1 y ∈ K
23 4 ralrimiva ⊢ φ → ∀ x ∈ J F x ∈ K
24 23 adantr ⊢ φ ∧ y ⊆ Y ∧ F -1 y ∈ J → ∀ x ∈ J F x ∈ K
25 simprr ⊢ φ ∧ y ⊆ Y ∧ F -1 y ∈ J → F -1 y ∈ J
26 22 24 25 rspcdva ⊢ φ ∧ y ⊆ Y ∧ F -1 y ∈ J → F F -1 y ∈ K
27 20 26 eqeltrrd ⊢ φ ∧ y ⊆ Y ∧ F -1 y ∈ J → y ∈ K
28 27 ex ⊢ φ → y ⊆ Y ∧ F -1 y ∈ J → y ∈ K
29 17 28 sylbid ⊢ φ → y ∈ J qTop F → y ∈ K
30 29 ssrdv ⊢ φ → J qTop F ⊆ K
31 6 30 eqssd ⊢ φ → K = J qTop F