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 
|- ( ph -> K e. ( TopOn ` Y ) )
qtopomap.5 
|- ( ph -> F e. ( J Cn K ) )
qtopomap.6 
|- ( ph -> ran F = Y )
qtopomap.7 
|- ( ( ph /\ x e. J ) -> ( F " x ) e. K )
Assertion qtopomap 
|- ( 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 qtopomap.7 
 |-  ( ( ph /\ x e. J ) -> ( F " x ) e. 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 elqtop3 
 |-  ( ( J e. ( TopOn ` U. J ) /\ F : U. J -onto-> Y ) -> ( y e. ( J qTop F ) <-> ( y C_ Y /\ ( `' F " y ) e. J ) ) )
17 10 15 16 syl2anc 
 |-  ( ph -> ( y e. ( J qTop F ) <-> ( y C_ Y /\ ( `' F " y ) e. J ) ) )
18 foimacnv 
 |-  ( ( F : U. J -onto-> Y /\ y C_ Y ) -> ( F " ( `' F " y ) ) = y )
19 15 18 sylan 
 |-  ( ( ph /\ y C_ Y ) -> ( F " ( `' F " y ) ) = y )
20 19 adantrr 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( F " ( `' F " y ) ) = y )
21 imaeq2 
 |-  ( x = ( `' F " y ) -> ( F " x ) = ( F " ( `' F " y ) ) )
22 21 eleq1d 
 |-  ( x = ( `' F " y ) -> ( ( F " x ) e. K <-> ( F " ( `' F " y ) ) e. K ) )
23 4 ralrimiva 
 |-  ( ph -> A. x e. J ( F " x ) e. K )
24 23 adantr 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> A. x e. J ( F " x ) e. K )
25 simprr 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( `' F " y ) e. J )
26 22 24 25 rspcdva 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> ( F " ( `' F " y ) ) e. K )
27 20 26 eqeltrrd 
 |-  ( ( ph /\ ( y C_ Y /\ ( `' F " y ) e. J ) ) -> y e. K )
28 27 ex 
 |-  ( ph -> ( ( y C_ Y /\ ( `' F " y ) e. J ) -> y e. K ) )
29 17 28 sylbid 
 |-  ( ph -> ( y e. ( J qTop F ) -> y e. K ) )
30 29 ssrdv 
 |-  ( ph -> ( J qTop F ) C_ K )
31 6 30 eqssd 
 |-  ( ph -> K = ( J qTop F ) )