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	$⊢ φ \to J \in TopOn (X)$
	qtophmeo.3	$⊢ φ \to F : X \underset{onto}{⟶} Y$
	qtophmeo.4	$⊢ φ \to G : X \underset{onto}{⟶} Y$
	qtophmeo.5	$⊢ (φ \land (x \in X \land y \in X)) \to (F (x) = F (y) \leftrightarrow G (x) = G (y))$
Assertion	qtophmeo	$⊢ φ \to \exists! f \in ((J qTop F) Homeo (J qTop G)) G = f \circ F$

Proof

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

Metamath Proof Explorer

Theorem qtophmeo

Proof