Step | Hyp | Ref
| Expression |
1 | | ccatws1cl 13249 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ++ 〈“𝐵”〉) ∈ Word 𝑋) |
2 | | wrdf 13165 |
. . . . 5
⊢ ((𝐴 ++ 〈“𝐵”〉) ∈ Word 𝑋 → (𝐴 ++ 〈“𝐵”〉):(0..^(#‘(𝐴 ++ 〈“𝐵”〉)))⟶𝑋) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ++ 〈“𝐵”〉):(0..^(#‘(𝐴 ++ 〈“𝐵”〉)))⟶𝑋) |
4 | | ccatws1len 13251 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (#‘(𝐴 ++ 〈“𝐵”〉)) = ((#‘𝐴) + 1)) |
5 | 4 | oveq2d 6565 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (0..^(#‘(𝐴 ++ 〈“𝐵”〉))) = (0..^((#‘𝐴) + 1))) |
6 | | lencl 13179 |
. . . . . . . . 9
⊢ (𝐴 ∈ Word 𝑋 → (#‘𝐴) ∈
ℕ0) |
7 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (#‘𝐴) ∈
ℕ0) |
8 | | nn0uz 11598 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
9 | 7, 8 | syl6eleq 2698 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (#‘𝐴) ∈
(ℤ≥‘0)) |
10 | | fzosplitsn 12442 |
. . . . . . 7
⊢
((#‘𝐴) ∈
(ℤ≥‘0) → (0..^((#‘𝐴) + 1)) = ((0..^(#‘𝐴)) ∪ {(#‘𝐴)})) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (0..^((#‘𝐴) + 1)) = ((0..^(#‘𝐴)) ∪ {(#‘𝐴)})) |
12 | 5, 11 | eqtrd 2644 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (0..^(#‘(𝐴 ++ 〈“𝐵”〉))) = ((0..^(#‘𝐴)) ∪ {(#‘𝐴)})) |
13 | 12 | feq2d 5944 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 ++ 〈“𝐵”〉):(0..^(#‘(𝐴 ++ 〈“𝐵”〉)))⟶𝑋 ↔ (𝐴 ++ 〈“𝐵”〉):((0..^(#‘𝐴)) ∪ {(#‘𝐴)})⟶𝑋)) |
14 | 3, 13 | mpbid 221 |
. . 3
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ++ 〈“𝐵”〉):((0..^(#‘𝐴)) ∪ {(#‘𝐴)})⟶𝑋) |
15 | | ffn 5958 |
. . 3
⊢ ((𝐴 ++ 〈“𝐵”〉):((0..^(#‘𝐴)) ∪ {(#‘𝐴)})⟶𝑋 → (𝐴 ++ 〈“𝐵”〉) Fn ((0..^(#‘𝐴)) ∪ {(#‘𝐴)})) |
16 | 14, 15 | syl 17 |
. 2
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ++ 〈“𝐵”〉) Fn ((0..^(#‘𝐴)) ∪ {(#‘𝐴)})) |
17 | | wrdf 13165 |
. . . . 5
⊢ (𝐴 ∈ Word 𝑋 → 𝐴:(0..^(#‘𝐴))⟶𝑋) |
18 | 17 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐴:(0..^(#‘𝐴))⟶𝑋) |
19 | | eqid 2610 |
. . . . . 6
⊢
{〈(#‘𝐴),
𝐵〉} =
{〈(#‘𝐴), 𝐵〉} |
20 | | fsng 6310 |
. . . . . 6
⊢
(((#‘𝐴) ∈
ℕ0 ∧ 𝐵
∈ 𝑋) →
({〈(#‘𝐴), 𝐵〉}:{(#‘𝐴)}⟶{𝐵} ↔ {〈(#‘𝐴), 𝐵〉} = {〈(#‘𝐴), 𝐵〉})) |
21 | 19, 20 | mpbiri 247 |
. . . . 5
⊢
(((#‘𝐴) ∈
ℕ0 ∧ 𝐵
∈ 𝑋) →
{〈(#‘𝐴), 𝐵〉}:{(#‘𝐴)}⟶{𝐵}) |
22 | 6, 21 | sylan 487 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → {〈(#‘𝐴), 𝐵〉}:{(#‘𝐴)}⟶{𝐵}) |
23 | | fzonel 12352 |
. . . . . 6
⊢ ¬
(#‘𝐴) ∈
(0..^(#‘𝐴)) |
24 | 23 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ¬ (#‘𝐴) ∈ (0..^(#‘𝐴))) |
25 | | disjsn 4192 |
. . . . 5
⊢
(((0..^(#‘𝐴))
∩ {(#‘𝐴)}) =
∅ ↔ ¬ (#‘𝐴) ∈ (0..^(#‘𝐴))) |
26 | 24, 25 | sylibr 223 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((0..^(#‘𝐴)) ∩ {(#‘𝐴)}) = ∅) |
27 | | fun 5979 |
. . . 4
⊢ (((𝐴:(0..^(#‘𝐴))⟶𝑋 ∧ {〈(#‘𝐴), 𝐵〉}:{(#‘𝐴)}⟶{𝐵}) ∧ ((0..^(#‘𝐴)) ∩ {(#‘𝐴)}) = ∅) → (𝐴 ∪ {〈(#‘𝐴), 𝐵〉}):((0..^(#‘𝐴)) ∪ {(#‘𝐴)})⟶(𝑋 ∪ {𝐵})) |
28 | 18, 22, 26, 27 | syl21anc 1317 |
. . 3
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∪ {〈(#‘𝐴), 𝐵〉}):((0..^(#‘𝐴)) ∪ {(#‘𝐴)})⟶(𝑋 ∪ {𝐵})) |
29 | | ffn 5958 |
. . 3
⊢ ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉}):((0..^(#‘𝐴)) ∪ {(#‘𝐴)})⟶(𝑋 ∪ {𝐵}) → (𝐴 ∪ {〈(#‘𝐴), 𝐵〉}) Fn ((0..^(#‘𝐴)) ∪ {(#‘𝐴)})) |
30 | 28, 29 | syl 17 |
. 2
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∪ {〈(#‘𝐴), 𝐵〉}) Fn ((0..^(#‘𝐴)) ∪ {(#‘𝐴)})) |
31 | | elun 3715 |
. . 3
⊢ (𝑥 ∈ ((0..^(#‘𝐴)) ∪ {(#‘𝐴)}) ↔ (𝑥 ∈ (0..^(#‘𝐴)) ∨ 𝑥 ∈ {(#‘𝐴)})) |
32 | | ccats1val1 13255 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝑥 ∈ (0..^(#‘𝐴))) → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = (𝐴‘𝑥)) |
33 | 32 | 3expa 1257 |
. . . . 5
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ (0..^(#‘𝐴))) → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = (𝐴‘𝑥)) |
34 | | simpr 476 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ (0..^(#‘𝐴))) → 𝑥 ∈ (0..^(#‘𝐴))) |
35 | | nelne2 2879 |
. . . . . . . 8
⊢ ((𝑥 ∈ (0..^(#‘𝐴)) ∧ ¬ (#‘𝐴) ∈ (0..^(#‘𝐴))) → 𝑥 ≠ (#‘𝐴)) |
36 | 34, 23, 35 | sylancl 693 |
. . . . . . 7
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ (0..^(#‘𝐴))) → 𝑥 ≠ (#‘𝐴)) |
37 | 36 | necomd 2837 |
. . . . . 6
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ (0..^(#‘𝐴))) → (#‘𝐴) ≠ 𝑥) |
38 | | fvunsn 6350 |
. . . . . 6
⊢
((#‘𝐴) ≠
𝑥 → ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉})‘𝑥) = (𝐴‘𝑥)) |
39 | 37, 38 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ (0..^(#‘𝐴))) → ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉})‘𝑥) = (𝐴‘𝑥)) |
40 | 33, 39 | eqtr4d 2647 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ (0..^(#‘𝐴))) → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉})‘𝑥)) |
41 | | fvex 6113 |
. . . . . . . . 9
⊢
(#‘𝐴) ∈
V |
42 | 41 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (#‘𝐴) ∈ V) |
43 | | elex 3185 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑋 → 𝐵 ∈ V) |
44 | 43 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐵 ∈ V) |
45 | | fdm 5964 |
. . . . . . . . . . 11
⊢ (𝐴:(0..^(#‘𝐴))⟶𝑋 → dom 𝐴 = (0..^(#‘𝐴))) |
46 | 18, 45 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → dom 𝐴 = (0..^(#‘𝐴))) |
47 | 46 | eleq2d 2673 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((#‘𝐴) ∈ dom 𝐴 ↔ (#‘𝐴) ∈ (0..^(#‘𝐴)))) |
48 | 23, 47 | mtbiri 316 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ¬ (#‘𝐴) ∈ dom 𝐴) |
49 | | fsnunfv 6358 |
. . . . . . . 8
⊢
(((#‘𝐴) ∈
V ∧ 𝐵 ∈ V ∧
¬ (#‘𝐴) ∈
dom 𝐴) → ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉})‘(#‘𝐴)) = 𝐵) |
50 | 42, 44, 48, 49 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉})‘(#‘𝐴)) = 𝐵) |
51 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐴 ∈ Word 𝑋) |
52 | | s1cl 13235 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑋 → 〈“𝐵”〉 ∈ Word 𝑋) |
53 | 52 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → 〈“𝐵”〉 ∈ Word 𝑋) |
54 | | s1len 13238 |
. . . . . . . . . . . 12
⊢
(#‘〈“𝐵”〉) = 1 |
55 | | 1nn 10908 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
56 | 54, 55 | eqeltri 2684 |
. . . . . . . . . . 11
⊢
(#‘〈“𝐵”〉) ∈
ℕ |
57 | 56 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (#‘〈“𝐵”〉) ∈
ℕ) |
58 | | lbfzo0 12375 |
. . . . . . . . . 10
⊢ (0 ∈
(0..^(#‘〈“𝐵”〉)) ↔
(#‘〈“𝐵”〉) ∈
ℕ) |
59 | 57, 58 | sylibr 223 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ∈
(0..^(#‘〈“𝐵”〉))) |
60 | | ccatval3 13216 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑋 ∧ 〈“𝐵”〉 ∈ Word 𝑋 ∧ 0 ∈
(0..^(#‘〈“𝐵”〉))) → ((𝐴 ++ 〈“𝐵”〉)‘(0 + (#‘𝐴))) = (〈“𝐵”〉‘0)) |
61 | 51, 53, 59, 60 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 ++ 〈“𝐵”〉)‘(0 + (#‘𝐴))) = (〈“𝐵”〉‘0)) |
62 | | s1fv 13243 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑋 → (〈“𝐵”〉‘0) = 𝐵) |
63 | 62 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (〈“𝐵”〉‘0) = 𝐵) |
64 | 61, 63 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 ++ 〈“𝐵”〉)‘(0 + (#‘𝐴))) = 𝐵) |
65 | 7 | nn0cnd 11230 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (#‘𝐴) ∈ ℂ) |
66 | 65 | addid2d 10116 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (0 + (#‘𝐴)) = (#‘𝐴)) |
67 | 66 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 ++ 〈“𝐵”〉)‘(0 + (#‘𝐴))) = ((𝐴 ++ 〈“𝐵”〉)‘(#‘𝐴))) |
68 | 50, 64, 67 | 3eqtr2rd 2651 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 ++ 〈“𝐵”〉)‘(#‘𝐴)) = ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉})‘(#‘𝐴))) |
69 | | elsni 4142 |
. . . . . . . 8
⊢ (𝑥 ∈ {(#‘𝐴)} → 𝑥 = (#‘𝐴)) |
70 | 69 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 ∈ {(#‘𝐴)} → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = ((𝐴 ++ 〈“𝐵”〉)‘(#‘𝐴))) |
71 | 69 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 ∈ {(#‘𝐴)} → ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉})‘𝑥) = ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉})‘(#‘𝐴))) |
72 | 70, 71 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑥 ∈ {(#‘𝐴)} → (((𝐴 ++ 〈“𝐵”〉)‘𝑥) = ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉})‘𝑥) ↔ ((𝐴 ++ 〈“𝐵”〉)‘(#‘𝐴)) = ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉})‘(#‘𝐴)))) |
73 | 68, 72 | syl5ibrcom 236 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑥 ∈ {(#‘𝐴)} → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉})‘𝑥))) |
74 | 73 | imp 444 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ {(#‘𝐴)}) → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉})‘𝑥)) |
75 | 40, 74 | jaodan 822 |
. . 3
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑥 ∈ (0..^(#‘𝐴)) ∨ 𝑥 ∈ {(#‘𝐴)})) → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉})‘𝑥)) |
76 | 31, 75 | sylan2b 491 |
. 2
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑥 ∈ ((0..^(#‘𝐴)) ∪ {(#‘𝐴)})) → ((𝐴 ++ 〈“𝐵”〉)‘𝑥) = ((𝐴 ∪ {〈(#‘𝐴), 𝐵〉})‘𝑥)) |
77 | 16, 30, 76 | eqfnfvd 6222 |
1
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ++ 〈“𝐵”〉) = (𝐴 ∪ {〈(#‘𝐴), 𝐵〉})) |