| Step | Hyp | Ref
| Expression |
| 1 | | cycpmco2.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
| 2 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ⊆ Word 𝐷 |
| 3 | | cycpmco2.w |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ dom 𝑀) |
| 4 | | cycpmco2.c |
. . . . . . . . . 10
⊢ 𝑀 = (toCyc‘𝐷) |
| 5 | | cycpmco2.s |
. . . . . . . . . 10
⊢ 𝑆 = (SymGrp‘𝐷) |
| 6 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 7 | 4, 5, 6 | tocycf 33137 |
. . . . . . . . 9
⊢ (𝐷 ∈ 𝑉 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) |
| 8 | 1, 7 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) |
| 9 | 8 | fdmd 6746 |
. . . . . . 7
⊢ (𝜑 → dom 𝑀 = {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
| 10 | 3, 9 | eleqtrd 2843 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
| 11 | 2, 10 | sselid 3981 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ Word 𝐷) |
| 12 | | pfxcl 14715 |
. . . . 5
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 prefix 𝐸) ∈ Word 𝐷) |
| 13 | 11, 12 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑊 prefix 𝐸) ∈ Word 𝐷) |
| 14 | | cycpmco2.i |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) |
| 15 | 14 | eldifad 3963 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ 𝐷) |
| 16 | 15 | s1cld 14641 |
. . . 4
⊢ (𝜑 → 〈“𝐼”〉 ∈ Word 𝐷) |
| 17 | | ccatcl 14612 |
. . . 4
⊢ (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷) → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) |
| 18 | 13, 16, 17 | syl2anc 584 |
. . 3
⊢ (𝜑 → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) |
| 19 | | swrdcl 14683 |
. . . 4
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) |
| 20 | 11, 19 | syl 17 |
. . 3
⊢ (𝜑 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) |
| 21 | | id 22 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) |
| 22 | | dmeq 5914 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊) |
| 23 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → 𝐷 = 𝐷) |
| 24 | 21, 22, 23 | f1eq123d 6840 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑊:dom 𝑊–1-1→𝐷)) |
| 25 | 24 | elrab 3692 |
. . . . . . 7
⊢ (𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) |
| 26 | 10, 25 | sylib 218 |
. . . . . 6
⊢ (𝜑 → (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) |
| 27 | 26 | simprd 495 |
. . . . 5
⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) |
| 28 | | cycpmco2.e |
. . . . . 6
⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) |
| 29 | | f1cnv 6872 |
. . . . . . . . . 10
⊢ (𝑊:dom 𝑊–1-1→𝐷 → ◡𝑊:ran 𝑊–1-1-onto→dom
𝑊) |
| 30 | | f1of 6848 |
. . . . . . . . . 10
⊢ (◡𝑊:ran 𝑊–1-1-onto→dom
𝑊 → ◡𝑊:ran 𝑊⟶dom 𝑊) |
| 31 | 27, 29, 30 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → ◡𝑊:ran 𝑊⟶dom 𝑊) |
| 32 | | cycpmco2.j |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ ran 𝑊) |
| 33 | 31, 32 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ dom 𝑊) |
| 34 | | wrddm 14559 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊))) |
| 35 | 11, 34 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊))) |
| 36 | 33, 35 | eleqtrd 2843 |
. . . . . . 7
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊))) |
| 37 | | fzofzp1 13803 |
. . . . . . 7
⊢ ((◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) |
| 38 | 36, 37 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) |
| 39 | 28, 38 | eqeltrid 2845 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ (0...(♯‘𝑊))) |
| 40 | 11, 27, 39 | pfxf1 32926 |
. . . 4
⊢ (𝜑 → (𝑊 prefix 𝐸):dom (𝑊 prefix 𝐸)–1-1→𝐷) |
| 41 | 15 | s1f1 32927 |
. . . 4
⊢ (𝜑 → 〈“𝐼”〉:dom
〈“𝐼”〉–1-1→𝐷) |
| 42 | | s1rn 14637 |
. . . . . . 7
⊢ (𝐼 ∈ 𝐷 → ran 〈“𝐼”〉 = {𝐼}) |
| 43 | 15, 42 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 〈“𝐼”〉 = {𝐼}) |
| 44 | 43 | ineq2d 4220 |
. . . . 5
⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∩ ran 〈“𝐼”〉) = (ran (𝑊 prefix 𝐸) ∩ {𝐼})) |
| 45 | | pfxrn2 32924 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐸) ⊆ ran 𝑊) |
| 46 | 11, 39, 45 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ran (𝑊 prefix 𝐸) ⊆ ran 𝑊) |
| 47 | 46 | ssrind 4244 |
. . . . . . 7
⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∩ {𝐼}) ⊆ (ran 𝑊 ∩ {𝐼})) |
| 48 | 14 | eldifbd 3964 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝐼 ∈ ran 𝑊) |
| 49 | | disjsn 4711 |
. . . . . . . 8
⊢ ((ran
𝑊 ∩ {𝐼}) = ∅ ↔ ¬ 𝐼 ∈ ran 𝑊) |
| 50 | 48, 49 | sylibr 234 |
. . . . . . 7
⊢ (𝜑 → (ran 𝑊 ∩ {𝐼}) = ∅) |
| 51 | 47, 50 | sseqtrd 4020 |
. . . . . 6
⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∩ {𝐼}) ⊆ ∅) |
| 52 | | ss0 4402 |
. . . . . 6
⊢ ((ran
(𝑊 prefix 𝐸) ∩ {𝐼}) ⊆ ∅ → (ran (𝑊 prefix 𝐸) ∩ {𝐼}) = ∅) |
| 53 | 51, 52 | syl 17 |
. . . . 5
⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∩ {𝐼}) = ∅) |
| 54 | 44, 53 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∩ ran 〈“𝐼”〉) = ∅) |
| 55 | 1, 13, 16, 40, 41, 54 | ccatf1 32933 |
. . 3
⊢ (𝜑 → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉):dom ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)–1-1→𝐷) |
| 56 | | lencl 14571 |
. . . . 5
⊢ (𝑊 ∈ Word 𝐷 → (♯‘𝑊) ∈
ℕ0) |
| 57 | | nn0fz0 13665 |
. . . . . 6
⊢
((♯‘𝑊)
∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
| 58 | 57 | biimpi 216 |
. . . . 5
⊢
((♯‘𝑊)
∈ ℕ0 → (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
| 59 | 11, 56, 58 | 3syl 18 |
. . . 4
⊢ (𝜑 → (♯‘𝑊) ∈
(0...(♯‘𝑊))) |
| 60 | 11, 39, 59, 27 | swrdf1 32941 |
. . 3
⊢ (𝜑 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉):dom (𝑊 substr 〈𝐸, (♯‘𝑊)〉)–1-1→𝐷) |
| 61 | | ccatrn 14627 |
. . . . . . 7
⊢ (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷) → ran ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) = (ran (𝑊 prefix 𝐸) ∪ ran 〈“𝐼”〉)) |
| 62 | 13, 16, 61 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ran ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) = (ran (𝑊 prefix 𝐸) ∪ ran 〈“𝐼”〉)) |
| 63 | 62 | ineq1d 4219 |
. . . . 5
⊢ (𝜑 → (ran ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = ((ran (𝑊 prefix 𝐸) ∪ ran 〈“𝐼”〉) ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
| 64 | | indir 4286 |
. . . . 5
⊢ ((ran
(𝑊 prefix 𝐸) ∪ ran 〈“𝐼”〉) ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = ((ran (𝑊 prefix 𝐸) ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉)) ∪ (ran 〈“𝐼”〉 ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
| 65 | 63, 64 | eqtrdi 2793 |
. . . 4
⊢ (𝜑 → (ran ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = ((ran (𝑊 prefix 𝐸) ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉)) ∪ (ran 〈“𝐼”〉 ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉)))) |
| 66 | | fz0ssnn0 13662 |
. . . . . . . . . 10
⊢
(0...(♯‘𝑊)) ⊆
ℕ0 |
| 67 | 66, 39 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈
ℕ0) |
| 68 | | pfxval 14711 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ℕ0) → (𝑊 prefix 𝐸) = (𝑊 substr 〈0, 𝐸〉)) |
| 69 | 11, 67, 68 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝑊 prefix 𝐸) = (𝑊 substr 〈0, 𝐸〉)) |
| 70 | 69 | rneqd 5949 |
. . . . . . 7
⊢ (𝜑 → ran (𝑊 prefix 𝐸) = ran (𝑊 substr 〈0, 𝐸〉)) |
| 71 | 70 | ineq1d 4219 |
. . . . . 6
⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = (ran (𝑊 substr 〈0, 𝐸〉) ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
| 72 | | 0elfz 13664 |
. . . . . . . 8
⊢ (𝐸 ∈ ℕ0
→ 0 ∈ (0...𝐸)) |
| 73 | 67, 72 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ (0...𝐸)) |
| 74 | | elfzuz3 13561 |
. . . . . . . 8
⊢ (𝐸 ∈
(0...(♯‘𝑊))
→ (♯‘𝑊)
∈ (ℤ≥‘𝐸)) |
| 75 | | eluzfz1 13571 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ (ℤ≥‘𝐸) → 𝐸 ∈ (𝐸...(♯‘𝑊))) |
| 76 | 39, 74, 75 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ (𝐸...(♯‘𝑊))) |
| 77 | | eluzfz2 13572 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ (ℤ≥‘𝐸) → (♯‘𝑊) ∈ (𝐸...(♯‘𝑊))) |
| 78 | 39, 74, 77 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑊) ∈ (𝐸...(♯‘𝑊))) |
| 79 | 11, 73, 39, 27, 76, 78 | swrdrndisj 32942 |
. . . . . 6
⊢ (𝜑 → (ran (𝑊 substr 〈0, 𝐸〉) ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = ∅) |
| 80 | 71, 79 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (ran (𝑊 prefix 𝐸) ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = ∅) |
| 81 | | incom 4209 |
. . . . . 6
⊢ (ran
〈“𝐼”〉
∩ ran (𝑊 substr
〈𝐸,
(♯‘𝑊)〉)) =
(ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∩ ran
〈“𝐼”〉) |
| 82 | 43 | ineq2d 4220 |
. . . . . . 7
⊢ (𝜑 → (ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∩ ran 〈“𝐼”〉) = (ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∩ {𝐼})) |
| 83 | | swrdrn2 32939 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈
(0...(♯‘𝑊)))
→ ran (𝑊 substr
〈𝐸,
(♯‘𝑊)〉)
⊆ ran 𝑊) |
| 84 | 11, 39, 59, 83 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ⊆ ran 𝑊) |
| 85 | 84 | ssrind 4244 |
. . . . . . . . 9
⊢ (𝜑 → (ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∩ {𝐼}) ⊆ (ran 𝑊 ∩ {𝐼})) |
| 86 | 85, 50 | sseqtrd 4020 |
. . . . . . . 8
⊢ (𝜑 → (ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∩ {𝐼}) ⊆ ∅) |
| 87 | | ss0 4402 |
. . . . . . . 8
⊢ ((ran
(𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∩ {𝐼}) ⊆ ∅ → (ran
(𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∩ {𝐼}) = ∅) |
| 88 | 86, 87 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∩ {𝐼}) = ∅) |
| 89 | 82, 88 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → (ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∩ ran 〈“𝐼”〉) =
∅) |
| 90 | 81, 89 | eqtrid 2789 |
. . . . 5
⊢ (𝜑 → (ran 〈“𝐼”〉 ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = ∅) |
| 91 | 80, 90 | uneq12d 4169 |
. . . 4
⊢ (𝜑 → ((ran (𝑊 prefix 𝐸) ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉)) ∪ (ran 〈“𝐼”〉 ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) = (∅ ∪
∅)) |
| 92 | | unidm 4157 |
. . . . 5
⊢ (∅
∪ ∅) = ∅ |
| 93 | 92 | a1i 11 |
. . . 4
⊢ (𝜑 → (∅ ∪ ∅) =
∅) |
| 94 | 65, 91, 93 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (ran ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∩ ran (𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = ∅) |
| 95 | 1, 18, 20, 55, 60, 94 | ccatf1 32933 |
. 2
⊢ (𝜑 → (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉)):dom (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))–1-1→𝐷) |
| 96 | | cycpmco2.1 |
. . . 4
⊢ 𝑈 = (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) |
| 97 | | ovexd 7466 |
. . . . . 6
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ V) |
| 98 | 28, 97 | eqeltrid 2845 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ V) |
| 99 | | splval 14789 |
. . . . 5
⊢ ((𝑊 ∈ dom 𝑀 ∧ (𝐸 ∈ V ∧ 𝐸 ∈ V ∧ 〈“𝐼”〉 ∈ Word 𝐷)) → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
| 100 | 3, 98, 98, 16, 99 | syl13anc 1374 |
. . . 4
⊢ (𝜑 → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
| 101 | 96, 100 | eqtrid 2789 |
. . 3
⊢ (𝜑 → 𝑈 = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
| 102 | 101 | dmeqd 5916 |
. . 3
⊢ (𝜑 → dom 𝑈 = dom (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
| 103 | | eqidd 2738 |
. . 3
⊢ (𝜑 → 𝐷 = 𝐷) |
| 104 | 101, 102,
103 | f1eq123d 6840 |
. 2
⊢ (𝜑 → (𝑈:dom 𝑈–1-1→𝐷 ↔ (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉)):dom (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))–1-1→𝐷)) |
| 105 | 95, 104 | mpbird 257 |
1
⊢ (𝜑 → 𝑈:dom 𝑈–1-1→𝐷) |