This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qtopcmap

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

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

Proof

Step Hyp Ref Expression
1 qtopomap.4 ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
2 qtopomap.5 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3 qtopomap.6 ⊢ ( 𝜑 → ran 𝐹 = 𝑌 )
4 qtopcmap.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) )
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 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
17 16 elqtop2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 : ∪ 𝐽 –onto→ 𝑌 ) → ( 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
18 8 15 17 syl2anc ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
19 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝐹 : ∪ 𝐽 –onto→ 𝑌 )
20 difss ⊢ ( 𝑌 ∖ 𝑦 ) ⊆ 𝑌
21 foimacnv ⊢ ( ( 𝐹 : ∪ 𝐽 –onto→ 𝑌 ∧ ( 𝑌 ∖ 𝑦 ) ⊆ 𝑌 ) → ( 𝐹 “ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) ) = ( 𝑌 ∖ 𝑦 ) )
22 19 20 21 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) ) = ( 𝑌 ∖ 𝑦 ) )
23 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
24 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
25 23 24 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑌 = ∪ 𝐾 )
26 25 difeq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝑌 ∖ 𝑦 ) = ( ∪ 𝐾 ∖ 𝑦 ) )
27 22 26 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) ) = ( ∪ 𝐾 ∖ 𝑦 ) )
28 imaeq2 ⊢ ( 𝑥 = ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) ) )
29 28 eleq1d ⊢ ( 𝑥 = ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) → ( ( 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) ↔ ( 𝐹 “ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) ) ∈ ( Clsd ‘ 𝐾 ) ) )
30 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐾 ) )
32 fofun ⊢ ( 𝐹 : ∪ 𝐽 –onto→ 𝑌 → Fun 𝐹 )
33 funcnvcnv ⊢ ( Fun 𝐹 → Fun ◡ ◡ 𝐹 )
34 imadif ⊢ ( Fun ◡ ◡ 𝐹 → ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) = ( ( ◡ 𝐹 “ 𝑌 ) ∖ ( ◡ 𝐹 “ 𝑦 ) ) )
35 19 32 33 34 4syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) = ( ( ◡ 𝐹 “ 𝑌 ) ∖ ( ◡ 𝐹 “ 𝑦 ) ) )
36 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
37 fimacnv ⊢ ( 𝐹 : ∪ 𝐽 ⟶ 𝑌 → ( ◡ 𝐹 “ 𝑌 ) = ∪ 𝐽 )
38 36 37 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ 𝑌 ) = ∪ 𝐽 )
39 38 difeq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ( ◡ 𝐹 “ 𝑌 ) ∖ ( ◡ 𝐹 “ 𝑦 ) ) = ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝑦 ) ) )
40 35 39 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) = ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝑦 ) ) )
41 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝐽 ∈ Top )
42 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
43 16 opncld ⊢ ( ( 𝐽 ∈ Top ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) → ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝑦 ) ) ∈ ( Clsd ‘ 𝐽 ) )
44 41 42 43 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ∪ 𝐽 ∖ ( ◡ 𝐹 “ 𝑦 ) ) ∈ ( Clsd ‘ 𝐽 ) )
45 40 44 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) ∈ ( Clsd ‘ 𝐽 ) )
46 29 31 45 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ ( 𝑌 ∖ 𝑦 ) ) ) ∈ ( Clsd ‘ 𝐾 ) )
47 27 46 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ∪ 𝐾 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐾 ) )
48 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
49 23 48 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝐾 ∈ Top )
50 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑦 ⊆ 𝑌 )
51 50 25 sseqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑦 ⊆ ∪ 𝐾 )
52 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
53 52 isopn2 ⊢ ( ( 𝐾 ∈ Top ∧ 𝑦 ⊆ ∪ 𝐾 ) → ( 𝑦 ∈ 𝐾 ↔ ( ∪ 𝐾 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐾 ) ) )
54 49 51 53 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝑦 ∈ 𝐾 ↔ ( ∪ 𝐾 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐾 ) ) )
55 47 54 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑦 ∈ 𝐾 )
56 55 ex ⊢ ( 𝜑 → ( ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) → 𝑦 ∈ 𝐾 ) )
57 18 56 sylbid ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐽 qTop 𝐹 ) → 𝑦 ∈ 𝐾 ) )
58 57 ssrdv ⊢ ( 𝜑 → ( 𝐽 qTop 𝐹 ) ⊆ 𝐾 )
59 6 58 eqssd ⊢ ( 𝜑 → 𝐾 = ( 𝐽 qTop 𝐹 ) )