# 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 ) )`
` |-  ( ( 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 ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> F : X -onto-> Y )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 syl5ib
` |-  ( ( 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 ) )`