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	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
	qtopeu.3	$$⊢\phi \to F:X\underset{onto}{⟶}Y$$
	qtopeu.4	$$⊢\phi \to G\in \left(J\mathrm{Cn}K\right)$$
	qtopeu.5	$$⊢\left(\phi \wedge \left(x\in X\wedge y\in X\wedge F\left(x\right)=F\left(y\right)\right)\right)\to G\left(x\right)=G\left(y\right)$$
Assertion	qtopeu	$$⊢\phi \to \exists !f\in \left(\left(J\mathrm{qTop}F\right)\mathrm{Cn}K\right)G=f\circ F$$

Proof

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