Step | Hyp | Ref
| Expression |
1 | | qtopeu.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) |
2 | | fofn 6333 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹 Fn 𝑋) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 Fn 𝑋) |
4 | 3 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐹 Fn 𝑋) |
5 | | fniniseg 6564 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝑋 → (𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) ↔ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) ↔ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) |
7 | | eqcom 2806 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = (𝐹‘𝑥)) |
8 | 7 | 3anbi3i 1199 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥))) |
9 | | 3anass 1117 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) |
10 | 8, 9 | bitri 267 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) |
11 | | qtopeu.5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐺‘𝑥) = (𝐺‘𝑦)) |
12 | 10, 11 | sylan2br 589 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) → (𝐺‘𝑥) = (𝐺‘𝑦)) |
13 | 12 | eqcomd 2805 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) → (𝐺‘𝑦) = (𝐺‘𝑥)) |
14 | 13 | expr 449 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)) → (𝐺‘𝑦) = (𝐺‘𝑥))) |
15 | 6, 14 | sylbid 232 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) → (𝐺‘𝑦) = (𝐺‘𝑥))) |
16 | 15 | ralrimiv 3146 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)})(𝐺‘𝑦) = (𝐺‘𝑥)) |
17 | | qtopeu.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
18 | | qtopeu.4 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) |
19 | | cntop2 21374 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ Top) |
21 | | eqid 2799 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝐾 =
∪ 𝐾 |
22 | 21 | toptopon 21050 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
23 | 20, 22 | sylib 210 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
24 | | cnf2 21382 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐺 ∈ (𝐽 Cn 𝐾)) → 𝐺:𝑋⟶∪ 𝐾) |
25 | 17, 23, 18, 24 | syl3anc 1491 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:𝑋⟶∪ 𝐾) |
26 | 25 | ffnd 6257 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 Fn 𝑋) |
27 | 26 | adantr 473 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐺 Fn 𝑋) |
28 | | cnvimass 5702 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 “ {(𝐹‘𝑥)}) ⊆ dom 𝐹 |
29 | | fof 6331 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
30 | 1, 29 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) |
31 | 30 | fdmd 6265 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝐹 = 𝑋) |
32 | 31 | adantr 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → dom 𝐹 = 𝑋) |
33 | 28, 32 | syl5sseq 3849 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (◡𝐹 “ {(𝐹‘𝑥)}) ⊆ 𝑋) |
34 | | eqeq1 2803 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐺‘𝑦) → (𝑤 = (𝐺‘𝑥) ↔ (𝐺‘𝑦) = (𝐺‘𝑥))) |
35 | 34 | ralima 6727 |
. . . . . . . . . . . 12
⊢ ((𝐺 Fn 𝑋 ∧ (◡𝐹 “ {(𝐹‘𝑥)}) ⊆ 𝑋) → (∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥) ↔ ∀𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)})(𝐺‘𝑦) = (𝐺‘𝑥))) |
36 | 27, 33, 35 | syl2anc 580 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥) ↔ ∀𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)})(𝐺‘𝑦) = (𝐺‘𝑥))) |
37 | 16, 36 | mpbird 249 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥)) |
38 | 25 | fdmd 6265 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝐺 = 𝑋) |
39 | 38 | eleq2d 2864 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ dom 𝐺 ↔ 𝑥 ∈ 𝑋)) |
40 | 39 | biimpar 470 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ dom 𝐺) |
41 | | simpr 478 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
42 | | eqidd 2800 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
43 | | fniniseg 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 Fn 𝑋 → (𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) ↔ (𝑥 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑥)))) |
44 | 4, 43 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) ↔ (𝑥 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑥)))) |
45 | 41, 42, 44 | mpbir2and 705 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑥)})) |
46 | | inelcm 4227 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑥)})) → (dom 𝐺 ∩ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅) |
47 | 40, 45, 46 | syl2anc 580 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (dom 𝐺 ∩ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅) |
48 | | imadisj 5701 |
. . . . . . . . . . . . 13
⊢ ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = ∅ ↔ (dom 𝐺 ∩ (◡𝐹 “ {(𝐹‘𝑥)})) = ∅) |
49 | 48 | necon3bii 3023 |
. . . . . . . . . . . 12
⊢ ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅ ↔ (dom 𝐺 ∩ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅) |
50 | 47, 49 | sylibr 226 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅) |
51 | | eqsn 4548 |
. . . . . . . . . . 11
⊢ ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅ → ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = {(𝐺‘𝑥)} ↔ ∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥))) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = {(𝐺‘𝑥)} ↔ ∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥))) |
53 | 37, 52 | mpbird 249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = {(𝐺‘𝑥)}) |
54 | 53 | unieqd 4638 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = ∪ {(𝐺‘𝑥)}) |
55 | | fvex 6424 |
. . . . . . . . 9
⊢ (𝐺‘𝑥) ∈ V |
56 | 55 | unisn 4644 |
. . . . . . . 8
⊢ ∪ {(𝐺‘𝑥)} = (𝐺‘𝑥) |
57 | 54, 56 | syl6req 2850 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) = ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))) |
58 | 57 | mpteq2dva 4937 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥)) = (𝑥 ∈ 𝑋 ↦ ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})))) |
59 | 25 | feqmptd 6474 |
. . . . . 6
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) |
60 | 30 | ffvelrnda 6585 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ 𝑌) |
61 | 30 | feqmptd 6474 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
62 | | eqidd 2800 |
. . . . . . 7
⊢ (𝜑 → (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) = (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤})))) |
63 | | sneq 4378 |
. . . . . . . . . 10
⊢ (𝑤 = (𝐹‘𝑥) → {𝑤} = {(𝐹‘𝑥)}) |
64 | 63 | imaeq2d 5683 |
. . . . . . . . 9
⊢ (𝑤 = (𝐹‘𝑥) → (◡𝐹 “ {𝑤}) = (◡𝐹 “ {(𝐹‘𝑥)})) |
65 | 64 | imaeq2d 5683 |
. . . . . . . 8
⊢ (𝑤 = (𝐹‘𝑥) → (𝐺 “ (◡𝐹 “ {𝑤})) = (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))) |
66 | 65 | unieqd 4638 |
. . . . . . 7
⊢ (𝑤 = (𝐹‘𝑥) → ∪ (𝐺 “ (◡𝐹 “ {𝑤})) = ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))) |
67 | 60, 61, 62, 66 | fmptco 6623 |
. . . . . 6
⊢ (𝜑 → ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹) = (𝑥 ∈ 𝑋 ↦ ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})))) |
68 | 58, 59, 67 | 3eqtr4d 2843 |
. . . . 5
⊢ (𝜑 → 𝐺 = ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹)) |
69 | 68, 18 | eqeltrrd 2879 |
. . . 4
⊢ (𝜑 → ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹) ∈ (𝐽 Cn 𝐾)) |
70 | 25 | ffvelrnda 6585 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) ∈ ∪ 𝐾) |
71 | 57, 70 | eqeltrrd 2879 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾) |
72 | 71 | ralrimiva 3147 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾) |
73 | 66 | eqcomd 2805 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝐹‘𝑥) → ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) |
74 | 73 | eqcoms 2807 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) = 𝑤 → ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) |
75 | 74 | eleq1d 2863 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) = 𝑤 → (∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾 ↔ ∪ (𝐺
“ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾)) |
76 | 75 | cbvfo 6772 |
. . . . . . . 8
⊢ (𝐹:𝑋–onto→𝑌 → (∀𝑥 ∈ 𝑋 ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾 ↔ ∀𝑤 ∈ 𝑌 ∪ (𝐺 “ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾)) |
77 | 1, 76 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾 ↔ ∀𝑤 ∈ 𝑌 ∪ (𝐺 “ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾)) |
78 | 72, 77 | mpbid 224 |
. . . . . 6
⊢ (𝜑 → ∀𝑤 ∈ 𝑌 ∪ (𝐺 “ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾) |
79 | | eqid 2799 |
. . . . . . 7
⊢ (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) = (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) |
80 | 79 | fmpt 6606 |
. . . . . 6
⊢
(∀𝑤 ∈
𝑌 ∪ (𝐺
“ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾 ↔ (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))):𝑌⟶∪ 𝐾) |
81 | 78, 80 | sylib 210 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))):𝑌⟶∪ 𝐾) |
82 | | qtopcn 21846 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾))
∧ (𝐹:𝑋–onto→𝑌 ∧ (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))):𝑌⟶∪ 𝐾)) → ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹) ∈ (𝐽 Cn 𝐾))) |
83 | 17, 23, 1, 81, 82 | syl22anc 868 |
. . . 4
⊢ (𝜑 → ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹) ∈ (𝐽 Cn 𝐾))) |
84 | 69, 83 | mpbird 249 |
. . 3
⊢ (𝜑 → (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) |
85 | | coeq1 5483 |
. . . 4
⊢ (𝑓 = (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) → (𝑓 ∘ 𝐹) = ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹)) |
86 | 85 | rspceeqv 3515 |
. . 3
⊢ (((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝐺 = ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹)) → ∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹)) |
87 | 84, 68, 86 | syl2anc 580 |
. 2
⊢ (𝜑 → ∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹)) |
88 | | eqtr2 2819 |
. . . 4
⊢ ((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → (𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹)) |
89 | 1 | adantr 473 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝐹:𝑋–onto→𝑌) |
90 | | qtoptopon 21836 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
91 | 17, 1, 90 | syl2anc 580 |
. . . . . . . 8
⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
92 | 91 | adantr 473 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
93 | 23 | adantr 473 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
94 | | simprl 788 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) |
95 | | cnf2 21382 |
. . . . . . 7
⊢ (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) → 𝑓:𝑌⟶∪ 𝐾) |
96 | 92, 93, 94, 95 | syl3anc 1491 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑓:𝑌⟶∪ 𝐾) |
97 | 96 | ffnd 6257 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑓 Fn 𝑌) |
98 | | simprr 790 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) |
99 | | cnf2 21382 |
. . . . . . 7
⊢ (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) → 𝑔:𝑌⟶∪ 𝐾) |
100 | 92, 93, 98, 99 | syl3anc 1491 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑔:𝑌⟶∪ 𝐾) |
101 | 100 | ffnd 6257 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑔 Fn 𝑌) |
102 | | cocan2 6775 |
. . . . 5
⊢ ((𝐹:𝑋–onto→𝑌 ∧ 𝑓 Fn 𝑌 ∧ 𝑔 Fn 𝑌) → ((𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹) ↔ 𝑓 = 𝑔)) |
103 | 89, 97, 101, 102 | syl3anc 1491 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → ((𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹) ↔ 𝑓 = 𝑔)) |
104 | 88, 103 | syl5ib 236 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → ((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → 𝑓 = 𝑔)) |
105 | 104 | ralrimivva 3152 |
. 2
⊢ (𝜑 → ∀𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)∀𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → 𝑓 = 𝑔)) |
106 | | coeq1 5483 |
. . . 4
⊢ (𝑓 = 𝑔 → (𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹)) |
107 | 106 | eqeq2d 2809 |
. . 3
⊢ (𝑓 = 𝑔 → (𝐺 = (𝑓 ∘ 𝐹) ↔ 𝐺 = (𝑔 ∘ 𝐹))) |
108 | 107 | reu4 3596 |
. 2
⊢
(∃!𝑓 ∈
((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹) ↔ (∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹) ∧ ∀𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)∀𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → 𝑓 = 𝑔))) |
109 | 87, 105, 108 | sylanbrc 579 |
1
⊢ (𝜑 → ∃!𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹)) |