| Step | Hyp | Ref
| Expression |
| 1 | | ccatws1cl 14654 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ++ 〈“𝐵”〉) ∈ Word 𝑋) |
| 2 | | wrdf 14557 |
. . . . 5
⊢ ((𝐴 ++ 〈“𝐵”〉) ∈ Word 𝑋 → (𝐴 ++ 〈“𝐵”〉):(0..^(♯‘(𝐴 ++ 〈“𝐵”〉)))⟶𝑋) |
| 3 | 1, 2 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ++ 〈“𝐵”〉):(0..^(♯‘(𝐴 ++ 〈“𝐵”〉)))⟶𝑋) |
| 4 | | ccatws1len 14658 |
. . . . . . . 8
⊢ (𝐴 ∈ Word 𝑋 → (♯‘(𝐴 ++ 〈“𝐵”〉)) = ((♯‘𝐴) + 1)) |
| 5 | 4 | oveq2d 7447 |
. . . . . . 7
⊢ (𝐴 ∈ Word 𝑋 → (0..^(♯‘(𝐴 ++ 〈“𝐵”〉))) =
(0..^((♯‘𝐴) +
1))) |
| 6 | | lencl 14571 |
. . . . . . . . 9
⊢ (𝐴 ∈ Word 𝑋 → (♯‘𝐴) ∈
ℕ0) |
| 7 | | nn0uz 12920 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
| 8 | 6, 7 | eleqtrdi 2851 |
. . . . . . . 8
⊢ (𝐴 ∈ Word 𝑋 → (♯‘𝐴) ∈
(ℤ≥‘0)) |
| 9 | | fzosplitsn 13814 |
. . . . . . . 8
⊢
((♯‘𝐴)
∈ (ℤ≥‘0) → (0..^((♯‘𝐴) + 1)) =
((0..^(♯‘𝐴))
∪ {(♯‘𝐴)})) |
| 10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ Word 𝑋 → (0..^((♯‘𝐴) + 1)) =
((0..^(♯‘𝐴))
∪ {(♯‘𝐴)})) |
| 11 | 5, 10 | eqtrd 2777 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑋 → (0..^(♯‘(𝐴 ++ 〈“𝐵”〉))) =
((0..^(♯‘𝐴))
∪ {(♯‘𝐴)})) |
| 12 | 11 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (0..^(♯‘(𝐴 ++ 〈“𝐵”〉))) =
((0..^(♯‘𝐴))
∪ {(♯‘𝐴)})) |
| 13 | 12 | feq2d 6722 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 ++ 〈“𝐵”〉):(0..^(♯‘(𝐴 ++ 〈“𝐵”〉)))⟶𝑋 ↔ (𝐴 ++ 〈“𝐵”〉):((0..^(♯‘𝐴)) ∪ {(♯‘𝐴)})⟶𝑋)) |
| 14 | 3, 13 | mpbid 232 |
. . 3
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ++ 〈“𝐵”〉):((0..^(♯‘𝐴)) ∪ {(♯‘𝐴)})⟶𝑋) |
| 15 | 14 | ffnd 6737 |
. 2
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ++ 〈“𝐵”〉) Fn ((0..^(♯‘𝐴)) ∪ {(♯‘𝐴)})) |
| 16 | | wrdf 14557 |
. . . . 5
⊢ (𝐴 ∈ Word 𝑋 → 𝐴:(0..^(♯‘𝐴))⟶𝑋) |
| 17 | 16 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐴:(0..^(♯‘𝐴))⟶𝑋) |
| 18 | | eqid 2737 |
. . . . . 6
⊢
{〈(♯‘𝐴), 𝐵〉} = {〈(♯‘𝐴), 𝐵〉} |
| 19 | | fsng 7157 |
. . . . . 6
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ 𝐵 ∈ 𝑋) → ({〈(♯‘𝐴), 𝐵〉}:{(♯‘𝐴)}⟶{𝐵} ↔ {〈(♯‘𝐴), 𝐵〉} = {〈(♯‘𝐴), 𝐵〉})) |
| 20 | 18, 19 | mpbiri 258 |
. . . . 5
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ 𝐵 ∈ 𝑋) → {〈(♯‘𝐴), 𝐵〉}:{(♯‘𝐴)}⟶{𝐵}) |
| 21 | 6, 20 | sylan 580 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → {〈(♯‘𝐴), 𝐵〉}:{(♯‘𝐴)}⟶{𝐵}) |
| 22 | | fzodisjsn 13737 |
. . . . 5
⊢
((0..^(♯‘𝐴)) ∩ {(♯‘𝐴)}) = ∅ |
| 23 | 22 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((0..^(♯‘𝐴)) ∩ {(♯‘𝐴)}) = ∅) |
| 24 | | fun 6770 |
. . . 4
⊢ (((𝐴:(0..^(♯‘𝐴))⟶𝑋 ∧ {〈(♯‘𝐴), 𝐵〉}:{(♯‘𝐴)}⟶{𝐵}) ∧ ((0..^(♯‘𝐴)) ∩ {(♯‘𝐴)}) = ∅) → (𝐴 ∪
{〈(♯‘𝐴),
𝐵〉}):((0..^(♯‘𝐴)) ∪ {(♯‘𝐴)})⟶(𝑋 ∪ {𝐵})) |
| 25 | 17, 21, 23, 24 | syl21anc 838 |
. . 3
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∪ {〈(♯‘𝐴), 𝐵〉}):((0..^(♯‘𝐴)) ∪ {(♯‘𝐴)})⟶(𝑋 ∪ {𝐵})) |
| 26 | 25 | ffnd 6737 |
. 2
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∪ {〈(♯‘𝐴), 𝐵〉}) Fn ((0..^(♯‘𝐴)) ∪ {(♯‘𝐴)})) |
| 27 | | elun 4153 |
. . 3
⊢ (𝑥 ∈
((0..^(♯‘𝐴))
∪ {(♯‘𝐴)})
↔ (𝑥 ∈
(0..^(♯‘𝐴))
∨ 𝑥 ∈
{(♯‘𝐴)})) |
| 28 | | ccats1val1 14664 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝑥 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = (𝐴‘𝑥)) |
| 29 | 28 | adantlr 715 |
. . . . 5
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = (𝐴‘𝑥)) |
| 30 | | simpr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ (0..^(♯‘𝐴))) → 𝑥 ∈ (0..^(♯‘𝐴))) |
| 31 | | fzonel 13713 |
. . . . . . . 8
⊢ ¬
(♯‘𝐴) ∈
(0..^(♯‘𝐴)) |
| 32 | | nelne2 3040 |
. . . . . . . 8
⊢ ((𝑥 ∈
(0..^(♯‘𝐴))
∧ ¬ (♯‘𝐴) ∈ (0..^(♯‘𝐴))) → 𝑥 ≠ (♯‘𝐴)) |
| 33 | 30, 31, 32 | sylancl 586 |
. . . . . . 7
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ (0..^(♯‘𝐴))) → 𝑥 ≠ (♯‘𝐴)) |
| 34 | 33 | necomd 2996 |
. . . . . 6
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ (0..^(♯‘𝐴))) → (♯‘𝐴) ≠ 𝑥) |
| 35 | | fvunsn 7199 |
. . . . . 6
⊢
((♯‘𝐴)
≠ 𝑥 → ((𝐴 ∪
{〈(♯‘𝐴),
𝐵〉})‘𝑥) = (𝐴‘𝑥)) |
| 36 | 34, 35 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ (0..^(♯‘𝐴))) → ((𝐴 ∪ {〈(♯‘𝐴), 𝐵〉})‘𝑥) = (𝐴‘𝑥)) |
| 37 | 29, 36 | eqtr4d 2780 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = ((𝐴 ∪ {〈(♯‘𝐴), 𝐵〉})‘𝑥)) |
| 38 | | fvexd 6921 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (♯‘𝐴) ∈ V) |
| 39 | | simpr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐵 ∈ 𝑋) |
| 40 | 17 | fdmd 6746 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → dom 𝐴 = (0..^(♯‘𝐴))) |
| 41 | 40 | eleq2d 2827 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((♯‘𝐴) ∈ dom 𝐴 ↔ (♯‘𝐴) ∈ (0..^(♯‘𝐴)))) |
| 42 | 31, 41 | mtbiri 327 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ¬ (♯‘𝐴) ∈ dom 𝐴) |
| 43 | | fsnunfv 7207 |
. . . . . . . 8
⊢
(((♯‘𝐴)
∈ V ∧ 𝐵 ∈
𝑋 ∧ ¬
(♯‘𝐴) ∈
dom 𝐴) → ((𝐴 ∪
{〈(♯‘𝐴),
𝐵〉})‘(♯‘𝐴)) = 𝐵) |
| 44 | 38, 39, 42, 43 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 ∪ {〈(♯‘𝐴), 𝐵〉})‘(♯‘𝐴)) = 𝐵) |
| 45 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐴 ∈ Word 𝑋) |
| 46 | | s1cl 14640 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑋 → 〈“𝐵”〉 ∈ Word 𝑋) |
| 47 | 46 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → 〈“𝐵”〉 ∈ Word 𝑋) |
| 48 | | s1len 14644 |
. . . . . . . . . . . 12
⊢
(♯‘〈“𝐵”〉) = 1 |
| 49 | | 1nn 12277 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
| 50 | 48, 49 | eqeltri 2837 |
. . . . . . . . . . 11
⊢
(♯‘〈“𝐵”〉) ∈
ℕ |
| 51 | | lbfzo0 13739 |
. . . . . . . . . . 11
⊢ (0 ∈
(0..^(♯‘〈“𝐵”〉)) ↔
(♯‘〈“𝐵”〉) ∈
ℕ) |
| 52 | 50, 51 | mpbir 231 |
. . . . . . . . . 10
⊢ 0 ∈
(0..^(♯‘〈“𝐵”〉)) |
| 53 | 52 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ∈
(0..^(♯‘〈“𝐵”〉))) |
| 54 | | ccatval3 14617 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑋 ∧ 〈“𝐵”〉 ∈ Word 𝑋 ∧ 0 ∈
(0..^(♯‘〈“𝐵”〉))) → ((𝐴 ++ 〈“𝐵”〉)‘(0 +
(♯‘𝐴))) =
(〈“𝐵”〉‘0)) |
| 55 | 45, 47, 53, 54 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 ++ 〈“𝐵”〉)‘(0 +
(♯‘𝐴))) =
(〈“𝐵”〉‘0)) |
| 56 | | s1fv 14648 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑋 → (〈“𝐵”〉‘0) = 𝐵) |
| 57 | 56 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (〈“𝐵”〉‘0) = 𝐵) |
| 58 | 55, 57 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 ++ 〈“𝐵”〉)‘(0 +
(♯‘𝐴))) = 𝐵) |
| 59 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (♯‘𝐴) ∈
ℕ0) |
| 60 | 59 | nn0cnd 12589 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (♯‘𝐴) ∈ ℂ) |
| 61 | 60 | addlidd 11462 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (0 + (♯‘𝐴)) = (♯‘𝐴)) |
| 62 | 61 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 ++ 〈“𝐵”〉)‘(0 +
(♯‘𝐴))) =
((𝐴 ++ 〈“𝐵”〉)‘(♯‘𝐴))) |
| 63 | 44, 58, 62 | 3eqtr2rd 2784 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 ++ 〈“𝐵”〉)‘(♯‘𝐴)) = ((𝐴 ∪ {〈(♯‘𝐴), 𝐵〉})‘(♯‘𝐴))) |
| 64 | | elsni 4643 |
. . . . . . . 8
⊢ (𝑥 ∈ {(♯‘𝐴)} → 𝑥 = (♯‘𝐴)) |
| 65 | 64 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑥 ∈ {(♯‘𝐴)} → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = ((𝐴 ++ 〈“𝐵”〉)‘(♯‘𝐴))) |
| 66 | 64 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑥 ∈ {(♯‘𝐴)} → ((𝐴 ∪ {〈(♯‘𝐴), 𝐵〉})‘𝑥) = ((𝐴 ∪ {〈(♯‘𝐴), 𝐵〉})‘(♯‘𝐴))) |
| 67 | 65, 66 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑥 ∈ {(♯‘𝐴)} → (((𝐴 ++ 〈“𝐵”〉)‘𝑥) = ((𝐴 ∪ {〈(♯‘𝐴), 𝐵〉})‘𝑥) ↔ ((𝐴 ++ 〈“𝐵”〉)‘(♯‘𝐴)) = ((𝐴 ∪ {〈(♯‘𝐴), 𝐵〉})‘(♯‘𝐴)))) |
| 68 | 63, 67 | syl5ibrcom 247 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑥 ∈ {(♯‘𝐴)} → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = ((𝐴 ∪ {〈(♯‘𝐴), 𝐵〉})‘𝑥))) |
| 69 | 68 | imp 406 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ {(♯‘𝐴)}) → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = ((𝐴 ∪ {〈(♯‘𝐴), 𝐵〉})‘𝑥)) |
| 70 | 37, 69 | jaodan 960 |
. . 3
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑥 ∈ (0..^(♯‘𝐴)) ∨ 𝑥 ∈ {(♯‘𝐴)})) → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = ((𝐴 ∪ {〈(♯‘𝐴), 𝐵〉})‘𝑥)) |
| 71 | 27, 70 | sylan2b 594 |
. 2
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ ((0..^(♯‘𝐴)) ∪ {(♯‘𝐴)})) → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = ((𝐴 ∪ {〈(♯‘𝐴), 𝐵〉})‘𝑥)) |
| 72 | 15, 26, 71 | eqfnfvd 7054 |
1
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ++ 〈“𝐵”〉) = (𝐴 ∪ {〈(♯‘𝐴), 𝐵〉})) |