Step | Hyp | Ref
| Expression |
1 | | qtopeu.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) |
2 | | fofn 6030 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹 Fn 𝑋) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 Fn 𝑋) |
4 | 3 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐹 Fn 𝑋) |
5 | | fniniseg 6246 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝑋 → (𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) ↔ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) ↔ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) |
7 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = (𝐹‘𝑥)) |
8 | 7 | 3anbi3i 1248 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥))) |
9 | | 3anass 1035 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) |
10 | 8, 9 | bitri 263 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) |
11 | | qtopeu.5 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐺‘𝑥) = (𝐺‘𝑦)) |
12 | 10, 11 | sylan2br 492 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) → (𝐺‘𝑥) = (𝐺‘𝑦)) |
13 | 12 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)))) → (𝐺‘𝑦) = (𝐺‘𝑥)) |
14 | 13 | expr 641 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = (𝐹‘𝑥)) → (𝐺‘𝑦) = (𝐺‘𝑥))) |
15 | 6, 14 | sylbid 229 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) → (𝐺‘𝑦) = (𝐺‘𝑥))) |
16 | 15 | ralrimiv 2948 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)})(𝐺‘𝑦) = (𝐺‘𝑥)) |
17 | | qtopeu.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
18 | | qtopeu.4 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) |
19 | | cntop2 20855 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ Top) |
21 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝐾 =
∪ 𝐾 |
22 | 21 | toptopon 20548 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
23 | 20, 22 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
24 | | cnf2 20863 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐺 ∈ (𝐽 Cn 𝐾)) → 𝐺:𝑋⟶∪ 𝐾) |
25 | 17, 23, 18, 24 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:𝑋⟶∪ 𝐾) |
26 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ (𝐺:𝑋⟶∪ 𝐾 → 𝐺 Fn 𝑋) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 Fn 𝑋) |
28 | 27 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐺 Fn 𝑋) |
29 | | cnvimass 5404 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 “ {(𝐹‘𝑥)}) ⊆ dom 𝐹 |
30 | | fof 6028 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
31 | 1, 30 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) |
32 | | fdm 5964 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝐹 = 𝑋) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → dom 𝐹 = 𝑋) |
35 | 29, 34 | syl5sseq 3616 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (◡𝐹 “ {(𝐹‘𝑥)}) ⊆ 𝑋) |
36 | | eqeq1 2614 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐺‘𝑦) → (𝑤 = (𝐺‘𝑥) ↔ (𝐺‘𝑦) = (𝐺‘𝑥))) |
37 | 36 | ralima 6402 |
. . . . . . . . . . . 12
⊢ ((𝐺 Fn 𝑋 ∧ (◡𝐹 “ {(𝐹‘𝑥)}) ⊆ 𝑋) → (∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥) ↔ ∀𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)})(𝐺‘𝑦) = (𝐺‘𝑥))) |
38 | 28, 35, 37 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥) ↔ ∀𝑦 ∈ (◡𝐹 “ {(𝐹‘𝑥)})(𝐺‘𝑦) = (𝐺‘𝑥))) |
39 | 16, 38 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥)) |
40 | | fdm 5964 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:𝑋⟶∪ 𝐾 → dom 𝐺 = 𝑋) |
41 | 25, 40 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝐺 = 𝑋) |
42 | 41 | eleq2d 2673 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ dom 𝐺 ↔ 𝑥 ∈ 𝑋)) |
43 | 42 | biimpar 501 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ dom 𝐺) |
44 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
45 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
46 | | fniniseg 6246 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 Fn 𝑋 → (𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) ↔ (𝑥 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑥)))) |
47 | 4, 46 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑥)}) ↔ (𝑥 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑥)))) |
48 | 44, 45, 47 | mpbir2and 959 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑥)})) |
49 | | inelcm 3984 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ (◡𝐹 “ {(𝐹‘𝑥)})) → (dom 𝐺 ∩ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅) |
50 | 43, 48, 49 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (dom 𝐺 ∩ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅) |
51 | | imadisj 5403 |
. . . . . . . . . . . . 13
⊢ ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = ∅ ↔ (dom 𝐺 ∩ (◡𝐹 “ {(𝐹‘𝑥)})) = ∅) |
52 | 51 | necon3bii 2834 |
. . . . . . . . . . . 12
⊢ ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅ ↔ (dom 𝐺 ∩ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅) |
53 | 50, 52 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅) |
54 | | eqsn 4301 |
. . . . . . . . . . 11
⊢ ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ≠ ∅ → ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = {(𝐺‘𝑥)} ↔ ∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥))) |
55 | 53, 54 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = {(𝐺‘𝑥)} ↔ ∀𝑤 ∈ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))𝑤 = (𝐺‘𝑥))) |
56 | 39, 55 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = {(𝐺‘𝑥)}) |
57 | 56 | unieqd 4382 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = ∪ {(𝐺‘𝑥)}) |
58 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝐺‘𝑥) ∈ V |
59 | 58 | unisn 4387 |
. . . . . . . 8
⊢ ∪ {(𝐺‘𝑥)} = (𝐺‘𝑥) |
60 | 57, 59 | syl6req 2661 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) = ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))) |
61 | 60 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥)) = (𝑥 ∈ 𝑋 ↦ ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})))) |
62 | 25 | feqmptd 6159 |
. . . . . 6
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝑋 ↦ (𝐺‘𝑥))) |
63 | 31 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ 𝑌) |
64 | 31 | feqmptd 6159 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥))) |
65 | | eqidd 2611 |
. . . . . . 7
⊢ (𝜑 → (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) = (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤})))) |
66 | | sneq 4135 |
. . . . . . . . . 10
⊢ (𝑤 = (𝐹‘𝑥) → {𝑤} = {(𝐹‘𝑥)}) |
67 | 66 | imaeq2d 5385 |
. . . . . . . . 9
⊢ (𝑤 = (𝐹‘𝑥) → (◡𝐹 “ {𝑤}) = (◡𝐹 “ {(𝐹‘𝑥)})) |
68 | 67 | imaeq2d 5385 |
. . . . . . . 8
⊢ (𝑤 = (𝐹‘𝑥) → (𝐺 “ (◡𝐹 “ {𝑤})) = (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))) |
69 | 68 | unieqd 4382 |
. . . . . . 7
⊢ (𝑤 = (𝐹‘𝑥) → ∪ (𝐺 “ (◡𝐹 “ {𝑤})) = ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)}))) |
70 | 63, 64, 65, 69 | fmptco 6303 |
. . . . . 6
⊢ (𝜑 → ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹) = (𝑥 ∈ 𝑋 ↦ ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})))) |
71 | 61, 62, 70 | 3eqtr4d 2654 |
. . . . 5
⊢ (𝜑 → 𝐺 = ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹)) |
72 | 71, 18 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹) ∈ (𝐽 Cn 𝐾)) |
73 | 25 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐺‘𝑥) ∈ ∪ 𝐾) |
74 | 60, 73 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾) |
75 | 74 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾) |
76 | 69 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝐹‘𝑥) → ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) |
77 | 76 | eqcoms 2618 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) = 𝑤 → ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) = ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) |
78 | 77 | eleq1d 2672 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) = 𝑤 → (∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾 ↔ ∪ (𝐺
“ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾)) |
79 | 78 | cbvfo 6444 |
. . . . . . . 8
⊢ (𝐹:𝑋–onto→𝑌 → (∀𝑥 ∈ 𝑋 ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾 ↔ ∀𝑤 ∈ 𝑌 ∪ (𝐺 “ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾)) |
80 | 1, 79 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∪ (𝐺 “ (◡𝐹 “ {(𝐹‘𝑥)})) ∈ ∪
𝐾 ↔ ∀𝑤 ∈ 𝑌 ∪ (𝐺 “ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾)) |
81 | 75, 80 | mpbid 221 |
. . . . . 6
⊢ (𝜑 → ∀𝑤 ∈ 𝑌 ∪ (𝐺 “ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾) |
82 | | eqid 2610 |
. . . . . . 7
⊢ (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) = (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) |
83 | 82 | fmpt 6289 |
. . . . . 6
⊢
(∀𝑤 ∈
𝑌 ∪ (𝐺
“ (◡𝐹 “ {𝑤})) ∈ ∪ 𝐾 ↔ (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))):𝑌⟶∪ 𝐾) |
84 | 81, 83 | sylib 207 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))):𝑌⟶∪ 𝐾) |
85 | | qtopcn 21327 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾))
∧ (𝐹:𝑋–onto→𝑌 ∧ (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))):𝑌⟶∪ 𝐾)) → ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹) ∈ (𝐽 Cn 𝐾))) |
86 | 17, 23, 1, 84, 85 | syl22anc 1319 |
. . . 4
⊢ (𝜑 → ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹) ∈ (𝐽 Cn 𝐾))) |
87 | 72, 86 | mpbird 246 |
. . 3
⊢ (𝜑 → (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) |
88 | | coeq1 5201 |
. . . . 5
⊢ (𝑓 = (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) → (𝑓 ∘ 𝐹) = ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹)) |
89 | 88 | eqeq2d 2620 |
. . . 4
⊢ (𝑓 = (𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) → (𝐺 = (𝑓 ∘ 𝐹) ↔ 𝐺 = ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹))) |
90 | 89 | rspcev 3282 |
. . 3
⊢ (((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝐺 = ((𝑤 ∈ 𝑌 ↦ ∪ (𝐺 “ (◡𝐹 “ {𝑤}))) ∘ 𝐹)) → ∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹)) |
91 | 87, 71, 90 | syl2anc 691 |
. 2
⊢ (𝜑 → ∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹)) |
92 | | eqtr2 2630 |
. . . 4
⊢ ((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → (𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹)) |
93 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝐹:𝑋–onto→𝑌) |
94 | | qtoptopon 21317 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
95 | 17, 1, 94 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
96 | 95 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
97 | 23 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
98 | | simprl 790 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) |
99 | | cnf2 20863 |
. . . . . . 7
⊢ (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) → 𝑓:𝑌⟶∪ 𝐾) |
100 | 96, 97, 98, 99 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑓:𝑌⟶∪ 𝐾) |
101 | | ffn 5958 |
. . . . . 6
⊢ (𝑓:𝑌⟶∪ 𝐾 → 𝑓 Fn 𝑌) |
102 | 100, 101 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑓 Fn 𝑌) |
103 | | simprr 792 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) |
104 | | cnf2 20863 |
. . . . . . 7
⊢ (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)) → 𝑔:𝑌⟶∪ 𝐾) |
105 | 96, 97, 103, 104 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑔:𝑌⟶∪ 𝐾) |
106 | | ffn 5958 |
. . . . . 6
⊢ (𝑔:𝑌⟶∪ 𝐾 → 𝑔 Fn 𝑌) |
107 | 105, 106 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → 𝑔 Fn 𝑌) |
108 | | cocan2 6447 |
. . . . 5
⊢ ((𝐹:𝑋–onto→𝑌 ∧ 𝑓 Fn 𝑌 ∧ 𝑔 Fn 𝑌) → ((𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹) ↔ 𝑓 = 𝑔)) |
109 | 93, 102, 107, 108 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → ((𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹) ↔ 𝑓 = 𝑔)) |
110 | 92, 109 | syl5ib 233 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾))) → ((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → 𝑓 = 𝑔)) |
111 | 110 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)∀𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → 𝑓 = 𝑔)) |
112 | | coeq1 5201 |
. . . 4
⊢ (𝑓 = 𝑔 → (𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹)) |
113 | 112 | eqeq2d 2620 |
. . 3
⊢ (𝑓 = 𝑔 → (𝐺 = (𝑓 ∘ 𝐹) ↔ 𝐺 = (𝑔 ∘ 𝐹))) |
114 | 113 | reu4 3367 |
. 2
⊢
(∃!𝑓 ∈
((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹) ↔ (∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹) ∧ ∀𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)∀𝑔 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → 𝑓 = 𝑔))) |
115 | 91, 111, 114 | sylanbrc 695 |
1
⊢ (𝜑 → ∃!𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹)) |