Metamath Proof Explorer

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 ⊢ φ → J ∈ TopOn ⁡ X
qtopeu.3 ⊢ φ → F : X ⟶ onto Y
qtopeu.4 ⊢ φ → G ∈ J Cn K
qtopeu.5 ⊢ φ ∧ x ∈ X ∧ y ∈ X ∧ F ⁡ x = F ⁡ y → G ⁡ x = G ⁡ y
Assertion qtopeu ⊢ φ → ∃! f ∈ J qTop F Cn K G = f ∘ F

Proof

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