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

Theorem qtopeu 23739
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 7079 . . . . . . . . . . . . . 14 (𝐹 Fn 𝑋 → (𝑦 ∈ (𝐹 “ {(𝐹𝑥)}) ↔ (𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥))))
64, 5syl 17 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → (𝑦 ∈ (𝐹 “ {(𝐹𝑥)}) ↔ (𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥))))
7 eqcom 2741 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) = (𝐹𝑦) ↔ (𝐹𝑦) = (𝐹𝑥))
873anbi3i 1158 . . . . . . . . . . . . . . . . 17 ((𝑥𝑋𝑦𝑋 ∧ (𝐹𝑥) = (𝐹𝑦)) ↔ (𝑥𝑋𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥)))
9 3anass 1094 . . . . . . . . . . . . . . . . 17 ((𝑥𝑋𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥)) ↔ (𝑥𝑋 ∧ (𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥))))
108, 9bitri 275 . . . . . . . . . . . . . . . 16 ((𝑥𝑋𝑦𝑋 ∧ (𝐹𝑥) = (𝐹𝑦)) ↔ (𝑥𝑋 ∧ (𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥))))
11 qtopeu.5 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑋𝑦𝑋 ∧ (𝐹𝑥) = (𝐹𝑦))) → (𝐺𝑥) = (𝐺𝑦))
1210, 11sylan2br 595 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥)))) → (𝐺𝑥) = (𝐺𝑦))
1312eqcomd 2740 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝑋 ∧ (𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥)))) → (𝐺𝑦) = (𝐺𝑥))
1413expr 456 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → ((𝑦𝑋 ∧ (𝐹𝑦) = (𝐹𝑥)) → (𝐺𝑦) = (𝐺𝑥)))
156, 14sylbid 240 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → (𝑦 ∈ (𝐹 “ {(𝐹𝑥)}) → (𝐺𝑦) = (𝐺𝑥)))
1615ralrimiv 3142 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → ∀𝑦 ∈ (𝐹 “ {(𝐹𝑥)})(𝐺𝑦) = (𝐺𝑥))
17 qtopeu.1 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ (TopOn‘𝑋))
18 qtopeu.4 . . . . . . . . . . . . . . . . 17 (𝜑𝐺 ∈ (𝐽 Cn 𝐾))
19 cntop2 23264 . . . . . . . . . . . . . . . . 17 (𝐺 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
2018, 19syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ Top)
21 toptopon2 22939 . . . . . . . . . . . . . . . 16 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘ 𝐾))
2220, 21sylib 218 . . . . . . . . . . . . . . 15 (𝜑𝐾 ∈ (TopOn‘ 𝐾))
23 cnf2 23272 . . . . . . . . . . . . . . 15 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘ 𝐾) ∧ 𝐺 ∈ (𝐽 Cn 𝐾)) → 𝐺:𝑋 𝐾)
2417, 22, 18, 23syl3anc 1370 . . . . . . . . . . . . . 14 (𝜑𝐺:𝑋 𝐾)
2524ffnd 6737 . . . . . . . . . . . . 13 (𝜑𝐺 Fn 𝑋)
2625adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → 𝐺 Fn 𝑋)
27 cnvimass 6101 . . . . . . . . . . . . 13 (𝐹 “ {(𝐹𝑥)}) ⊆ dom 𝐹
28 fof 6820 . . . . . . . . . . . . . . . 16 (𝐹:𝑋onto𝑌𝐹:𝑋𝑌)
291, 28syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝑋𝑌)
3029fdmd 6746 . . . . . . . . . . . . . 14 (𝜑 → dom 𝐹 = 𝑋)
3130adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → dom 𝐹 = 𝑋)
3227, 31sseqtrid 4047 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → (𝐹 “ {(𝐹𝑥)}) ⊆ 𝑋)
33 eqeq1 2738 . . . . . . . . . . . . 13 (𝑤 = (𝐺𝑦) → (𝑤 = (𝐺𝑥) ↔ (𝐺𝑦) = (𝐺𝑥)))
3433ralima 7256 . . . . . . . . . . . 12 ((𝐺 Fn 𝑋 ∧ (𝐹 “ {(𝐹𝑥)}) ⊆ 𝑋) → (∀𝑤 ∈ (𝐺 “ (𝐹 “ {(𝐹𝑥)}))𝑤 = (𝐺𝑥) ↔ ∀𝑦 ∈ (𝐹 “ {(𝐹𝑥)})(𝐺𝑦) = (𝐺𝑥)))
3526, 32, 34syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → (∀𝑤 ∈ (𝐺 “ (𝐹 “ {(𝐹𝑥)}))𝑤 = (𝐺𝑥) ↔ ∀𝑦 ∈ (𝐹 “ {(𝐹𝑥)})(𝐺𝑦) = (𝐺𝑥)))
3616, 35mpbird 257 . . . . . . . . . 10 ((𝜑𝑥𝑋) → ∀𝑤 ∈ (𝐺 “ (𝐹 “ {(𝐹𝑥)}))𝑤 = (𝐺𝑥))
3724fdmd 6746 . . . . . . . . . . . . . . 15 (𝜑 → dom 𝐺 = 𝑋)
3837eleq2d 2824 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ dom 𝐺𝑥𝑋))
3938biimpar 477 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → 𝑥 ∈ dom 𝐺)
40 simpr 484 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → 𝑥𝑋)
41 eqidd 2735 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝐹𝑥) = (𝐹𝑥))
42 fniniseg 7079 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝑋 → (𝑥 ∈ (𝐹 “ {(𝐹𝑥)}) ↔ (𝑥𝑋 ∧ (𝐹𝑥) = (𝐹𝑥))))
434, 42syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑥 ∈ (𝐹 “ {(𝐹𝑥)}) ↔ (𝑥𝑋 ∧ (𝐹𝑥) = (𝐹𝑥))))
4440, 41, 43mpbir2and 713 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → 𝑥 ∈ (𝐹 “ {(𝐹𝑥)}))
45 inelcm 4470 . . . . . . . . . . . . 13 ((𝑥 ∈ dom 𝐺𝑥 ∈ (𝐹 “ {(𝐹𝑥)})) → (dom 𝐺 ∩ (𝐹 “ {(𝐹𝑥)})) ≠ ∅)
4639, 44, 45syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → (dom 𝐺 ∩ (𝐹 “ {(𝐹𝑥)})) ≠ ∅)
47 imadisj 6099 . . . . . . . . . . . . 13 ((𝐺 “ (𝐹 “ {(𝐹𝑥)})) = ∅ ↔ (dom 𝐺 ∩ (𝐹 “ {(𝐹𝑥)})) = ∅)
4847necon3bii 2990 . . . . . . . . . . . 12 ((𝐺 “ (𝐹 “ {(𝐹𝑥)})) ≠ ∅ ↔ (dom 𝐺 ∩ (𝐹 “ {(𝐹𝑥)})) ≠ ∅)
4946, 48sylibr 234 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → (𝐺 “ (𝐹 “ {(𝐹𝑥)})) ≠ ∅)
50 eqsn 4833 . . . . . . . . . . 11 ((𝐺 “ (𝐹 “ {(𝐹𝑥)})) ≠ ∅ → ((𝐺 “ (𝐹 “ {(𝐹𝑥)})) = {(𝐺𝑥)} ↔ ∀𝑤 ∈ (𝐺 “ (𝐹 “ {(𝐹𝑥)}))𝑤 = (𝐺𝑥)))
5149, 50syl 17 . . . . . . . . . 10 ((𝜑𝑥𝑋) → ((𝐺 “ (𝐹 “ {(𝐹𝑥)})) = {(𝐺𝑥)} ↔ ∀𝑤 ∈ (𝐺 “ (𝐹 “ {(𝐹𝑥)}))𝑤 = (𝐺𝑥)))
5236, 51mpbird 257 . . . . . . . . 9 ((𝜑𝑥𝑋) → (𝐺 “ (𝐹 “ {(𝐹𝑥)})) = {(𝐺𝑥)})
5352unieqd 4924 . . . . . . . 8 ((𝜑𝑥𝑋) → (𝐺 “ (𝐹 “ {(𝐹𝑥)})) = {(𝐺𝑥)})
54 fvex 6919 . . . . . . . . 9 (𝐺𝑥) ∈ V
5554unisn 4930 . . . . . . . 8 {(𝐺𝑥)} = (𝐺𝑥)
5653, 55eqtr2di 2791 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐺𝑥) = (𝐺 “ (𝐹 “ {(𝐹𝑥)})))
5756mpteq2dva 5247 . . . . . 6 (𝜑 → (𝑥𝑋 ↦ (𝐺𝑥)) = (𝑥𝑋 (𝐺 “ (𝐹 “ {(𝐹𝑥)}))))
5824feqmptd 6976 . . . . . 6 (𝜑𝐺 = (𝑥𝑋 ↦ (𝐺𝑥)))
5929ffvelcdmda 7103 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐹𝑥) ∈ 𝑌)
6029feqmptd 6976 . . . . . . 7 (𝜑𝐹 = (𝑥𝑋 ↦ (𝐹𝑥)))
61 eqidd 2735 . . . . . . 7 (𝜑 → (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) = (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))))
62 sneq 4640 . . . . . . . . . 10 (𝑤 = (𝐹𝑥) → {𝑤} = {(𝐹𝑥)})
6362imaeq2d 6079 . . . . . . . . 9 (𝑤 = (𝐹𝑥) → (𝐹 “ {𝑤}) = (𝐹 “ {(𝐹𝑥)}))
6463imaeq2d 6079 . . . . . . . 8 (𝑤 = (𝐹𝑥) → (𝐺 “ (𝐹 “ {𝑤})) = (𝐺 “ (𝐹 “ {(𝐹𝑥)})))
6564unieqd 4924 . . . . . . 7 (𝑤 = (𝐹𝑥) → (𝐺 “ (𝐹 “ {𝑤})) = (𝐺 “ (𝐹 “ {(𝐹𝑥)})))
6659, 60, 61, 65fmptco 7148 . . . . . 6 (𝜑 → ((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∘ 𝐹) = (𝑥𝑋 (𝐺 “ (𝐹 “ {(𝐹𝑥)}))))
6757, 58, 663eqtr4d 2784 . . . . 5 (𝜑𝐺 = ((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∘ 𝐹))
6867, 18eqeltrrd 2839 . . . 4 (𝜑 → ((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∘ 𝐹) ∈ (𝐽 Cn 𝐾))
6924ffvelcdmda 7103 . . . . . . . . 9 ((𝜑𝑥𝑋) → (𝐺𝑥) ∈ 𝐾)
7056, 69eqeltrrd 2839 . . . . . . . 8 ((𝜑𝑥𝑋) → (𝐺 “ (𝐹 “ {(𝐹𝑥)})) ∈ 𝐾)
7170ralrimiva 3143 . . . . . . 7 (𝜑 → ∀𝑥𝑋 (𝐺 “ (𝐹 “ {(𝐹𝑥)})) ∈ 𝐾)
7265eqcomd 2740 . . . . . . . . . . 11 (𝑤 = (𝐹𝑥) → (𝐺 “ (𝐹 “ {(𝐹𝑥)})) = (𝐺 “ (𝐹 “ {𝑤})))
7372eqcoms 2742 . . . . . . . . . 10 ((𝐹𝑥) = 𝑤 (𝐺 “ (𝐹 “ {(𝐹𝑥)})) = (𝐺 “ (𝐹 “ {𝑤})))
7473eleq1d 2823 . . . . . . . . 9 ((𝐹𝑥) = 𝑤 → ( (𝐺 “ (𝐹 “ {(𝐹𝑥)})) ∈ 𝐾 (𝐺 “ (𝐹 “ {𝑤})) ∈ 𝐾))
7574cbvfo 7308 . . . . . . . 8 (𝐹:𝑋onto𝑌 → (∀𝑥𝑋 (𝐺 “ (𝐹 “ {(𝐹𝑥)})) ∈ 𝐾 ↔ ∀𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤})) ∈ 𝐾))
761, 75syl 17 . . . . . . 7 (𝜑 → (∀𝑥𝑋 (𝐺 “ (𝐹 “ {(𝐹𝑥)})) ∈ 𝐾 ↔ ∀𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤})) ∈ 𝐾))
7771, 76mpbid 232 . . . . . 6 (𝜑 → ∀𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤})) ∈ 𝐾)
78 eqid 2734 . . . . . . 7 (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) = (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤})))
7978fmpt 7129 . . . . . 6 (∀𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤})) ∈ 𝐾 ↔ (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))):𝑌 𝐾)
8077, 79sylib 218 . . . . 5 (𝜑 → (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))):𝑌 𝐾)
81 qtopcn 23737 . . . . 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 5870 . . . 4 (𝑓 = (𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) → (𝑓𝐹) = ((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∘ 𝐹))
8584rspceeqv 3644 . . 3 (((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝐺 = ((𝑤𝑌 (𝐺 “ (𝐹 “ {𝑤}))) ∘ 𝐹)) → ∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓𝐹))
8683, 67, 85syl2anc 584 . 2 (𝜑 → ∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓𝐹))
87 eqtr2 2758 . . . 4 ((𝐺 = (𝑓𝐹) ∧ 𝐺 = (𝑔𝐹)) → (𝑓𝐹) = (𝑔𝐹))
881adantr 480 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝐹:𝑋onto𝑌)
89 qtoptopon 23727 . . . . . . . . 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 23272 . . . . . . 7 (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘ 𝐾) ∧ 𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) → 𝑓:𝑌 𝐾)
9591, 92, 93, 94syl3anc 1370 . . . . . 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 23272 . . . . . . 7 (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘ 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) → 𝑔:𝑌 𝐾)
9991, 92, 97, 98syl3anc 1370 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑔:𝑌 𝐾)
10099ffnd 6737 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑔 Fn 𝑌)
101 cocan2 7311 . . . . 5 ((𝐹:𝑋onto𝑌𝑓 Fn 𝑌𝑔 Fn 𝑌) → ((𝑓𝐹) = (𝑔𝐹) ↔ 𝑓 = 𝑔))
10288, 96, 100, 101syl3anc 1370 . . . 4 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → ((𝑓𝐹) = (𝑔𝐹) ↔ 𝑓 = 𝑔))
10387, 102imbitrid 244 . . 3 ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → ((𝐺 = (𝑓𝐹) ∧ 𝐺 = (𝑔𝐹)) → 𝑓 = 𝑔))
104103ralrimivva 3199 . 2 (𝜑 → ∀𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)∀𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)((𝐺 = (𝑓𝐹) ∧ 𝐺 = (𝑔𝐹)) → 𝑓 = 𝑔))
105 coeq1 5870 . . . 4 (𝑓 = 𝑔 → (𝑓𝐹) = (𝑔𝐹))
106105eqeq2d 2745 . . 3 (𝑓 = 𝑔 → (𝐺 = (𝑓𝐹) ↔ 𝐺 = (𝑔𝐹)))
107106reu4 3739 . 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 1086   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  ∃!wreu 3375  cin 3961  wss 3962  c0 4338  {csn 4630   cuni 4911  cmpt 5230  ccnv 5687  dom cdm 5688  cima 5691  ccom 5692   Fn wfn 6557  wf 6558  ontowfo 6560  cfv 6562  (class class class)co 7430   qTop cqtop 17549  Topctop 22914  TopOnctopon 22931   Cn ccn 23247
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-map 8866  df-qtop 17553  df-top 22915  df-topon 22932  df-cn 23250
This theorem is referenced by:  qtophmeo  23840
  Copyright terms: Public domain W3C validator