MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  qtopeu Structured version   Visualization version   GIF version

Theorem qtopeu 23724
Description: Universal property of the quotient topology. If 𝐺 is a function from 𝐽 to 𝐾 which is equal on all equivalent elements under 𝐹, then there is a unique continuous map 𝑓:(𝐽 / 𝐹)⟶𝐾 such that 𝐺 = 𝑓𝐹, and we say that 𝐺 "passes to the quotient". (Contributed by Mario Carneiro, 24-Mar-2015.)
Hypotheses
Ref Expression
qtopeu.1 (𝜑𝐽 ∈ (TopOn‘𝑋))
qtopeu.3 (𝜑𝐹:𝑋onto𝑌)
qtopeu.4 (𝜑𝐺 ∈ (𝐽 Cn 𝐾))
qtopeu.5 ((𝜑 ∧ (𝑥𝑋𝑦𝑋 ∧ (𝐹𝑥) = (𝐹𝑦))) → (𝐺𝑥) = (𝐺𝑦))
Assertion
Ref Expression
qtopeu (𝜑 → ∃!𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓𝐹))
Distinct variable groups:   𝑥,𝑓,𝑦,𝐹   𝑓,𝐽,𝑥   𝑓,𝐾,𝑥   𝑥,𝑋,𝑦   𝑓,𝐺,𝑥,𝑦   𝜑,𝑓,𝑥,𝑦   𝑓,𝑌,𝑥
Allowed substitution hints:   𝐽(𝑦)   𝐾(𝑦)   𝑋(𝑓)   𝑌(𝑦)

Proof of Theorem qtopeu
Dummy variables 𝑔 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 qtopeu.3 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑋onto𝑌)
2 fofn 6822 . . . . . . . . . . . . . . . 16 (𝐹:𝑋onto𝑌𝐹 Fn 𝑋)
31, 2syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹 Fn 𝑋)
43adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → 𝐹 Fn 𝑋)
5 fniniseg 7080 . . . . . . . . . . . . . 14 (𝐹 Fn 𝑋 → (𝑦 ∈ (𝐹 “ {(𝐹𝑥)}) ↔ (𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥))))
64, 5syl 17 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → (𝑦 ∈ (𝐹 “ {(𝐹𝑥)}) ↔ (𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥))))
7 eqcom 2744 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) = (𝐹𝑦) ↔ (𝐹𝑦) = (𝐹𝑥))
873anbi3i 1160 . . . . . . . . . . . . . . . . 17 ((𝑥𝑋𝑦𝑋 ∧ (𝐹𝑥) = (𝐹𝑦)) ↔ (𝑥𝑋𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥)))
9 3anass 1095 . . . . . . . . . . . . . . . . 17 ((𝑥𝑋𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥)) ↔ (𝑥𝑋 ∧ (𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥))))
108, 9bitri 275 . . . . . . . . . . . . . . . 16 ((𝑥𝑋𝑦𝑋 ∧ (𝐹𝑥) = (𝐹𝑦)) ↔ (𝑥𝑋 ∧ (𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥))))
11 qtopeu.5 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑋𝑦𝑋 ∧ (𝐹𝑥) = (𝐹𝑦))) → (𝐺𝑥) = (𝐺𝑦))
1210, 11sylan2br 595 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥)))) → (𝐺𝑥) = (𝐺𝑦))
1312eqcomd 2743 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥)))) → (𝐺𝑦) = (𝐺𝑥))
1413expr 456 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → ((𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥)) → (𝐺𝑦) = (𝐺𝑥)))
156, 14sylbid 240 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → (𝑦 ∈ (𝐹 “ {(𝐹𝑥)}) → (𝐺𝑦) = (𝐺𝑥)))
1615ralrimiv 3145 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → ∀𝑦 ∈ (𝐹 “ {(𝐹𝑥)})(𝐺𝑦) = (𝐺𝑥))
17 qtopeu.1 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ (TopOn‘𝑋))
18 qtopeu.4 . . . . . . . . . . . . . . . . 17 (𝜑𝐺 ∈ (𝐽 Cn 𝐾))
19 cntop2 23249 . . . . . . . . . . . . . . . . 17 (𝐺 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
2018, 19syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ Top)
21 toptopon2 22924 . . . . . . . . . . . . . . . 16 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘ 𝐾))
2220, 21sylib 218 . . . . . . . . . . . . . . 15 (𝜑𝐾 ∈ (TopOn‘ 𝐾))
23 cnf2 23257 . . . . . . . . . . . . . . 15 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘ 𝐾) ∧ 𝐺 ∈ (𝐽 Cn 𝐾)) → 𝐺:𝑋 𝐾)
2417, 22, 18, 23syl3anc 1373 . . . . . . . . . . . . . 14 (𝜑𝐺:𝑋 𝐾)
2524ffnd 6737 . . . . . . . . . . . . 13 (𝜑𝐺 Fn 𝑋)
2625adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → 𝐺 Fn 𝑋)
27 cnvimass 6100 . . . . . . . . . . . . 13 (𝐹 “ {(𝐹𝑥)}) ⊆ dom 𝐹
28 fof 6820 . . . . . . . . . . . . . . . 16 (𝐹:𝑋onto𝑌𝐹:𝑋𝑌)
291, 28syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝑋𝑌)
3029fdmd 6746 . . . . . . . . . . . . . 14 (𝜑 → dom 𝐹 = 𝑋)
3130adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → dom 𝐹 = 𝑋)
3227, 31sseqtrid 4026 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → (𝐹 “ {(𝐹𝑥)}) ⊆ 𝑋)
33 eqeq1 2741 . . . . . . . . . . . . 13 (𝑤 = (𝐺𝑦) → (𝑤 = (𝐺𝑥) ↔ (𝐺𝑦) = (𝐺𝑥)))
3433ralima 7257 . . . . . . . . . . . 12 ((𝐺 Fn 𝑋 ∧ (𝐹 “ {(𝐹𝑥)}) ⊆ 𝑋) → (∀𝑤 ∈ (𝐺 “ (𝐹 “ {(𝐹𝑥)}))𝑤 = (𝐺𝑥) ↔ ∀𝑦 ∈ (𝐹 “ {(𝐹𝑥)})(𝐺𝑦) = (𝐺𝑥)))
3526, 32, 34syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → (∀𝑤 ∈ (𝐺 “ (𝐹 “ {(𝐹𝑥)}))𝑤 = (𝐺𝑥) ↔ ∀𝑦 ∈ (𝐹 “ {(𝐹𝑥)})(𝐺𝑦) = (𝐺𝑥)))
3616, 35mpbird 257 . . . . . . . . . 10 ((𝜑𝑥𝑋) → ∀𝑤 ∈ (𝐺 “ (𝐹 “ {(𝐹𝑥)}))𝑤 = (𝐺𝑥))
3724fdmd 6746 . . . . . . . . . . . . . . 15 (𝜑 → dom 𝐺 = 𝑋)
3837eleq2d 2827 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ dom 𝐺𝑥𝑋))
3938biimpar 477 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → 𝑥 ∈ dom 𝐺)
40 simpr 484 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → 𝑥𝑋)
41 eqidd 2738 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝐹𝑥) = (𝐹𝑥))
42 fniniseg 7080 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝑋 → (𝑥 ∈ (𝐹 “ {(𝐹𝑥)}) ↔ (𝑥𝑋 ∧ (𝐹𝑥) = (𝐹𝑥))))
434, 42syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑥 ∈ (𝐹 “ {(𝐹𝑥)}) ↔ (𝑥𝑋 ∧ (𝐹𝑥) = (𝐹𝑥))))
4440, 41, 43mpbir2and 713 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → 𝑥 ∈ (𝐹 “ {(𝐹𝑥)}))
45 inelcm 4465 . . . . . . . . . . . . 13 ((𝑥 ∈ dom 𝐺𝑥 ∈ (𝐹 “ {(𝐹𝑥)})) → (dom 𝐺 ∩ (𝐹 “ {(𝐹𝑥)})) ≠ ∅)
4639, 44, 45syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → (dom 𝐺 ∩ (𝐹 “ {(𝐹𝑥)})) ≠ ∅)
47 imadisj 6098 . . . . . . . . . . . . 13 ((𝐺 “ (𝐹 “ {(𝐹𝑥)})) = ∅ ↔ (dom 𝐺 ∩ (𝐹 “ {(𝐹𝑥)})) = ∅)
4847necon3bii 2993 . . . . . . . . . . . 12 ((𝐺 “ (𝐹 “ {(𝐹𝑥)})) ≠ ∅ ↔ (dom 𝐺 ∩ (𝐹 “ {(𝐹𝑥)})) ≠ ∅)
4946, 48sylibr 234 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → (𝐺 “ (𝐹 “ {(𝐹𝑥)})) ≠ ∅)
50 eqsn 4829 . . . . . . . . . . 11 ((𝐺 “ (𝐹 “ {(𝐹𝑥)})) ≠ ∅ → ((𝐺 “ (𝐹 “ {(𝐹𝑥)})) = {(𝐺𝑥)} ↔ ∀𝑤 ∈ (𝐺 “ (𝐹 “ {(𝐹𝑥)}))𝑤 = (𝐺𝑥)))
5149, 50syl 17 . . . . . . . . . 10 ((𝜑𝑥𝑋) → ((𝐺 “ (𝐹 “ {(𝐹𝑥)})) = {(𝐺𝑥)} ↔ ∀𝑤 ∈ (𝐺 “ (𝐹 “ {(𝐹𝑥)}))𝑤 = (𝐺𝑥)))
5236, 51mpbird 257 . . . . . . . . 9 ((𝜑𝑥𝑋) → (𝐺 “ (𝐹 “ {(𝐹𝑥)})) = {(𝐺𝑥)})
5352unieqd 4920 . . . . . . . 8 ((𝜑𝑥𝑋) → (𝐺 “ (𝐹 “ {(𝐹𝑥)})) = {(𝐺𝑥)})
54 fvex 6919 . . . . . . . . 9 (𝐺𝑥) ∈ V
5554unisn 4926 . . . . . . . 8 {(𝐺𝑥)} = (𝐺𝑥)
5653, 55eqtr2di 2794 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐺𝑥) = (𝐺 “ (𝐹 “ {(𝐹𝑥)})))
5756mpteq2dva 5242 . . . . . 6 (𝜑 → (𝑥𝑋 ↦ (𝐺𝑥)) = (𝑥𝑋 (𝐺 “ (𝐹 “ {(𝐹𝑥)}))))
5824feqmptd 6977 . . . . . 6 (𝜑𝐺 = (𝑥𝑋 ↦ (𝐺𝑥)))
5929ffvelcdmda 7104 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐹𝑥) ∈ 𝑌)
6029feqmptd 6977 . . . . . . 7 (𝜑𝐹 = (𝑥𝑋 ↦ (𝐹𝑥)))
61 eqidd 2738 . . . . . . 7 (𝜑 → (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) = (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))))
62 sneq 4636 . . . . . . . . . 10 (𝑤 = (𝐹𝑥) → {𝑤} = {(𝐹𝑥)})
6362imaeq2d 6078 . . . . . . . . 9 (𝑤 = (𝐹𝑥) → (𝐹 “ {𝑤}) = (𝐹 “ {(𝐹𝑥)}))
6463imaeq2d 6078 . . . . . . . 8 (𝑤 = (𝐹𝑥) → (𝐺 “ (𝐹 “ {𝑤})) = (𝐺 “ (𝐹 “ {(𝐹𝑥)})))
6564unieqd 4920 . . . . . . 7 (𝑤 = (𝐹𝑥) → (𝐺 “ (𝐹 “ {𝑤})) = (𝐺 “ (𝐹 “ {(𝐹𝑥)})))
6659, 60, 61, 65fmptco 7149 . . . . . 6 (𝜑 → ((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∘ 𝐹) = (𝑥𝑋 (𝐺 “ (𝐹 “ {(𝐹𝑥)}))))
6757, 58, 663eqtr4d 2787 . . . . 5 (𝜑𝐺 = ((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∘ 𝐹))
6867, 18eqeltrrd 2842 . . . 4 (𝜑 → ((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∘ 𝐹) ∈ (𝐽 Cn 𝐾))
6924ffvelcdmda 7104 . . . . . . . . 9 ((𝜑𝑥𝑋) → (𝐺𝑥) ∈ 𝐾)
7056, 69eqeltrrd 2842 . . . . . . . 8 ((𝜑𝑥𝑋) → (𝐺 “ (𝐹 “ {(𝐹𝑥)})) ∈ 𝐾)
7170ralrimiva 3146 . . . . . . 7 (𝜑 → ∀𝑥𝑋 (𝐺 “ (𝐹 “ {(𝐹𝑥)})) ∈ 𝐾)
7265eqcomd 2743 . . . . . . . . . . 11 (𝑤 = (𝐹𝑥) → (𝐺 “ (𝐹 “ {(𝐹𝑥)})) = (𝐺 “ (𝐹 “ {𝑤})))
7372eqcoms 2745 . . . . . . . . . 10 ((𝐹𝑥) = 𝑤 (𝐺 “ (𝐹 “ {(𝐹𝑥)})) = (𝐺 “ (𝐹 “ {𝑤})))
7473eleq1d 2826 . . . . . . . . 9 ((𝐹𝑥) = 𝑤 → ( (𝐺 “ (𝐹 “ {(𝐹𝑥)})) ∈ 𝐾 (𝐺 “ (𝐹 “ {𝑤})) ∈ 𝐾))
7574cbvfo 7309 . . . . . . . 8 (𝐹:𝑋onto𝑌 → (∀𝑥𝑋 (𝐺 “ (𝐹 “ {(𝐹𝑥)})) ∈ 𝐾 ↔ ∀𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤})) ∈ 𝐾))
761, 75syl 17 . . . . . . 7 (𝜑 → (∀𝑥𝑋 (𝐺 “ (𝐹 “ {(𝐹𝑥)})) ∈ 𝐾 ↔ ∀𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤})) ∈ 𝐾))
7771, 76mpbid 232 . . . . . 6 (𝜑 → ∀𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤})) ∈ 𝐾)
78 eqid 2737 . . . . . . 7 (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) = (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤})))
7978fmpt 7130 . . . . . 6 (∀𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤})) ∈ 𝐾 ↔ (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))):𝑌 𝐾)
8077, 79sylib 218 . . . . 5 (𝜑 → (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))):𝑌 𝐾)
81 qtopcn 23722 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘ 𝐾)) ∧ (𝐹:𝑋onto𝑌 ∧ (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))):𝑌 𝐾)) → ((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ ((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∘ 𝐹) ∈ (𝐽 Cn 𝐾)))
8217, 22, 1, 80, 81syl22anc 839 . . . 4 (𝜑 → ((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ ((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∘ 𝐹) ∈ (𝐽 Cn 𝐾)))
8368, 82mpbird 257 . . 3 (𝜑 → (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾))
84 coeq1 5868 . . . 4 (𝑓 = (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) → (𝑓𝐹) = ((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∘ 𝐹))
8584rspceeqv 3645 . . 3 (((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝐺 = ((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∘ 𝐹)) → ∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓𝐹))
8683, 67, 85syl2anc 584 . 2 (𝜑 → ∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓𝐹))
87 eqtr2 2761 . . . 4 ((𝐺 = (𝑓𝐹) ∧ 𝐺 = (𝑔𝐹)) → (𝑓𝐹) = (𝑔𝐹))
881adantr 480 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝐹:𝑋onto𝑌)
89 qtoptopon 23712 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
9017, 1, 89syl2anc 584 . . . . . . . 8 (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
9190adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
9222adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝐾 ∈ (TopOn‘ 𝐾))
93 simprl 771 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))
94 cnf2 23257 . . . . . . 7 (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘ 𝐾) ∧ 𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) → 𝑓:𝑌 𝐾)
9591, 92, 93, 94syl3anc 1373 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑓:𝑌 𝐾)
9695ffnd 6737 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑓 Fn 𝑌)
97 simprr 773 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))
98 cnf2 23257 . . . . . . 7 (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘ 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) → 𝑔:𝑌 𝐾)
9991, 92, 97, 98syl3anc 1373 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑔:𝑌 𝐾)
10099ffnd 6737 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑔 Fn 𝑌)
101 cocan2 7312 . . . . 5 ((𝐹:𝑋onto𝑌𝑓 Fn 𝑌𝑔 Fn 𝑌) → ((𝑓𝐹) = (𝑔𝐹) ↔ 𝑓 = 𝑔))
10288, 96, 100, 101syl3anc 1373 . . . 4 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → ((𝑓𝐹) = (𝑔𝐹) ↔ 𝑓 = 𝑔))
10387, 102imbitrid 244 . . 3 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → ((𝐺 = (𝑓𝐹) ∧ 𝐺 = (𝑔𝐹)) → 𝑓 = 𝑔))
104103ralrimivva 3202 . 2 (𝜑 → ∀𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)∀𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)((𝐺 = (𝑓𝐹) ∧ 𝐺 = (𝑔𝐹)) → 𝑓 = 𝑔))
105 coeq1 5868 . . . 4 (𝑓 = 𝑔 → (𝑓𝐹) = (𝑔𝐹))
106105eqeq2d 2748 . . 3 (𝑓 = 𝑔 → (𝐺 = (𝑓𝐹) ↔ 𝐺 = (𝑔𝐹)))
107106reu4 3737 . 2 (∃!𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓𝐹) ↔ (∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓𝐹) ∧ ∀𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)∀𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)((𝐺 = (𝑓𝐹) ∧ 𝐺 = (𝑔𝐹)) → 𝑓 = 𝑔)))
10886, 104, 107sylanbrc 583 1 (𝜑 → ∃!𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wral 3061  wrex 3070  ∃!wreu 3378  cin 3950  wss 3951  c0 4333  {csn 4626   cuni 4907  cmpt 5225  ccnv 5684  dom cdm 5685  cima 5688  ccom 5689   Fn wfn 6556  wf 6557  ontowfo 6559  cfv 6561  (class class class)co 7431   qTop cqtop 17548  Topctop 22899  TopOnctopon 22916   Cn ccn 23232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8868  df-qtop 17552  df-top 22900  df-topon 22917  df-cn 23235
This theorem is referenced by:  qtophmeo  23825
  Copyright terms: Public domain W3C validator