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 
|- ( ph -> K e. ( TopOn ` Y ) )
qtopomap.5 
|- ( ph -> F e. ( J Cn K ) )
qtopomap.6 
|- ( ph -> ran F = Y )
qtopcmap.7 
|- ( ( ph /\ x e. ( Clsd ` J ) ) -> ( F " x ) e. ( Clsd ` K ) )
Assertion qtopcmap 
|- ( ph -> K = ( J qTop F ) )

Proof

Step Hyp Ref Expression
1 qtopomap.4 
 |-  ( ph -> K e. ( TopOn ` Y ) )
2 qtopomap.5 
 |-  ( ph -> F e. ( J Cn K ) )
3 qtopomap.6 
 |-  ( ph -> ran F = Y )
4 qtopcmap.7 
 |-  ( ( ph /\ x e. ( Clsd ` J ) ) -> ( F " x ) e. ( Clsd ` K ) )
5 qtopss 
 |-  ( ( F e. ( J Cn K ) /\ K e. ( TopOn ` Y ) /\ ran F = Y ) -> K C_ ( J qTop F ) )
6 2 1 3 5 syl3anc 
 |-  ( ph -> K C_ ( J qTop F ) )
7 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
8 2 7 syl 
 |-  ( ph -> J e. Top )
9 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
10 8 9 sylib 
 |-  ( ph -> J e. ( TopOn ` U. J ) )
11 cnf2 
 |-  ( ( J e. ( TopOn ` U. J ) /\ K e. ( TopOn ` Y ) /\ F e. ( J Cn K ) ) -> F : U. J --> Y )
12 10 1 2 11 syl3anc 
 |-  ( ph -> F : U. J --> Y )
13 12 ffnd 
 |-  ( ph -> F Fn U. J )
14 df-fo 
 |-  ( F : U. J -onto-> Y <-> ( F Fn U. J /\ ran F = Y ) )
15 13 3 14 sylanbrc 
 |-  ( ph -> F : U. J -onto-> Y )
16 eqid 
 |-  U. J = U. J
17 16 elqtop2 
 |-  ( ( J e. Top /\ F : U. J -onto-> Y ) -> ( y e. ( J qTop F ) <-> ( y C_ Y /\ ( `' F " y ) e. J ) ) )
18 8 15 17 syl2anc 
 |-  ( ph -> ( y e. ( J qTop F ) <-> ( y C_ Y /\ ( `' F " y ) e. J ) ) )
19 15 adantr 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> F : U. J -onto-> Y )
20 difss 
 |-  ( Y \ y ) C_ Y
21 foimacnv 
 |-  ( ( F : U. J -onto-> Y /\ ( Y \ y ) C_ Y ) -> ( F " ( `' F " ( Y \ y ) ) ) = ( Y \ y ) )
22 19 20 21 sylancl 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( F " ( `' F " ( Y \ y ) ) ) = ( Y \ y ) )
23 1 adantr 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> K e. ( TopOn ` Y ) )
24 toponuni 
 |-  ( K e. ( TopOn ` Y ) -> Y = U. K )
25 23 24 syl 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> Y = U. K )
26 25 difeq1d 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( Y \ y ) = ( U. K \ y ) )
27 22 26 eqtrd 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( F " ( `' F " ( Y \ y ) ) ) = ( U. K \ y ) )
28 imaeq2 
 |-  ( x = ( `' F " ( Y \ y ) ) -> ( F " x ) = ( F " ( `' F " ( Y \ y ) ) ) )
29 28 eleq1d 
 |-  ( x = ( `' F " ( Y \ y ) ) -> ( ( F " x ) e. ( Clsd ` K ) <-> ( F " ( `' F " ( Y \ y ) ) ) e. ( Clsd ` K ) ) )
30 4 ralrimiva 
 |-  ( ph -> A. x e. ( Clsd ` J ) ( F " x ) e. ( Clsd ` K ) )
31 30 adantr 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> A. x e. ( Clsd ` J ) ( F " x ) e. ( Clsd ` K ) )
32 fofun 
 |-  ( F : U. J -onto-> Y -> Fun F )
33 funcnvcnv 
 |-  ( Fun F -> Fun `' `' F )
34 imadif 
 |-  ( Fun `' `' F -> ( `' F " ( Y \ y ) ) = ( ( `' F " Y ) \ ( `' F " y ) ) )
35 19 32 33 34 4syl 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( `' F " ( Y \ y ) ) = ( ( `' F " Y ) \ ( `' F " y ) ) )
36 12 adantr 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> F : U. J --> Y )
37 fimacnv 
 |-  ( F : U. J --> Y -> ( `' F " Y ) = U. J )
38 36 37 syl 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( `' F " Y ) = U. J )
39 38 difeq1d 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( ( `' F " Y ) \ ( `' F " y ) ) = ( U. J \ ( `' F " y ) ) )
40 35 39 eqtrd 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( `' F " ( Y \ y ) ) = ( U. J \ ( `' F " y ) ) )
41 8 adantr 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> J e. Top )
42 simprr 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( `' F " y ) e. J )
43 16 opncld 
 |-  ( ( J e. Top /\ ( `' F " y ) e. J ) -> ( U. J \ ( `' F " y ) ) e. ( Clsd ` J ) )
44 41 42 43 syl2anc 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( U. J \ ( `' F " y ) ) e. ( Clsd ` J ) )
45 40 44 eqeltrd 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( `' F " ( Y \ y ) ) e. ( Clsd ` J ) )
46 29 31 45 rspcdva 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( F " ( `' F " ( Y \ y ) ) ) e. ( Clsd ` K ) )
47 27 46 eqeltrrd 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( U. K \ y ) e. ( Clsd ` K ) )
48 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
49 23 48 syl 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> K e. Top )
50 simprl 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> y C_ Y )
51 50 25 sseqtrd 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> y C_ U. K )
52 eqid 
 |-  U. K = U. K
53 52 isopn2 
 |-  ( ( K e. Top /\ y C_ U. K ) -> ( y e. K <-> ( U. K \ y ) e. ( Clsd ` K ) ) )
54 49 51 53 syl2anc 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( y e. K <-> ( U. K \ y ) e. ( Clsd ` K ) ) )
55 47 54 mpbird 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> y e. K )
56 55 ex 
 |-  ( ph -> ( ( y C_ Y /\ ( `' F " y ) e. J ) -> y e. K ) )
57 18 56 sylbid 
 |-  ( ph -> ( y e. ( J qTop F ) -> y e. K ) )
58 57 ssrdv 
 |-  ( ph -> ( J qTop F ) C_ K )
59 6 58 eqssd 
 |-  ( ph -> K = ( J qTop F ) )