Metamath Proof Explorer

Theorem qtopeu

Description: Universal property of the quotient topology. If G is a function from J to K which is equal on all equivalent elements under F , then there is a unique continuous map f : ( J / F ) --> K such that G = f o. F , and we say that G "passes to the quotient". (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypotheses qtopeu.1 
|- ( ph -> J e. ( TopOn ` X ) )
qtopeu.3 
|- ( ph -> F : X -onto-> Y )
qtopeu.4 
|- ( ph -> G e. ( J Cn K ) )
qtopeu.5 
|- ( ( ph /\ ( x e. X /\ y e. X /\ ( F ` x ) = ( F ` y ) ) ) -> ( G ` x ) = ( G ` y ) )
Assertion qtopeu 
|- ( ph -> E! f e. ( ( J qTop F ) Cn K ) G = ( f o. F ) )

Proof

Step Hyp Ref Expression
1 qtopeu.1 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 qtopeu.3 
 |-  ( ph -> F : X -onto-> Y )
3 qtopeu.4 
 |-  ( ph -> G e. ( J Cn K ) )
4 qtopeu.5 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ ( F ` x ) = ( F ` y ) ) ) -> ( G ` x ) = ( G ` y ) )
5 fofn 
 |-  ( F : X -onto-> Y -> F Fn X )
6 2 5 syl 
 |-  ( ph -> F Fn X )
7 6 adantr 
 |-  ( ( ph /\ x e. X ) -> F Fn X )
8 fniniseg 
 |-  ( F Fn X -> ( y e. ( `' F " { ( F ` x ) } ) <-> ( y e. X /\ ( F ` y ) = ( F ` x ) ) ) )
9 7 8 syl 
 |-  ( ( ph /\ x e. X ) -> ( y e. ( `' F " { ( F ` x ) } ) <-> ( y e. X /\ ( F ` y ) = ( F ` x ) ) ) )
10 eqcom 
 |-  ( ( F ` x ) = ( F ` y ) <-> ( F ` y ) = ( F ` x ) )
11 10 3anbi3i 
 |-  ( ( x e. X /\ y e. X /\ ( F ` x ) = ( F ` y ) ) <-> ( x e. X /\ y e. X /\ ( F ` y ) = ( F ` x ) ) )
12 3anass 
 |-  ( ( x e. X /\ y e. X /\ ( F ` y ) = ( F ` x ) ) <-> ( x e. X /\ ( y e. X /\ ( F ` y ) = ( F ` x ) ) ) )
13 11 12 bitri 
 |-  ( ( x e. X /\ y e. X /\ ( F ` x ) = ( F ` y ) ) <-> ( x e. X /\ ( y e. X /\ ( F ` y ) = ( F ` x ) ) ) )
14 13 4 sylan2br 
 |-  ( ( ph /\ ( x e. X /\ ( y e. X /\ ( F ` y ) = ( F ` x ) ) ) ) -> ( G ` x ) = ( G ` y ) )
15 14 eqcomd 
 |-  ( ( ph /\ ( x e. X /\ ( y e. X /\ ( F ` y ) = ( F ` x ) ) ) ) -> ( G ` y ) = ( G ` x ) )
16 15 expr 
 |-  ( ( ph /\ x e. X ) -> ( ( y e. X /\ ( F ` y ) = ( F ` x ) ) -> ( G ` y ) = ( G ` x ) ) )
17 9 16 sylbid 
 |-  ( ( ph /\ x e. X ) -> ( y e. ( `' F " { ( F ` x ) } ) -> ( G ` y ) = ( G ` x ) ) )
18 17 ralrimiv 
 |-  ( ( ph /\ x e. X ) -> A. y e. ( `' F " { ( F ` x ) } ) ( G ` y ) = ( G ` x ) )
19 cntop2 
 |-  ( G e. ( J Cn K ) -> K e. Top )
20 3 19 syl 
 |-  ( ph -> K e. Top )
21 toptopon2 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
22 20 21 sylib 
 |-  ( ph -> K e. ( TopOn ` U. K ) )
23 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` U. K ) /\ G e. ( J Cn K ) ) -> G : X --> U. K )
24 1 22 3 23 syl3anc 
 |-  ( ph -> G : X --> U. K )
25 24 ffnd 
 |-  ( ph -> G Fn X )
26 25 adantr 
 |-  ( ( ph /\ x e. X ) -> G Fn X )
27 cnvimass 
 |-  ( `' F " { ( F ` x ) } ) C_ dom F
28 fof 
 |-  ( F : X -onto-> Y -> F : X --> Y )
29 2 28 syl 
 |-  ( ph -> F : X --> Y )
30 29 fdmd 
 |-  ( ph -> dom F = X )
31 30 adantr 
 |-  ( ( ph /\ x e. X ) -> dom F = X )
32 27 31 sseqtrid 
 |-  ( ( ph /\ x e. X ) -> ( `' F " { ( F ` x ) } ) C_ X )
33 eqeq1 
 |-  ( w = ( G ` y ) -> ( w = ( G ` x ) <-> ( G ` y ) = ( G ` x ) ) )
34 33 ralima 
 |-  ( ( G Fn X /\ ( `' F " { ( F ` x ) } ) C_ X ) -> ( A. w e. ( G " ( `' F " { ( F ` x ) } ) ) w = ( G ` x ) <-> A. y e. ( `' F " { ( F ` x ) } ) ( G ` y ) = ( G ` x ) ) )
35 26 32 34 syl2anc 
 |-  ( ( ph /\ x e. X ) -> ( A. w e. ( G " ( `' F " { ( F ` x ) } ) ) w = ( G ` x ) <-> A. y e. ( `' F " { ( F ` x ) } ) ( G ` y ) = ( G ` x ) ) )
36 18 35 mpbird 
 |-  ( ( ph /\ x e. X ) -> A. w e. ( G " ( `' F " { ( F ` x ) } ) ) w = ( G ` x ) )
37 24 fdmd 
 |-  ( ph -> dom G = X )
38 37 eleq2d 
 |-  ( ph -> ( x e. dom G <-> x e. X ) )
39 38 biimpar 
 |-  ( ( ph /\ x e. X ) -> x e. dom G )
40 simpr 
 |-  ( ( ph /\ x e. X ) -> x e. X )
41 eqidd 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) = ( F ` x ) )
42 fniniseg 
 |-  ( F Fn X -> ( x e. ( `' F " { ( F ` x ) } ) <-> ( x e. X /\ ( F ` x ) = ( F ` x ) ) ) )
43 7 42 syl 
 |-  ( ( ph /\ x e. X ) -> ( x e. ( `' F " { ( F ` x ) } ) <-> ( x e. X /\ ( F ` x ) = ( F ` x ) ) ) )
44 40 41 43 mpbir2and 
 |-  ( ( ph /\ x e. X ) -> x e. ( `' F " { ( F ` x ) } ) )
45 inelcm 
 |-  ( ( x e. dom G /\ x e. ( `' F " { ( F ` x ) } ) ) -> ( dom G i^i ( `' F " { ( F ` x ) } ) ) =/= (/) )
46 39 44 45 syl2anc 
 |-  ( ( ph /\ x e. X ) -> ( dom G i^i ( `' F " { ( F ` x ) } ) ) =/= (/) )
47 imadisj 
 |-  ( ( G " ( `' F " { ( F ` x ) } ) ) = (/) <-> ( dom G i^i ( `' F " { ( F ` x ) } ) ) = (/) )
48 47 necon3bii 
 |-  ( ( G " ( `' F " { ( F ` x ) } ) ) =/= (/) <-> ( dom G i^i ( `' F " { ( F ` x ) } ) ) =/= (/) )
49 46 48 sylibr 
 |-  ( ( ph /\ x e. X ) -> ( G " ( `' F " { ( F ` x ) } ) ) =/= (/) )
50 eqsn 
 |-  ( ( G " ( `' F " { ( F ` x ) } ) ) =/= (/) -> ( ( G " ( `' F " { ( F ` x ) } ) ) = { ( G ` x ) } <-> A. w e. ( G " ( `' F " { ( F ` x ) } ) ) w = ( G ` x ) ) )
51 49 50 syl 
 |-  ( ( ph /\ x e. X ) -> ( ( G " ( `' F " { ( F ` x ) } ) ) = { ( G ` x ) } <-> A. w e. ( G " ( `' F " { ( F ` x ) } ) ) w = ( G ` x ) ) )
52 36 51 mpbird 
 |-  ( ( ph /\ x e. X ) -> ( G " ( `' F " { ( F ` x ) } ) ) = { ( G ` x ) } )
53 52 unieqd 
 |-  ( ( ph /\ x e. X ) -> U. ( G " ( `' F " { ( F ` x ) } ) ) = U. { ( G ` x ) } )
54 fvex 
 |-  ( G ` x ) e. _V
55 54 unisn 
 |-  U. { ( G ` x ) } = ( G ` x )
56 53 55 eqtr2di 
 |-  ( ( ph /\ x e. X ) -> ( G ` x ) = U. ( G " ( `' F " { ( F ` x ) } ) ) )
57 56 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( G ` x ) ) = ( x e. X |-> U. ( G " ( `' F " { ( F ` x ) } ) ) ) )
58 24 feqmptd 
 |-  ( ph -> G = ( x e. X |-> ( G ` x ) ) )
59 29 ffvelrnda 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. Y )
60 29 feqmptd 
 |-  ( ph -> F = ( x e. X |-> ( F ` x ) ) )
61 eqidd 
 |-  ( ph -> ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) = ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) )
62 sneq 
 |-  ( w = ( F ` x ) -> { w } = { ( F ` x ) } )
63 62 imaeq2d 
 |-  ( w = ( F ` x ) -> ( `' F " { w } ) = ( `' F " { ( F ` x ) } ) )
64 63 imaeq2d 
 |-  ( w = ( F ` x ) -> ( G " ( `' F " { w } ) ) = ( G " ( `' F " { ( F ` x ) } ) ) )
65 64 unieqd 
 |-  ( w = ( F ` x ) -> U. ( G " ( `' F " { w } ) ) = U. ( G " ( `' F " { ( F ` x ) } ) ) )
66 59 60 61 65 fmptco 
 |-  ( ph -> ( ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) o. F ) = ( x e. X |-> U. ( G " ( `' F " { ( F ` x ) } ) ) ) )
67 57 58 66 3eqtr4d 
 |-  ( ph -> G = ( ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) o. F ) )
68 67 3 eqeltrrd 
 |-  ( ph -> ( ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) o. F ) e. ( J Cn K ) )
69 24 ffvelrnda 
 |-  ( ( ph /\ x e. X ) -> ( G ` x ) e. U. K )
70 56 69 eqeltrrd 
 |-  ( ( ph /\ x e. X ) -> U. ( G " ( `' F " { ( F ` x ) } ) ) e. U. K )
71 70 ralrimiva 
 |-  ( ph -> A. x e. X U. ( G " ( `' F " { ( F ` x ) } ) ) e. U. K )
72 65 eqcomd 
 |-  ( w = ( F ` x ) -> U. ( G " ( `' F " { ( F ` x ) } ) ) = U. ( G " ( `' F " { w } ) ) )
73 72 eqcoms 
 |-  ( ( F ` x ) = w -> U. ( G " ( `' F " { ( F ` x ) } ) ) = U. ( G " ( `' F " { w } ) ) )
74 73 eleq1d 
 |-  ( ( F ` x ) = w -> ( U. ( G " ( `' F " { ( F ` x ) } ) ) e. U. K <-> U. ( G " ( `' F " { w } ) ) e. U. K ) )
75 74 cbvfo 
 |-  ( F : X -onto-> Y -> ( A. x e. X U. ( G " ( `' F " { ( F ` x ) } ) ) e. U. K <-> A. w e. Y U. ( G " ( `' F " { w } ) ) e. U. K ) )
76 2 75 syl 
 |-  ( ph -> ( A. x e. X U. ( G " ( `' F " { ( F ` x ) } ) ) e. U. K <-> A. w e. Y U. ( G " ( `' F " { w } ) ) e. U. K ) )
77 71 76 mpbid 
 |-  ( ph -> A. w e. Y U. ( G " ( `' F " { w } ) ) e. U. K )
78 eqid 
 |-  ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) = ( w e. Y |-> U. ( G " ( `' F " { w } ) ) )
79 78 fmpt 
 |-  ( A. w e. Y U. ( G " ( `' F " { w } ) ) e. U. K <-> ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) : Y --> U. K )
80 77 79 sylib 
 |-  ( ph -> ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) : Y --> U. K )
81 qtopcn 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` U. K ) ) /\ ( F : X -onto-> Y /\ ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) : Y --> U. K ) ) -> ( ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) e. ( ( J qTop F ) Cn K ) <-> ( ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) o. F ) e. ( J Cn K ) ) )
82 1 22 2 80 81 syl22anc 
 |-  ( ph -> ( ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) e. ( ( J qTop F ) Cn K ) <-> ( ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) o. F ) e. ( J Cn K ) ) )
83 68 82 mpbird 
 |-  ( ph -> ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) e. ( ( J qTop F ) Cn K ) )
84 coeq1 
 |-  ( f = ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) -> ( f o. F ) = ( ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) o. F ) )
85 84 rspceeqv 
 |-  ( ( ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) e. ( ( J qTop F ) Cn K ) /\ G = ( ( w e. Y |-> U. ( G " ( `' F " { w } ) ) ) o. F ) ) -> E. f e. ( ( J qTop F ) Cn K ) G = ( f o. F ) )
86 83 67 85 syl2anc 
 |-  ( ph -> E. f e. ( ( J qTop F ) Cn K ) G = ( f o. F ) )
87 eqtr2 
 |-  ( ( G = ( f o. F ) /\ G = ( g o. F ) ) -> ( f o. F ) = ( g o. F ) )
88 2 adantr 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn K ) /\ g e. ( ( J qTop F ) Cn K ) ) ) -> F : X -onto-> Y )
89 qtoptopon 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( J qTop F ) e. ( TopOn ` Y ) )
90 1 2 89 syl2anc 
 |-  ( ph -> ( J qTop F ) e. ( TopOn ` Y ) )
91 90 adantr 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn K ) /\ g e. ( ( J qTop F ) Cn K ) ) ) -> ( J qTop F ) e. ( TopOn ` Y ) )
92 22 adantr 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn K ) /\ g e. ( ( J qTop F ) Cn K ) ) ) -> K e. ( TopOn ` U. K ) )
93 simprl 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn K ) /\ g e. ( ( J qTop F ) Cn K ) ) ) -> f e. ( ( J qTop F ) Cn K ) )
94 cnf2 
 |-  ( ( ( J qTop F ) e. ( TopOn ` Y ) /\ K e. ( TopOn ` U. K ) /\ f e. ( ( J qTop F ) Cn K ) ) -> f : Y --> U. K )
95 91 92 93 94 syl3anc 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn K ) /\ g e. ( ( J qTop F ) Cn K ) ) ) -> f : Y --> U. K )
96 95 ffnd 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn K ) /\ g e. ( ( J qTop F ) Cn K ) ) ) -> f Fn Y )
97 simprr 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn K ) /\ g e. ( ( J qTop F ) Cn K ) ) ) -> g e. ( ( J qTop F ) Cn K ) )
98 cnf2 
 |-  ( ( ( J qTop F ) e. ( TopOn ` Y ) /\ K e. ( TopOn ` U. K ) /\ g e. ( ( J qTop F ) Cn K ) ) -> g : Y --> U. K )
99 91 92 97 98 syl3anc 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn K ) /\ g e. ( ( J qTop F ) Cn K ) ) ) -> g : Y --> U. K )
100 99 ffnd 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn K ) /\ g e. ( ( J qTop F ) Cn K ) ) ) -> g Fn Y )
101 cocan2 
 |-  ( ( F : X -onto-> Y /\ f Fn Y /\ g Fn Y ) -> ( ( f o. F ) = ( g o. F ) <-> f = g ) )
102 88 96 100 101 syl3anc 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn K ) /\ g e. ( ( J qTop F ) Cn K ) ) ) -> ( ( f o. F ) = ( g o. F ) <-> f = g ) )
103 87 102 syl5ib 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn K ) /\ g e. ( ( J qTop F ) Cn K ) ) ) -> ( ( G = ( f o. F ) /\ G = ( g o. F ) ) -> f = g ) )
104 103 ralrimivva 
 |-  ( ph -> A. f e. ( ( J qTop F ) Cn K ) A. g e. ( ( J qTop F ) Cn K ) ( ( G = ( f o. F ) /\ G = ( g o. F ) ) -> f = g ) )
105 coeq1 
 |-  ( f = g -> ( f o. F ) = ( g o. F ) )
106 105 eqeq2d 
 |-  ( f = g -> ( G = ( f o. F ) <-> G = ( g o. F ) ) )
107 106 reu4 
 |-  ( E! f e. ( ( J qTop F ) Cn K ) G = ( f o. F ) <-> ( E. f e. ( ( J qTop F ) Cn K ) G = ( f o. F ) /\ A. f e. ( ( J qTop F ) Cn K ) A. g e. ( ( J qTop F ) Cn K ) ( ( G = ( f o. F ) /\ G = ( g o. F ) ) -> f = g ) ) )
108 86 104 107 sylanbrc 
 |-  ( ph -> E! f e. ( ( J qTop F ) Cn K ) G = ( f o. F ) )