Step | Hyp | Ref
| Expression |
1 | | qtopeu.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) |
2 | | fofn 6635 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹 Fn 𝑋) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 Fn 𝑋) |
4 | 3 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐹 Fn 𝑋) |
5 | | fniniseg 6880 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝑋 → (𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) ↔ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) ↔ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) |
7 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = (𝐹‘𝑥)) |
8 | 7 | 3anbi3i 1161 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥))) |
9 | | 3anass 1097 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) |
10 | 8, 9 | bitri 278 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) |
11 | | qtopeu.5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐺‘𝑥) = (𝐺‘𝑦)) |
12 | 10, 11 | sylan2br 598 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) → (𝐺‘𝑥) = (𝐺‘𝑦)) |
13 | 12 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) → (𝐺‘𝑦) = (𝐺‘𝑥)) |
14 | 13 | expr 460 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)) → (𝐺‘𝑦) = (𝐺‘𝑥))) |
15 | 6, 14 | sylbid 243 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) → (𝐺‘𝑦) = (𝐺‘𝑥))) |
16 | 15 | ralrimiv 3104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)})(𝐺‘𝑦) = (𝐺‘𝑥)) |
17 | | qtopeu.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
18 | | qtopeu.4 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) |
19 | | cntop2 22138 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ Top) |
21 | | toptopon2 21815 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
22 | 20, 21 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
23 | | cnf2 22146 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐺 ∈ (𝐽 Cn 𝐾)) → 𝐺:𝑋⟶∪ 𝐾) |
24 | 17, 22, 18, 23 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:𝑋⟶∪ 𝐾) |
25 | 24 | ffnd 6546 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 Fn 𝑋) |
26 | 25 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐺 Fn 𝑋) |
27 | | cnvimass 5949 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 “ {(𝐹‘𝑥)}) ⊆ dom 𝐹 |
28 | | fof 6633 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
29 | 1, 28 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) |
30 | 29 | fdmd 6556 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝐹 = 𝑋) |
31 | 30 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → dom 𝐹 = 𝑋) |
32 | 27, 31 | sseqtrid 3953 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (◡𝐹 “ {(𝐹‘𝑥)}) ⊆ 𝑋) |
33 | | eqeq1 2741 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐺‘𝑦) → (𝑤 = (𝐺‘𝑥) ↔ (𝐺‘𝑦) = (𝐺‘𝑥))) |
34 | 33 | ralima 7054 |
. . . . . . . . . . . 12
⊢ ((𝐺 Fn 𝑋 ∧ (◡𝐹 “ {(𝐹‘𝑥)}) ⊆ 𝑋) → (∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥) ↔ ∀𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)})(𝐺‘𝑦) = (𝐺‘𝑥))) |
35 | 26, 32, 34 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥) ↔ ∀𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)})(𝐺‘𝑦) = (𝐺‘𝑥))) |
36 | 16, 35 | mpbird 260 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥)) |
37 | 24 | fdmd 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝐺 = 𝑋) |
38 | 37 | eleq2d 2823 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ dom 𝐺 ↔ 𝑥 ∈ 𝑋)) |
39 | 38 | biimpar 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ dom 𝐺) |
40 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
41 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
42 | | fniniseg 6880 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 Fn 𝑋 → (𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) ↔ (𝑥 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑥)))) |
43 | 4, 42 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) ↔ (𝑥 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑥)))) |
44 | 40, 41, 43 | mpbir2and 713 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑥)})) |
45 | | inelcm 4379 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑥)})) → (dom 𝐺 ∩ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅) |
46 | 39, 44, 45 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (dom 𝐺 ∩ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅) |
47 | | imadisj 5948 |
. . . . . . . . . . . . 13
⊢ ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = ∅ ↔ (dom 𝐺 ∩ (◡𝐹 “ {(𝐹‘𝑥)})) = ∅) |
48 | 47 | necon3bii 2993 |
. . . . . . . . . . . 12
⊢ ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅ ↔ (dom 𝐺 ∩ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅) |
49 | 46, 48 | sylibr 237 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅) |
50 | | eqsn 4742 |
. . . . . . . . . . 11
⊢ ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅ → ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = {(𝐺‘𝑥)} ↔ ∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥))) |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = {(𝐺‘𝑥)} ↔ ∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥))) |
52 | 36, 51 | mpbird 260 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = {(𝐺‘𝑥)}) |
53 | 52 | unieqd 4833 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = ∪ {(𝐺‘𝑥)}) |
54 | | fvex 6730 |
. . . . . . . . 9
⊢ (𝐺‘𝑥) ∈ V |
55 | 54 | unisn 4841 |
. . . . . . . 8
⊢ ∪ {(𝐺‘𝑥)} = (𝐺‘𝑥) |
56 | 53, 55 | eqtr2di 2795 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) = ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))) |
57 | 56 | mpteq2dva 5150 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥)) = (𝑥 ∈ 𝑋 ↦ ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})))) |
58 | 24 | feqmptd 6780 |
. . . . . 6
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) |
59 | 29 | ffvelrnda 6904 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ 𝑌) |
60 | 29 | feqmptd 6780 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
61 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) = (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤})))) |
62 | | sneq 4551 |
. . . . . . . . . 10
⊢ (𝑤 = (𝐹‘𝑥) → {𝑤} = {(𝐹‘𝑥)}) |
63 | 62 | imaeq2d 5929 |
. . . . . . . . 9
⊢ (𝑤 = (𝐹‘𝑥) → (◡𝐹 “ {𝑤}) = (◡𝐹 “ {(𝐹‘𝑥)})) |
64 | 63 | imaeq2d 5929 |
. . . . . . . 8
⊢ (𝑤 = (𝐹‘𝑥) → (𝐺 “ (◡𝐹 “ {𝑤})) = (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))) |
65 | 64 | unieqd 4833 |
. . . . . . 7
⊢ (𝑤 = (𝐹‘𝑥) → ∪ (𝐺 “ (◡𝐹 “ {𝑤})) = ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))) |
66 | 59, 60, 61, 65 | fmptco 6944 |
. . . . . 6
⊢ (𝜑 → ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹) = (𝑥 ∈ 𝑋 ↦ ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})))) |
67 | 57, 58, 66 | 3eqtr4d 2787 |
. . . . 5
⊢ (𝜑 → 𝐺 = ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹)) |
68 | 67, 18 | eqeltrrd 2839 |
. . . 4
⊢ (𝜑 → ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹) ∈ (𝐽 Cn 𝐾)) |
69 | 24 | ffvelrnda 6904 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) ∈ ∪ 𝐾) |
70 | 56, 69 | eqeltrrd 2839 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾) |
71 | 70 | ralrimiva 3105 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾) |
72 | 65 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝐹‘𝑥) → ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) |
73 | 72 | eqcoms 2745 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) = 𝑤 → ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) |
74 | 73 | eleq1d 2822 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) = 𝑤 → (∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾 ↔ ∪ (𝐺
“ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾)) |
75 | 74 | cbvfo 7099 |
. . . . . . . 8
⊢ (𝐹:𝑋–onto→𝑌 → (∀𝑥 ∈ 𝑋 ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾 ↔ ∀𝑤 ∈ 𝑌 ∪ (𝐺 “ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾)) |
76 | 1, 75 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾 ↔ ∀𝑤 ∈ 𝑌 ∪ (𝐺 “ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾)) |
77 | 71, 76 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → ∀𝑤 ∈ 𝑌 ∪ (𝐺 “ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾) |
78 | | eqid 2737 |
. . . . . . 7
⊢ (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) = (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) |
79 | 78 | fmpt 6927 |
. . . . . 6
⊢
(∀𝑤 ∈
𝑌 ∪ (𝐺
“ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾 ↔ (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))):𝑌⟶∪ 𝐾) |
80 | 77, 79 | sylib 221 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))):𝑌⟶∪ 𝐾) |
81 | | qtopcn 22611 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾))
∧ (𝐹:𝑋–onto→𝑌 ∧ (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))):𝑌⟶∪ 𝐾)) → ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹) ∈ (𝐽 Cn 𝐾))) |
82 | 17, 22, 1, 80, 81 | syl22anc 839 |
. . . 4
⊢ (𝜑 → ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹) ∈ (𝐽 Cn 𝐾))) |
83 | 68, 82 | mpbird 260 |
. . 3
⊢ (𝜑 → (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) |
84 | | coeq1 5726 |
. . . 4
⊢ (𝑓 = (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) → (𝑓 ∘ 𝐹) = ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹)) |
85 | 84 | rspceeqv 3552 |
. . 3
⊢ (((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝐺 = ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹)) → ∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹)) |
86 | 83, 67, 85 | syl2anc 587 |
. 2
⊢ (𝜑 → ∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹)) |
87 | | eqtr2 2761 |
. . . 4
⊢ ((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → (𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹)) |
88 | 1 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝐹:𝑋–onto→𝑌) |
89 | | qtoptopon 22601 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
90 | 17, 1, 89 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
91 | 90 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
92 | 22 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
93 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) |
94 | | cnf2 22146 |
. . . . . . 7
⊢ (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) → 𝑓:𝑌⟶∪ 𝐾) |
95 | 91, 92, 93, 94 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑓:𝑌⟶∪ 𝐾) |
96 | 95 | ffnd 6546 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑓 Fn 𝑌) |
97 | | simprr 773 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) |
98 | | cnf2 22146 |
. . . . . . 7
⊢ (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) → 𝑔:𝑌⟶∪ 𝐾) |
99 | 91, 92, 97, 98 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑔:𝑌⟶∪ 𝐾) |
100 | 99 | ffnd 6546 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑔 Fn 𝑌) |
101 | | cocan2 7102 |
. . . . 5
⊢ ((𝐹:𝑋–onto→𝑌 ∧ 𝑓 Fn 𝑌 ∧ 𝑔 Fn 𝑌) → ((𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹) ↔ 𝑓 = 𝑔)) |
102 | 88, 96, 100, 101 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → ((𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹) ↔ 𝑓 = 𝑔)) |
103 | 87, 102 | syl5ib 247 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → ((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → 𝑓 = 𝑔)) |
104 | 103 | ralrimivva 3112 |
. 2
⊢ (𝜑 → ∀𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)∀𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → 𝑓 = 𝑔)) |
105 | | coeq1 5726 |
. . . 4
⊢ (𝑓 = 𝑔 → (𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹)) |
106 | 105 | eqeq2d 2748 |
. . 3
⊢ (𝑓 = 𝑔 → (𝐺 = (𝑓 ∘ 𝐹) ↔ 𝐺 = (𝑔 ∘ 𝐹))) |
107 | 106 | reu4 3644 |
. 2
⊢
(∃!𝑓 ∈
((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹) ↔ (∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹) ∧ ∀𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)∀𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → 𝑓 = 𝑔))) |
108 | 86, 104, 107 | sylanbrc 586 |
1
⊢ (𝜑 → ∃!𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹)) |