Metamath Proof Explorer

Theorem qtopcn

Description: Universal property of a quotient map. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Assertion qtopcn 
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) -> ( G e. ( ( J qTop F ) Cn K ) <-> ( G o. F ) e. ( J Cn K ) ) )

Proof

Step Hyp Ref Expression
1 cnvimass 
 |-  ( `' G " x ) C_ dom G
2 simplrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) /\ x e. K ) -> G : Y --> Z )
3 1 2 fssdm 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) /\ x e. K ) -> ( `' G " x ) C_ Y )
4 simplll 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) /\ x e. K ) -> J e. ( TopOn ` X ) )
5 simplrl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) /\ x e. K ) -> F : X -onto-> Y )
6 elqtop3 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( ( `' G " x ) e. ( J qTop F ) <-> ( ( `' G " x ) C_ Y /\ ( `' F " ( `' G " x ) ) e. J ) ) )
7 4 5 6 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) /\ x e. K ) -> ( ( `' G " x ) e. ( J qTop F ) <-> ( ( `' G " x ) C_ Y /\ ( `' F " ( `' G " x ) ) e. J ) ) )
8 3 7 mpbirand 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) /\ x e. K ) -> ( ( `' G " x ) e. ( J qTop F ) <-> ( `' F " ( `' G " x ) ) e. J ) )
9 cnvco 
 |-  `' ( G o. F ) = ( `' F o. `' G )
10 9 imaeq1i 
 |-  ( `' ( G o. F ) " x ) = ( ( `' F o. `' G ) " x )
11 imaco 
 |-  ( ( `' F o. `' G ) " x ) = ( `' F " ( `' G " x ) )
12 10 11 eqtri 
 |-  ( `' ( G o. F ) " x ) = ( `' F " ( `' G " x ) )
13 12 eleq1i 
 |-  ( ( `' ( G o. F ) " x ) e. J <-> ( `' F " ( `' G " x ) ) e. J )
14 8 13 bitr4di 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) /\ x e. K ) -> ( ( `' G " x ) e. ( J qTop F ) <-> ( `' ( G o. F ) " x ) e. J ) )
15 14 ralbidva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) -> ( A. x e. K ( `' G " x ) e. ( J qTop F ) <-> A. x e. K ( `' ( G o. F ) " x ) e. J ) )
16 simprr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) -> G : Y --> Z )
17 16 biantrurd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) -> ( A. x e. K ( `' G " x ) e. ( J qTop F ) <-> ( G : Y --> Z /\ A. x e. K ( `' G " x ) e. ( J qTop F ) ) ) )
18 fof 
 |-  ( F : X -onto-> Y -> F : X --> Y )
19 18 ad2antrl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) -> F : X --> Y )
20 fco 
 |-  ( ( G : Y --> Z /\ F : X --> Y ) -> ( G o. F ) : X --> Z )
21 16 19 20 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) -> ( G o. F ) : X --> Z )
22 21 biantrurd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) -> ( A. x e. K ( `' ( G o. F ) " x ) e. J <-> ( ( G o. F ) : X --> Z /\ A. x e. K ( `' ( G o. F ) " x ) e. J ) ) )
23 15 17 22 3bitr3d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) -> ( ( G : Y --> Z /\ A. x e. K ( `' G " x ) e. ( J qTop F ) ) <-> ( ( G o. F ) : X --> Z /\ A. x e. K ( `' ( G o. F ) " x ) e. J ) ) )
24 qtoptopon 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( J qTop F ) e. ( TopOn ` Y ) )
25 24 ad2ant2r 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) -> ( J qTop F ) e. ( TopOn ` Y ) )
26 simplr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) -> K e. ( TopOn ` Z ) )
27 iscn 
 |-  ( ( ( J qTop F ) e. ( TopOn ` Y ) /\ K e. ( TopOn ` Z ) ) -> ( G e. ( ( J qTop F ) Cn K ) <-> ( G : Y --> Z /\ A. x e. K ( `' G " x ) e. ( J qTop F ) ) ) )
28 25 26 27 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) -> ( G e. ( ( J qTop F ) Cn K ) <-> ( G : Y --> Z /\ A. x e. K ( `' G " x ) e. ( J qTop F ) ) ) )
29 iscn 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) -> ( ( G o. F ) e. ( J Cn K ) <-> ( ( G o. F ) : X --> Z /\ A. x e. K ( `' ( G o. F ) " x ) e. J ) ) )
30 29 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) -> ( ( G o. F ) e. ( J Cn K ) <-> ( ( G o. F ) : X --> Z /\ A. x e. K ( `' ( G o. F ) " x ) e. J ) ) )
31 23 28 30 3bitr4d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Z ) ) /\ ( F : X -onto-> Y /\ G : Y --> Z ) ) -> ( G e. ( ( J qTop F ) Cn K ) <-> ( G o. F ) e. ( J Cn K ) ) )