Metamath Proof Explorer

Theorem qtophmeo

Description: If two functions on a base topology J make the same identifications in order to create quotient spaces J qTop F and J qTop G , then not only are J qTop F and J qTop G homeomorphic, but there is a unique homeomorphism that makes the diagram commute. (Contributed by Mario Carneiro, 24-Mar-2015) (Proof shortened by Mario Carneiro, 23-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 qtophmeo.2 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 qtophmeo.3 
 |-  ( ph -> F : X -onto-> Y )
3 qtophmeo.4 
 |-  ( ph -> G : X -onto-> Y )
4 qtophmeo.5 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) = ( F ` y ) <-> ( G ` x ) = ( G ` y ) ) )
5 fofn 
 |-  ( G : X -onto-> Y -> G Fn X )
6 3 5 syl 
 |-  ( ph -> G Fn X )
7 qtopid 
 |-  ( ( J e. ( TopOn ` X ) /\ G Fn X ) -> G e. ( J Cn ( J qTop G ) ) )
8 1 6 7 syl2anc 
 |-  ( ph -> G e. ( J Cn ( J qTop G ) ) )
9 df-3an 
 |-  ( ( x e. X /\ y e. X /\ ( F ` x ) = ( F ` y ) ) <-> ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) )
10 4 biimpd 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) = ( F ` y ) -> ( G ` x ) = ( G ` y ) ) )
11 10 impr 
 |-  ( ( ph /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( G ` x ) = ( G ` y ) )
12 9 11 sylan2b 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ ( F ` x ) = ( F ` y ) ) ) -> ( G ` x ) = ( G ` y ) )
13 1 2 8 12 qtopeu 
 |-  ( ph -> E! f e. ( ( J qTop F ) Cn ( J qTop G ) ) G = ( f o. F ) )
14 reurex 
 |-  ( E! f e. ( ( J qTop F ) Cn ( J qTop G ) ) G = ( f o. F ) -> E. f e. ( ( J qTop F ) Cn ( J qTop G ) ) G = ( f o. F ) )
15 13 14 syl 
 |-  ( ph -> E. f e. ( ( J qTop F ) Cn ( J qTop G ) ) G = ( f o. F ) )
16 simprl 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) -> f e. ( ( J qTop F ) Cn ( J qTop G ) ) )
17 fofn 
 |-  ( F : X -onto-> Y -> F Fn X )
18 2 17 syl 
 |-  ( ph -> F Fn X )
19 qtopid 
 |-  ( ( J e. ( TopOn ` X ) /\ F Fn X ) -> F e. ( J Cn ( J qTop F ) ) )
20 1 18 19 syl2anc 
 |-  ( ph -> F e. ( J Cn ( J qTop F ) ) )
21 df-3an 
 |-  ( ( x e. X /\ y e. X /\ ( G ` x ) = ( G ` y ) ) <-> ( ( x e. X /\ y e. X ) /\ ( G ` x ) = ( G ` y ) ) )
22 4 biimprd 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( G ` x ) = ( G ` y ) -> ( F ` x ) = ( F ` y ) ) )
23 22 impr 
 |-  ( ( ph /\ ( ( x e. X /\ y e. X ) /\ ( G ` x ) = ( G ` y ) ) ) -> ( F ` x ) = ( F ` y ) )
24 21 23 sylan2b 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ ( G ` x ) = ( G ` y ) ) ) -> ( F ` x ) = ( F ` y ) )
25 1 3 20 24 qtopeu 
 |-  ( ph -> E! g e. ( ( J qTop G ) Cn ( J qTop F ) ) F = ( g o. G ) )
26 25 adantr 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) -> E! g e. ( ( J qTop G ) Cn ( J qTop F ) ) F = ( g o. G ) )
27 reurex 
 |-  ( E! g e. ( ( J qTop G ) Cn ( J qTop F ) ) F = ( g o. G ) -> E. g e. ( ( J qTop G ) Cn ( J qTop F ) ) F = ( g o. G ) )
28 26 27 syl 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) -> E. g e. ( ( J qTop G ) Cn ( J qTop F ) ) F = ( g o. G ) )
29 qtoptopon 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( J qTop F ) e. ( TopOn ` Y ) )
30 1 2 29 syl2anc 
 |-  ( ph -> ( J qTop F ) e. ( TopOn ` Y ) )
31 30 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> ( J qTop F ) e. ( TopOn ` Y ) )
32 qtoptopon 
 |-  ( ( J e. ( TopOn ` X ) /\ G : X -onto-> Y ) -> ( J qTop G ) e. ( TopOn ` Y ) )
33 1 3 32 syl2anc 
 |-  ( ph -> ( J qTop G ) e. ( TopOn ` Y ) )
34 33 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> ( J qTop G ) e. ( TopOn ` Y ) )
35 simplrl 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> f e. ( ( J qTop F ) Cn ( J qTop G ) ) )
36 cnf2 
 |-  ( ( ( J qTop F ) e. ( TopOn ` Y ) /\ ( J qTop G ) e. ( TopOn ` Y ) /\ f e. ( ( J qTop F ) Cn ( J qTop G ) ) ) -> f : Y --> Y )
37 31 34 35 36 syl3anc 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> f : Y --> Y )
38 simprl 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> g e. ( ( J qTop G ) Cn ( J qTop F ) ) )
39 cnf2 
 |-  ( ( ( J qTop G ) e. ( TopOn ` Y ) /\ ( J qTop F ) e. ( TopOn ` Y ) /\ g e. ( ( J qTop G ) Cn ( J qTop F ) ) ) -> g : Y --> Y )
40 34 31 38 39 syl3anc 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> g : Y --> Y )
41 coeq1 
 |-  ( h = ( g o. f ) -> ( h o. F ) = ( ( g o. f ) o. F ) )
42 41 eqeq2d 
 |-  ( h = ( g o. f ) -> ( F = ( h o. F ) <-> F = ( ( g o. f ) o. F ) ) )
43 coeq1 
 |-  ( h = ( _I |` Y ) -> ( h o. F ) = ( ( _I |` Y ) o. F ) )
44 43 eqeq2d 
 |-  ( h = ( _I |` Y ) -> ( F = ( h o. F ) <-> F = ( ( _I |` Y ) o. F ) ) )
45 simpr3 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ ( F ` x ) = ( F ` y ) ) ) -> ( F ` x ) = ( F ` y ) )
46 1 2 20 45 qtopeu 
 |-  ( ph -> E! h e. ( ( J qTop F ) Cn ( J qTop F ) ) F = ( h o. F ) )
47 46 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> E! h e. ( ( J qTop F ) Cn ( J qTop F ) ) F = ( h o. F ) )
48 cnco 
 |-  ( ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ g e. ( ( J qTop G ) Cn ( J qTop F ) ) ) -> ( g o. f ) e. ( ( J qTop F ) Cn ( J qTop F ) ) )
49 35 38 48 syl2anc 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> ( g o. f ) e. ( ( J qTop F ) Cn ( J qTop F ) ) )
50 idcn 
 |-  ( ( J qTop F ) e. ( TopOn ` Y ) -> ( _I |` Y ) e. ( ( J qTop F ) Cn ( J qTop F ) ) )
51 30 50 syl 
 |-  ( ph -> ( _I |` Y ) e. ( ( J qTop F ) Cn ( J qTop F ) ) )
52 51 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> ( _I |` Y ) e. ( ( J qTop F ) Cn ( J qTop F ) ) )
53 simprr 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> F = ( g o. G ) )
54 simplrr 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> G = ( f o. F ) )
55 54 coeq2d 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> ( g o. G ) = ( g o. ( f o. F ) ) )
56 53 55 eqtrd 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> F = ( g o. ( f o. F ) ) )
57 coass 
 |-  ( ( g o. f ) o. F ) = ( g o. ( f o. F ) )
58 56 57 eqtr4di 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> F = ( ( g o. f ) o. F ) )
59 fof 
 |-  ( F : X -onto-> Y -> F : X --> Y )
60 2 59 syl 
 |-  ( ph -> F : X --> Y )
61 60 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> F : X --> Y )
62 fcoi2 
 |-  ( F : X --> Y -> ( ( _I |` Y ) o. F ) = F )
63 61 62 syl 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> ( ( _I |` Y ) o. F ) = F )
64 63 eqcomd 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> F = ( ( _I |` Y ) o. F ) )
65 42 44 47 49 52 58 64 reu2eqd 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> ( g o. f ) = ( _I |` Y ) )
66 coeq1 
 |-  ( h = ( f o. g ) -> ( h o. G ) = ( ( f o. g ) o. G ) )
67 66 eqeq2d 
 |-  ( h = ( f o. g ) -> ( G = ( h o. G ) <-> G = ( ( f o. g ) o. G ) ) )
68 coeq1 
 |-  ( h = ( _I |` Y ) -> ( h o. G ) = ( ( _I |` Y ) o. G ) )
69 68 eqeq2d 
 |-  ( h = ( _I |` Y ) -> ( G = ( h o. G ) <-> G = ( ( _I |` Y ) o. G ) ) )
70 simpr3 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ ( G ` x ) = ( G ` y ) ) ) -> ( G ` x ) = ( G ` y ) )
71 1 3 8 70 qtopeu 
 |-  ( ph -> E! h e. ( ( J qTop G ) Cn ( J qTop G ) ) G = ( h o. G ) )
72 71 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> E! h e. ( ( J qTop G ) Cn ( J qTop G ) ) G = ( h o. G ) )
73 cnco 
 |-  ( ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ f e. ( ( J qTop F ) Cn ( J qTop G ) ) ) -> ( f o. g ) e. ( ( J qTop G ) Cn ( J qTop G ) ) )
74 38 35 73 syl2anc 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> ( f o. g ) e. ( ( J qTop G ) Cn ( J qTop G ) ) )
75 idcn 
 |-  ( ( J qTop G ) e. ( TopOn ` Y ) -> ( _I |` Y ) e. ( ( J qTop G ) Cn ( J qTop G ) ) )
76 33 75 syl 
 |-  ( ph -> ( _I |` Y ) e. ( ( J qTop G ) Cn ( J qTop G ) ) )
77 76 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> ( _I |` Y ) e. ( ( J qTop G ) Cn ( J qTop G ) ) )
78 53 coeq2d 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> ( f o. F ) = ( f o. ( g o. G ) ) )
79 54 78 eqtrd 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> G = ( f o. ( g o. G ) ) )
80 coass 
 |-  ( ( f o. g ) o. G ) = ( f o. ( g o. G ) )
81 79 80 eqtr4di 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> G = ( ( f o. g ) o. G ) )
82 fof 
 |-  ( G : X -onto-> Y -> G : X --> Y )
83 3 82 syl 
 |-  ( ph -> G : X --> Y )
84 83 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> G : X --> Y )
85 fcoi2 
 |-  ( G : X --> Y -> ( ( _I |` Y ) o. G ) = G )
86 84 85 syl 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> ( ( _I |` Y ) o. G ) = G )
87 86 eqcomd 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> G = ( ( _I |` Y ) o. G ) )
88 67 69 72 74 77 81 87 reu2eqd 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> ( f o. g ) = ( _I |` Y ) )
89 37 40 65 88 2fcoidinvd 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> `' f = g )
90 89 38 eqeltrd 
 |-  ( ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) /\ ( g e. ( ( J qTop G ) Cn ( J qTop F ) ) /\ F = ( g o. G ) ) ) -> `' f e. ( ( J qTop G ) Cn ( J qTop F ) ) )
91 28 90 rexlimddv 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) -> `' f e. ( ( J qTop G ) Cn ( J qTop F ) ) )
92 ishmeo 
 |-  ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) <-> ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ `' f e. ( ( J qTop G ) Cn ( J qTop F ) ) ) )
93 16 91 92 sylanbrc 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) -> f e. ( ( J qTop F ) Homeo ( J qTop G ) ) )
94 simprr 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) -> G = ( f o. F ) )
95 15 93 94 reximssdv 
 |-  ( ph -> E. f e. ( ( J qTop F ) Homeo ( J qTop G ) ) G = ( f o. F ) )
96 eqtr2 
 |-  ( ( G = ( f o. F ) /\ G = ( g o. F ) ) -> ( f o. F ) = ( g o. F ) )
97 2 adantr 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> F : X -onto-> Y )
98 30 adantr 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> ( J qTop F ) e. ( TopOn ` Y ) )
99 33 adantr 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> ( J qTop G ) e. ( TopOn ` Y ) )
100 simprl 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> f e. ( ( J qTop F ) Homeo ( J qTop G ) ) )
101 hmeof1o2 
 |-  ( ( ( J qTop F ) e. ( TopOn ` Y ) /\ ( J qTop G ) e. ( TopOn ` Y ) /\ f e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) -> f : Y -1-1-onto-> Y )
102 98 99 100 101 syl3anc 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> f : Y -1-1-onto-> Y )
103 f1ofn 
 |-  ( f : Y -1-1-onto-> Y -> f Fn Y )
104 102 103 syl 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> f Fn Y )
105 simprr 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> g e. ( ( J qTop F ) Homeo ( J qTop G ) ) )
106 hmeof1o2 
 |-  ( ( ( J qTop F ) e. ( TopOn ` Y ) /\ ( J qTop G ) e. ( TopOn ` Y ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) -> g : Y -1-1-onto-> Y )
107 98 99 105 106 syl3anc 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> g : Y -1-1-onto-> Y )
108 f1ofn 
 |-  ( g : Y -1-1-onto-> Y -> g Fn Y )
109 107 108 syl 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> g Fn Y )
110 cocan2 
 |-  ( ( F : X -onto-> Y /\ f Fn Y /\ g Fn Y ) -> ( ( f o. F ) = ( g o. F ) <-> f = g ) )
111 97 104 109 110 syl3anc 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> ( ( f o. F ) = ( g o. F ) <-> f = g ) )
112 96 111 imbitrid 
 |-  ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> ( ( G = ( f o. F ) /\ G = ( g o. F ) ) -> f = g ) )
113 112 ralrimivva 
 |-  ( ph -> A. f e. ( ( J qTop F ) Homeo ( J qTop G ) ) A. g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ( ( G = ( f o. F ) /\ G = ( g o. F ) ) -> f = g ) )
114 coeq1 
 |-  ( f = g -> ( f o. F ) = ( g o. F ) )
115 114 eqeq2d 
 |-  ( f = g -> ( G = ( f o. F ) <-> G = ( g o. F ) ) )
116 115 reu4 
 |-  ( E! f e. ( ( J qTop F ) Homeo ( J qTop G ) ) G = ( f o. F ) <-> ( E. f e. ( ( J qTop F ) Homeo ( J qTop G ) ) G = ( f o. F ) /\ A. f e. ( ( J qTop F ) Homeo ( J qTop G ) ) A. g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ( ( G = ( f o. F ) /\ G = ( g o. F ) ) -> f = g ) ) )
117 95 113 116 sylanbrc 
 |-  ( ph -> E! f e. ( ( J qTop F ) Homeo ( J qTop G ) ) G = ( f o. F ) )