Theorem qtophmeo 17802

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 homeomorhism that makes the diagram commute. (Contributed by Mario Carneiro, 24-Mar-2015.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)

Hypotheses

Ref	Expression
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

Ref	Expression
qtophmeo	|- ( ph -> E! f e. ( ( J qTop F ) Homeo ( J qTop G ) ) G = ( f o. F ) )

Distinct variable groups:   x, f, y, F   f, G, x, y   f, J, x, y   ph, f, x, y   x, X, y   f, Y, x

Allowed substitution hints:   X( f)   Y( y)

Proof of Theorem qtophmeo

Dummy variables g h are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		qtophmeo.2	. . . . 5 |- ( ph -> J e. (TopOn ` X ) )
2		qtophmeo.3	. . . . 5 |- ( ph -> F : X -onto-> Y )
3		qtophmeo.4	. . . . . . 7 |- ( ph -> G : X -onto-> Y )
4		fofn 5614	. . . . . . 7 |- ( G : X -onto-> Y -> G Fn X )
5	3, 4	syl 16	. . . . . 6 |- ( ph -> G Fn X )
6		qtopid 17690	. . . . . 6 |- ( ( J e. (TopOn ` X ) /\ G Fn X ) -> G e. ( J Cn ( J qTop G ) ) )
7	1, 5, 6	syl2anc 643	. . . . 5 |- ( ph -> G e. ( J Cn ( J qTop G ) ) )
8		df-3an 938	. . . . . 6 |- ( ( x e. X /\ y e. X /\ ( F ` x ) = ( F ` y ) ) <-> ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) )
9		qtophmeo.5	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) = ( F ` y ) <-> ( G ` x ) = ( G ` y ) ) )
10	9	biimpd 199	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) = ( F ` y ) -> ( G ` x ) = ( G ` y ) ) )
11	10	impr 603	. . . . . 6 |- ( ( ph /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( G ` x ) = ( G ` y ) )
12	8, 11	sylan2b 462	. . . . 5 |- ( ( ph /\ ( x e. X /\ y e. X /\ ( F ` x ) = ( F ` y ) ) ) -> ( G ` x ) = ( G ` y ) )
13	1, 2, 7, 12	qtopeu 17701	. . . 4 |- ( ph -> E! f e. ( ( J qTop F ) Cn ( J qTop G ) ) G = ( f o. F ) )
14		reurex 2882	. . . 4 |- ( 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 16	. . 3 |- ( ph -> E. f e. ( ( J qTop F ) Cn ( J qTop G ) ) G = ( f o. F ) )
16		simprl 733	. . . . . . 7 |- ( ( 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 5614	. . . . . . . . . . . . 13 |- ( F : X -onto-> Y -> F Fn X )
18	2, 17	syl 16	. . . . . . . . . . . 12 |- ( ph -> F Fn X )
19		qtopid 17690	. . . . . . . . . . . 12 |- ( ( J e. (TopOn ` X ) /\ F Fn X ) -> F e. ( J Cn ( J qTop F ) ) )
20	1, 18, 19	syl2anc 643	. . . . . . . . . . 11 |- ( ph -> F e. ( J Cn ( J qTop F ) ) )
21		df-3an 938	. . . . . . . . . . . 12 |- ( ( x e. X /\ y e. X /\ ( G ` x ) = ( G ` y ) ) <-> ( ( x e. X /\ y e. X ) /\ ( G ` x ) = ( G ` y ) ) )
22	9	biimprd 215	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( G ` x ) = ( G ` y ) -> ( F ` x ) = ( F ` y ) ) )
23	22	impr 603	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( x e. X /\ y e. X ) /\ ( G ` x ) = ( G ` y ) ) ) -> ( F ` x ) = ( F ` y ) )
24	21, 23	sylan2b 462	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. X /\ y e. X /\ ( G ` x ) = ( G ` y ) ) ) -> ( F ` x ) = ( F ` y ) )
25	1, 3, 20, 24	qtopeu 17701	. . . . . . . . . 10 |- ( ph -> E! g e. ( ( J qTop G ) Cn ( J qTop F ) ) F = ( g o. G ) )
26	25	adantr 452	. . . . . . . . 9 |- ( ( 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 2882	. . . . . . . . 9 |- ( 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 16	. . . . . . . 8 |- ( ( 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 17689	. . . . . . . . . . . . . 14 |- ( ( J e. (TopOn ` X ) /\ F : X -onto-> Y ) -> ( J qTop F ) e. (TopOn ` Y ) )
30	1, 2, 29	syl2anc 643	. . . . . . . . . . . . 13 |- ( ph -> ( J qTop F ) e. (TopOn ` Y ) )
31	30	ad2antrr 707	. . . . . . . . . . . 12 |- ( ( ( 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 17689	. . . . . . . . . . . . . 14 |- ( ( J e. (TopOn ` X ) /\ G : X -onto-> Y ) -> ( J qTop G ) e. (TopOn ` Y ) )
33	1, 3, 32	syl2anc 643	. . . . . . . . . . . . 13 |- ( ph -> ( J qTop G ) e. (TopOn ` Y ) )
34	33	ad2antrr 707	. . . . . . . . . . . 12 |- ( ( ( 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 737	. . . . . . . . . . . 12 |- ( ( ( 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 17267	. . . . . . . . . . . 12 |- ( ( ( 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 1184	. . . . . . . . . . 11 |- ( ( ( 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 733	. . . . . . . . . . . 12 |- ( ( ( 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 17267	. . . . . . . . . . . 12 |- ( ( ( 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 1184	. . . . . . . . . . 11 |- ( ( ( 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		simpr3 965	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. X /\ y e. X /\ ( G ` x ) = ( G ` y ) ) ) -> ( G ` x ) = ( G ` y ) )
42	1, 3, 7, 41	qtopeu 17701	. . . . . . . . . . . . . 14 |- ( ph -> E! h e. ( ( J qTop G ) Cn ( J qTop G ) ) G = ( h o. G ) )
43	42	ad2antrr 707	. . . . . . . . . . . . 13 |- ( ( ( 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 ) )
44		reurmo 2883	. . . . . . . . . . . . 13 |- ( E! h e. ( ( J qTop G ) Cn ( J qTop G ) ) G = ( h o. G ) -> E* h e. ( ( J qTop G ) Cn ( J qTop G ) ) G = ( h o. G ) )
45	43, 44	syl 16	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
46		cnco 17284	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
47	38, 35, 46	syl2anc 643	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
48		simplrr 738	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
49		simprr 734	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) )
50	49	coeq2d 4994	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) )
51	48, 50	eqtrd 2436	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
52		coass 5347	. . . . . . . . . . . . 13 |- ( ( f o. g ) o. G ) = ( f o. ( g o. G ) )
53	51, 52	syl6eqr 2454	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
54		idcn 17275	. . . . . . . . . . . . . 14 |- ( ( J qTop G ) e. (TopOn ` Y ) -> ( _I |` Y ) e. ( ( J qTop G ) Cn ( J qTop G ) ) )
55	33, 54	syl 16	. . . . . . . . . . . . 13 |- ( ph -> ( _I |` Y ) e. ( ( J qTop G ) Cn ( J qTop G ) ) )
56	55	ad2antrr 707	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
57		fof 5612	. . . . . . . . . . . . . . . 16 |- ( G : X -onto-> Y -> G : X --> Y )
58	3, 57	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> G : X --> Y )
59	58	ad2antrr 707	. . . . . . . . . . . . . 14 |- ( ( ( 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 )
60		fcoi2 5577	. . . . . . . . . . . . . 14 |- ( G : X --> Y -> ( ( _I |` Y ) o. G ) = G )
61	59, 60	syl 16	. . . . . . . . . . . . 13 |- ( ( ( 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 )
62	61	eqcomd 2409	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
63		coeq1 4989	. . . . . . . . . . . . . 14 |- ( h = ( f o. g ) -> ( h o. G ) = ( ( f o. g ) o. G ) )
64	63	eqeq2d 2415	. . . . . . . . . . . . 13 |- ( h = ( f o. g ) -> ( G = ( h o. G ) <-> G = ( ( f o. g ) o. G ) ) )
65		coeq1 4989	. . . . . . . . . . . . . 14 |- ( h = ( _I |` Y ) -> ( h o. G ) = ( ( _I |` Y ) o. G ) )
66	65	eqeq2d 2415	. . . . . . . . . . . . 13 |- ( h = ( _I |` Y ) -> ( G = ( h o. G ) <-> G = ( ( _I |` Y ) o. G ) ) )
67	64, 66	rmoi 3210	. . . . . . . . . . . 12 |- ( ( E* h e. ( ( J qTop G ) Cn ( J qTop G ) ) G = ( h o. G ) /\ ( ( f o. g ) e. ( ( J qTop G ) Cn ( J qTop G ) ) /\ G = ( ( f o. g ) o. G ) ) /\ ( ( _I |` Y ) e. ( ( J qTop G ) Cn ( J qTop G ) ) /\ G = ( ( _I |` Y ) o. G ) ) ) -> ( f o. g ) = ( _I |` Y ) )
68	45, 47, 53, 56, 62, 67	syl122anc 1193	. . . . . . . . . . 11 |- ( ( ( 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 ) )
69		simpr3 965	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. X /\ y e. X /\ ( F ` x ) = ( F ` y ) ) ) -> ( F ` x ) = ( F ` y ) )
70	1, 2, 20, 69	qtopeu 17701	. . . . . . . . . . . . . 14 |- ( ph -> E! h e. ( ( J qTop F ) Cn ( J qTop F ) ) F = ( h o. F ) )
71	70	ad2antrr 707	. . . . . . . . . . . . 13 |- ( ( ( 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 ) )
72		reurmo 2883	. . . . . . . . . . . . 13 |- ( E! h e. ( ( J qTop F ) Cn ( J qTop F ) ) F = ( h o. F ) -> E* h e. ( ( J qTop F ) Cn ( J qTop F ) ) F = ( h o. F ) )
73	71, 72	syl 16	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
74		cnco 17284	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
75	35, 38, 74	syl2anc 643	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
76	48	coeq2d 4994	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) )
77	49, 76	eqtrd 2436	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
78		coass 5347	. . . . . . . . . . . . 13 |- ( ( g o. f ) o. F ) = ( g o. ( f o. F ) )
79	77, 78	syl6eqr 2454	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
80		idcn 17275	. . . . . . . . . . . . . 14 |- ( ( J qTop F ) e. (TopOn ` Y ) -> ( _I |` Y ) e. ( ( J qTop F ) Cn ( J qTop F ) ) )
81	30, 80	syl 16	. . . . . . . . . . . . 13 |- ( ph -> ( _I |` Y ) e. ( ( J qTop F ) Cn ( J qTop F ) ) )
82	81	ad2antrr 707	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
83		fof 5612	. . . . . . . . . . . . . . . 16 |- ( F : X -onto-> Y -> F : X --> Y )
84	2, 83	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> F : X --> Y )
85	84	ad2antrr 707	. . . . . . . . . . . . . 14 |- ( ( ( 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 )
86		fcoi2 5577	. . . . . . . . . . . . . 14 |- ( F : X --> Y -> ( ( _I |` Y ) o. F ) = F )
87	85, 86	syl 16	. . . . . . . . . . . . 13 |- ( ( ( 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 )
88	87	eqcomd 2409	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
89		coeq1 4989	. . . . . . . . . . . . . 14 |- ( h = ( g o. f ) -> ( h o. F ) = ( ( g o. f ) o. F ) )
90	89	eqeq2d 2415	. . . . . . . . . . . . 13 |- ( h = ( g o. f ) -> ( F = ( h o. F ) <-> F = ( ( g o. f ) o. F ) ) )
91		coeq1 4989	. . . . . . . . . . . . . 14 |- ( h = ( _I |` Y ) -> ( h o. F ) = ( ( _I |` Y ) o. F ) )
92	91	eqeq2d 2415	. . . . . . . . . . . . 13 |- ( h = ( _I |` Y ) -> ( F = ( h o. F ) <-> F = ( ( _I |` Y ) o. F ) ) )
93	90, 92	rmoi 3210	. . . . . . . . . . . 12 |- ( ( E* h e. ( ( J qTop F ) Cn ( J qTop F ) ) F = ( h o. F ) /\ ( ( g o. f ) e. ( ( J qTop F ) Cn ( J qTop F ) ) /\ F = ( ( g o. f ) o. F ) ) /\ ( ( _I |` Y ) e. ( ( J qTop F ) Cn ( J qTop F ) ) /\ F = ( ( _I |` Y ) o. F ) ) ) -> ( g o. f ) = ( _I |` Y ) )
94	73, 75, 79, 82, 88, 93	syl122anc 1193	. . . . . . . . . . 11 |- ( ( ( 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 ) )
95		fcof1o 5985	. . . . . . . . . . 11 |- ( ( ( f : Y --> Y /\ g : Y --> Y ) /\ ( ( f o. g ) = ( _I |` Y ) /\ ( g o. f ) = ( _I |` Y ) ) ) -> ( f : Y -1-1-onto-> Y /\ `' f = g ) )
96	37, 40, 68, 94, 95	syl22anc 1185	. . . . . . . . . 10 |- ( ( ( 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 -1-1-onto-> Y /\ `' f = g ) )
97	96	simprd 450	. . . . . . . . 9 |- ( ( ( 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 )
98	97, 38	eqeltrd 2478	. . . . . . . 8 |- ( ( ( 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 ) ) )
99	28, 98	rexlimddv 2794	. . . . . . 7 |- ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) -> `' f e. ( ( J qTop G ) Cn ( J qTop F ) ) )
100		ishmeo 17744	. . . . . . 7 |- ( 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 ) ) ) )
101	16, 99, 100	sylanbrc 646	. . . . . 6 |- ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) -> f e. ( ( J qTop F ) Homeo ( J qTop G ) ) )
102		simprr 734	. . . . . 6 |- ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) -> G = ( f o. F ) )
103	101, 102	jca 519	. . . . 5 |- ( ( ph /\ ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) ) -> ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ G = ( f o. F ) ) )
104	103	ex 424	. . . 4 |- ( ph -> ( ( f e. ( ( J qTop F ) Cn ( J qTop G ) ) /\ G = ( f o. F ) ) -> ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ G = ( f o. F ) ) ) )
105	104	reximdv2 2775	. . 3 |- ( ph -> ( E. f e. ( ( J qTop F ) Cn ( J qTop G ) ) G = ( f o. F ) -> E. f e. ( ( J qTop F ) Homeo ( J qTop G ) ) G = ( f o. F ) ) )
106	15, 105	mpd 15	. 2 |- ( ph -> E. f e. ( ( J qTop F ) Homeo ( J qTop G ) ) G = ( f o. F ) )
107		eqtr2 2422	. . . 4 |- ( ( G = ( f o. F ) /\ G = ( g o. F ) ) -> ( f o. F ) = ( g o. F ) )
108	2	adantr 452	. . . . 5 |- ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> F : X -onto-> Y )
109	30	adantr 452	. . . . . . 7 |- ( ( 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 ) )
110	33	adantr 452	. . . . . . 7 |- ( ( 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 ) )
111		simprl 733	. . . . . . 7 |- ( ( 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 ) ) )
112		hmeof1o2 17748	. . . . . . 7 |- ( ( ( 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 )
113	109, 110, 111, 112	syl3anc 1184	. . . . . 6 |- ( ( 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 )
114		f1ofn 5634	. . . . . 6 |- ( f : Y -1-1-onto-> Y -> f Fn Y )
115	113, 114	syl 16	. . . . 5 |- ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> f Fn Y )
116		simprr 734	. . . . . . 7 |- ( ( 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 ) ) )
117		hmeof1o2 17748	. . . . . . 7 |- ( ( ( 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 )
118	109, 110, 116, 117	syl3anc 1184	. . . . . 6 |- ( ( 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 )
119		f1ofn 5634	. . . . . 6 |- ( g : Y -1-1-onto-> Y -> g Fn Y )
120	118, 119	syl 16	. . . . 5 |- ( ( ph /\ ( f e. ( ( J qTop F ) Homeo ( J qTop G ) ) /\ g e. ( ( J qTop F ) Homeo ( J qTop G ) ) ) ) -> g Fn Y )
121		cocan2 5984	. . . . 5 |- ( ( F : X -onto-> Y /\ f Fn Y /\ g Fn Y ) -> ( ( f o. F ) = ( g o. F ) <-> f = g ) )
122	108, 115, 120, 121	syl3anc 1184	. . . 4 |- ( ( 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 ) )
123	107, 122	syl5ib 211	. . 3 |- ( ( 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 ) )
124	123	ralrimivva 2758	. 2 |- ( 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 ) )
125		coeq1 4989	. . . 4 |- ( f = g -> ( f o. F ) = ( g o. F ) )
126	125	eqeq2d 2415	. . 3 |- ( f = g -> ( G = ( f o. F ) <-> G = ( g o. F ) ) )
127	126	reu4 3088	. 2 |- ( 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 ) ) )
128	106, 124, 127	sylanbrc 646	1 |- ( ph -> E! f e. ( ( J qTop F ) Homeo ( J qTop G ) ) G = ( f o. F ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   A.wral 2666   E.wrex 2667   E!wreu 2668   E*wrmo 2669   _I cid 4453   `'ccnv 4836   |` cres 4839   o. ccom 4841   Fn wfn 5408   -->wf 5409   -onto->wfo 5411   -1-1-onto->wf1o 5412   ` cfv 5413  (class class class)co 6040   qTop cqtop 13684  TopOnctopon 16914   Cn ccn 17242   Homeo chmeo 17738

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-map 6979  df-qtop 13688  df-top 16918  df-topon 16921  df-cn 17245  df-hmeo 17740