Step | Hyp | Ref
| Expression |
1 | | sseqval.2 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ Word 𝑆) |
2 | | wrdf 13165 |
. . . 4
⊢ (𝑀 ∈ Word 𝑆 → 𝑀:(0..^(#‘𝑀))⟶𝑆) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝑀:(0..^(#‘𝑀))⟶𝑆) |
4 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑤 ∈ V |
5 | 4 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑊 ∖ {∅})) → 𝑤 ∈ V) |
6 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝑥‘((#‘𝑥) − 1)) ∈
V |
7 | | df-lsw 13155 |
. . . . . . . . 9
⊢ lastS =
(𝑥 ∈ V ↦ (𝑥‘((#‘𝑥) − 1))) |
8 | 6, 7 | dmmpti 5936 |
. . . . . . . 8
⊢ dom lastS
= V |
9 | 5, 8 | syl6eleqr 2699 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑊 ∖ {∅})) → 𝑤 ∈ dom lastS
) |
10 | | eldifsn 4260 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝑊 ∖ {∅}) ↔ (𝑤 ∈ 𝑊 ∧ 𝑤 ≠ ∅)) |
11 | | sseqval.3 |
. . . . . . . . . . . 12
⊢ 𝑊 = (Word 𝑆 ∩ (◡# “
(ℤ≥‘(#‘𝑀)))) |
12 | | inss1 3795 |
. . . . . . . . . . . 12
⊢ (Word
𝑆 ∩ (◡# “
(ℤ≥‘(#‘𝑀)))) ⊆ Word 𝑆 |
13 | 11, 12 | eqsstri 3598 |
. . . . . . . . . . 11
⊢ 𝑊 ⊆ Word 𝑆 |
14 | 13 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝑊 → 𝑤 ∈ Word 𝑆) |
15 | | lswcl 13208 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ Word 𝑆 ∧ 𝑤 ≠ ∅) → ( lastS ‘𝑤) ∈ 𝑆) |
16 | 14, 15 | sylan 487 |
. . . . . . . . 9
⊢ ((𝑤 ∈ 𝑊 ∧ 𝑤 ≠ ∅) → ( lastS ‘𝑤) ∈ 𝑆) |
17 | 10, 16 | sylbi 206 |
. . . . . . . 8
⊢ (𝑤 ∈ (𝑊 ∖ {∅}) → ( lastS
‘𝑤) ∈ 𝑆) |
18 | 17 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑊 ∖ {∅})) → ( lastS
‘𝑤) ∈ 𝑆) |
19 | 9, 18 | jca 553 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑊 ∖ {∅})) → (𝑤 ∈ dom lastS ∧ ( lastS
‘𝑤) ∈ 𝑆)) |
20 | 19 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑤 ∈ (𝑊 ∖ {∅})(𝑤 ∈ dom lastS ∧ ( lastS ‘𝑤) ∈ 𝑆)) |
21 | 6, 7 | fnmpti 5935 |
. . . . . 6
⊢ lastS Fn
V |
22 | | fnfun 5902 |
. . . . . 6
⊢ ( lastS
Fn V → Fun lastS ) |
23 | | ffvresb 6301 |
. . . . . 6
⊢ (Fun
lastS → (( lastS ↾ (𝑊 ∖ {∅})):(𝑊 ∖ {∅})⟶𝑆 ↔ ∀𝑤 ∈ (𝑊 ∖ {∅})(𝑤 ∈ dom lastS ∧ ( lastS ‘𝑤) ∈ 𝑆))) |
24 | 21, 22, 23 | mp2b 10 |
. . . . 5
⊢ (( lastS
↾ (𝑊 ∖
{∅})):(𝑊 ∖
{∅})⟶𝑆 ↔
∀𝑤 ∈ (𝑊 ∖ {∅})(𝑤 ∈ dom lastS ∧ ( lastS
‘𝑤) ∈ 𝑆)) |
25 | 20, 24 | sylibr 223 |
. . . 4
⊢ (𝜑 → ( lastS ↾ (𝑊 ∖ {∅})):(𝑊 ∖ {∅})⟶𝑆) |
26 | | eqid 2610 |
. . . . 5
⊢
(ℤ≥‘(#‘𝑀)) =
(ℤ≥‘(#‘𝑀)) |
27 | | lencl 13179 |
. . . . . . 7
⊢ (𝑀 ∈ Word 𝑆 → (#‘𝑀) ∈
ℕ0) |
28 | 27 | nn0zd 11356 |
. . . . . 6
⊢ (𝑀 ∈ Word 𝑆 → (#‘𝑀) ∈ ℤ) |
29 | 1, 28 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘𝑀) ∈ ℤ) |
30 | | ovex 6577 |
. . . . . . 7
⊢ (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ V |
31 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(#‘𝑀))) → 𝑎 ∈
(ℤ≥‘(#‘𝑀))) |
32 | 1, 27 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘𝑀) ∈
ℕ0) |
33 | 32 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(#‘𝑀))) → (#‘𝑀) ∈
ℕ0) |
34 | | elnn0uz 11601 |
. . . . . . . . . 10
⊢
((#‘𝑀) ∈
ℕ0 ↔ (#‘𝑀) ∈
(ℤ≥‘0)) |
35 | 33, 34 | sylib 207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(#‘𝑀))) → (#‘𝑀) ∈
(ℤ≥‘0)) |
36 | | uztrn 11580 |
. . . . . . . . 9
⊢ ((𝑎 ∈
(ℤ≥‘(#‘𝑀)) ∧ (#‘𝑀) ∈ (ℤ≥‘0))
→ 𝑎 ∈
(ℤ≥‘0)) |
37 | 31, 35, 36 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(#‘𝑀))) → 𝑎 ∈
(ℤ≥‘0)) |
38 | | nn0uz 11598 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
39 | 37, 38 | syl6eleqr 2699 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(#‘𝑀))) → 𝑎 ∈ ℕ0) |
40 | | fvconst2g 6372 |
. . . . . . 7
⊢ (((𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ V ∧ 𝑎 ∈ ℕ0)
→ ((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘𝑎) = (𝑀 ++ 〈“(𝐹‘𝑀)”〉)) |
41 | 30, 39, 40 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(#‘𝑀))) → ((ℕ0 ×
{(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘𝑎) = (𝑀 ++ 〈“(𝐹‘𝑀)”〉)) |
42 | | sseqval.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝑊⟶𝑆) |
43 | | sseqval.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ V) |
44 | 43, 1, 11, 42 | sseqmw 29780 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ 𝑊) |
45 | 42, 44 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝑆) |
46 | 45 | s1cld 13236 |
. . . . . . . . . . 11
⊢ (𝜑 → 〈“(𝐹‘𝑀)”〉 ∈ Word 𝑆) |
47 | | ccatcl 13212 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ Word 𝑆 ∧ 〈“(𝐹‘𝑀)”〉 ∈ Word 𝑆) → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ Word 𝑆) |
48 | 1, 46, 47 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ Word 𝑆) |
49 | 30 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ V) |
50 | | ccatws1len 13251 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ Word 𝑆 ∧ (𝐹‘𝑀) ∈ 𝑆) → (#‘(𝑀 ++ 〈“(𝐹‘𝑀)”〉)) = ((#‘𝑀) + 1)) |
51 | 1, 45, 50 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (#‘(𝑀 ++ 〈“(𝐹‘𝑀)”〉)) = ((#‘𝑀) + 1)) |
52 | | uzid 11578 |
. . . . . . . . . . . . 13
⊢
((#‘𝑀) ∈
ℤ → (#‘𝑀)
∈ (ℤ≥‘(#‘𝑀))) |
53 | | peano2uz 11617 |
. . . . . . . . . . . . 13
⊢
((#‘𝑀) ∈
(ℤ≥‘(#‘𝑀)) → ((#‘𝑀) + 1) ∈
(ℤ≥‘(#‘𝑀))) |
54 | 29, 52, 53 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((#‘𝑀) + 1) ∈
(ℤ≥‘(#‘𝑀))) |
55 | 51, 54 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘(𝑀 ++ 〈“(𝐹‘𝑀)”〉)) ∈
(ℤ≥‘(#‘𝑀))) |
56 | | hashf 12987 |
. . . . . . . . . . . 12
⊢
#:V⟶(ℕ0 ∪ {+∞}) |
57 | | ffn 5958 |
. . . . . . . . . . . 12
⊢
(#:V⟶(ℕ0 ∪ {+∞}) → # Fn
V) |
58 | | elpreima 6245 |
. . . . . . . . . . . 12
⊢ (# Fn V
→ ((𝑀 ++
〈“(𝐹‘𝑀)”〉) ∈ (◡# “
(ℤ≥‘(#‘𝑀))) ↔ ((𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ V ∧
(#‘(𝑀 ++
〈“(𝐹‘𝑀)”〉)) ∈
(ℤ≥‘(#‘𝑀))))) |
59 | 56, 57, 58 | mp2b 10 |
. . . . . . . . . . 11
⊢ ((𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ (◡# “
(ℤ≥‘(#‘𝑀))) ↔ ((𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ V ∧
(#‘(𝑀 ++
〈“(𝐹‘𝑀)”〉)) ∈
(ℤ≥‘(#‘𝑀)))) |
60 | 49, 55, 59 | sylanbrc 695 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ (◡# “
(ℤ≥‘(#‘𝑀)))) |
61 | 48, 60 | elind 3760 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ (Word 𝑆 ∩ (◡# “
(ℤ≥‘(#‘𝑀))))) |
62 | 61, 11 | syl6eleqr 2699 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ 𝑊) |
63 | 62 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(#‘𝑀))) → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ 𝑊) |
64 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(#‘𝑀))) → 𝑀 ∈ Word 𝑆) |
65 | 42 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(#‘𝑀))) → 𝐹:𝑊⟶𝑆) |
66 | 44 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(#‘𝑀))) → 𝑀 ∈ 𝑊) |
67 | 65, 66 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(#‘𝑀))) → (𝐹‘𝑀) ∈ 𝑆) |
68 | | ccatws1n0 13261 |
. . . . . . . 8
⊢ ((𝑀 ∈ Word 𝑆 ∧ (𝐹‘𝑀) ∈ 𝑆) → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ≠
∅) |
69 | 64, 67, 68 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(#‘𝑀))) → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ≠
∅) |
70 | | eldifsn 4260 |
. . . . . . 7
⊢ ((𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ (𝑊 ∖ {∅}) ↔ ((𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ 𝑊 ∧ (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ≠
∅)) |
71 | 63, 69, 70 | sylanbrc 695 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(#‘𝑀))) → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ (𝑊 ∖ {∅})) |
72 | 41, 71 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(#‘𝑀))) → ((ℕ0 ×
{(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘𝑎) ∈ (𝑊 ∖ {∅})) |
73 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)) = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))) |
74 | | simprl 790 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → 𝑥 = 𝑎) |
75 | 74 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → (𝐹‘𝑥) = (𝐹‘𝑎)) |
76 | 75 | s1eqd 13234 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → 〈“(𝐹‘𝑥)”〉 = 〈“(𝐹‘𝑎)”〉) |
77 | 74, 76 | oveq12d 6567 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → (𝑥 ++ 〈“(𝐹‘𝑥)”〉) = (𝑎 ++ 〈“(𝐹‘𝑎)”〉)) |
78 | | vex 3176 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
79 | 78 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ V) |
80 | | vex 3176 |
. . . . . . . 8
⊢ 𝑏 ∈ V |
81 | 80 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑏 ∈ V) |
82 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ V |
83 | 82 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ V) |
84 | 73, 77, 79, 81, 83 | ovmpt2d 6686 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))𝑏) = (𝑎 ++ 〈“(𝐹‘𝑎)”〉)) |
85 | | eldifi 3694 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (𝑊 ∖ {∅}) → 𝑎 ∈ 𝑊) |
86 | 85 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ 𝑊) |
87 | 13, 86 | sseldi 3566 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ Word 𝑆) |
88 | 42 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝐹:𝑊⟶𝑆) |
89 | 88, 86 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝐹‘𝑎) ∈ 𝑆) |
90 | 89 | s1cld 13236 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) →
〈“(𝐹‘𝑎)”〉 ∈ Word 𝑆) |
91 | | ccatcl 13212 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ Word 𝑆 ∧ 〈“(𝐹‘𝑎)”〉 ∈ Word 𝑆) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ Word 𝑆) |
92 | 87, 90, 91 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ Word 𝑆) |
93 | | ccatws1len 13251 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ Word 𝑆 ∧ (𝐹‘𝑎) ∈ 𝑆) → (#‘(𝑎 ++ 〈“(𝐹‘𝑎)”〉)) = ((#‘𝑎) + 1)) |
94 | 87, 89, 93 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (#‘(𝑎 ++ 〈“(𝐹‘𝑎)”〉)) = ((#‘𝑎) + 1)) |
95 | 86, 11 | syl6eleq 2698 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ (Word 𝑆 ∩ (◡# “
(ℤ≥‘(#‘𝑀))))) |
96 | | elin 3758 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (Word 𝑆 ∩ (◡# “
(ℤ≥‘(#‘𝑀)))) ↔ (𝑎 ∈ Word 𝑆 ∧ 𝑎 ∈ (◡# “
(ℤ≥‘(#‘𝑀))))) |
97 | 96 | simprbi 479 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (Word 𝑆 ∩ (◡# “
(ℤ≥‘(#‘𝑀)))) → 𝑎 ∈ (◡# “
(ℤ≥‘(#‘𝑀)))) |
98 | 95, 97 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ (◡# “
(ℤ≥‘(#‘𝑀)))) |
99 | | elpreima 6245 |
. . . . . . . . . . . . . . 15
⊢ (# Fn V
→ (𝑎 ∈ (◡# “
(ℤ≥‘(#‘𝑀))) ↔ (𝑎 ∈ V ∧ (#‘𝑎) ∈
(ℤ≥‘(#‘𝑀))))) |
100 | 56, 57, 99 | mp2b 10 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (◡# “
(ℤ≥‘(#‘𝑀))) ↔ (𝑎 ∈ V ∧ (#‘𝑎) ∈
(ℤ≥‘(#‘𝑀)))) |
101 | 98, 100 | sylib 207 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ∈ V ∧ (#‘𝑎) ∈
(ℤ≥‘(#‘𝑀)))) |
102 | 101 | simprd 478 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (#‘𝑎) ∈
(ℤ≥‘(#‘𝑀))) |
103 | | peano2uz 11617 |
. . . . . . . . . . . 12
⊢
((#‘𝑎) ∈
(ℤ≥‘(#‘𝑀)) → ((#‘𝑎) + 1) ∈
(ℤ≥‘(#‘𝑀))) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → ((#‘𝑎) + 1) ∈
(ℤ≥‘(#‘𝑀))) |
105 | 94, 104 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (#‘(𝑎 ++ 〈“(𝐹‘𝑎)”〉)) ∈
(ℤ≥‘(#‘𝑀))) |
106 | | elpreima 6245 |
. . . . . . . . . . 11
⊢ (# Fn V
→ ((𝑎 ++
〈“(𝐹‘𝑎)”〉) ∈ (◡# “
(ℤ≥‘(#‘𝑀))) ↔ ((𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ V ∧
(#‘(𝑎 ++
〈“(𝐹‘𝑎)”〉)) ∈
(ℤ≥‘(#‘𝑀))))) |
107 | 56, 57, 106 | mp2b 10 |
. . . . . . . . . 10
⊢ ((𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ (◡# “
(ℤ≥‘(#‘𝑀))) ↔ ((𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ V ∧
(#‘(𝑎 ++
〈“(𝐹‘𝑎)”〉)) ∈
(ℤ≥‘(#‘𝑀)))) |
108 | 83, 105, 107 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ (◡# “
(ℤ≥‘(#‘𝑀)))) |
109 | 92, 108 | elind 3760 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ (Word 𝑆 ∩ (◡# “
(ℤ≥‘(#‘𝑀))))) |
110 | 109, 11 | syl6eleqr 2699 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ 𝑊) |
111 | | ccatws1n0 13261 |
. . . . . . . 8
⊢ ((𝑎 ∈ Word 𝑆 ∧ (𝐹‘𝑎) ∈ 𝑆) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ≠
∅) |
112 | 87, 89, 111 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ≠
∅) |
113 | | eldifsn 4260 |
. . . . . . 7
⊢ ((𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ (𝑊 ∖ {∅}) ↔ ((𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ 𝑊 ∧ (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ≠
∅)) |
114 | 110, 112,
113 | sylanbrc 695 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ (𝑊 ∖ {∅})) |
115 | 84, 114 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))𝑏) ∈ (𝑊 ∖ {∅})) |
116 | 26, 29, 72, 115 | seqf 12684 |
. . . 4
⊢ (𝜑 → seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})):(ℤ≥‘(#‘𝑀))⟶(𝑊 ∖ {∅})) |
117 | | fco2 5972 |
. . . 4
⊢ ((( lastS
↾ (𝑊 ∖
{∅})):(𝑊 ∖
{∅})⟶𝑆 ∧
seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})):(ℤ≥‘(#‘𝑀))⟶(𝑊 ∖ {∅})) → ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦
∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)}))):(ℤ≥‘(#‘𝑀))⟶𝑆) |
118 | 25, 116, 117 | syl2anc 691 |
. . 3
⊢ (𝜑 → ( lastS ∘
seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))):(ℤ≥‘(#‘𝑀))⟶𝑆) |
119 | | fzouzdisj 12373 |
. . . 4
⊢
((0..^(#‘𝑀))
∩ (ℤ≥‘(#‘𝑀))) = ∅ |
120 | 119 | a1i 11 |
. . 3
⊢ (𝜑 → ((0..^(#‘𝑀)) ∩
(ℤ≥‘(#‘𝑀))) = ∅) |
121 | | fun 5979 |
. . 3
⊢ (((𝑀:(0..^(#‘𝑀))⟶𝑆 ∧ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))):(ℤ≥‘(#‘𝑀))⟶𝑆) ∧ ((0..^(#‘𝑀)) ∩ (ℤ≥‘(#‘𝑀))) = ∅) → (𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈
V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})))):((0..^(#‘𝑀)) ∪ (ℤ≥‘(#‘𝑀)))⟶(𝑆 ∪ 𝑆)) |
122 | 3, 118, 120, 121 | syl21anc 1317 |
. 2
⊢ (𝜑 → (𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))):((0..^(#‘𝑀)) ∪
(ℤ≥‘(#‘𝑀)))⟶(𝑆 ∪ 𝑆)) |
123 | 43, 1, 11, 42 | sseqval 29777 |
. . 3
⊢ (𝜑 → (𝑀seqstr𝐹) = (𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))))) |
124 | | fzouzsplit 12372 |
. . . . . 6
⊢
((#‘𝑀) ∈
(ℤ≥‘0) → (ℤ≥‘0) =
((0..^(#‘𝑀)) ∪
(ℤ≥‘(#‘𝑀)))) |
125 | 34, 124 | sylbi 206 |
. . . . 5
⊢
((#‘𝑀) ∈
ℕ0 → (ℤ≥‘0) =
((0..^(#‘𝑀)) ∪
(ℤ≥‘(#‘𝑀)))) |
126 | 1, 27, 125 | 3syl 18 |
. . . 4
⊢ (𝜑 →
(ℤ≥‘0) = ((0..^(#‘𝑀)) ∪
(ℤ≥‘(#‘𝑀)))) |
127 | 38, 126 | syl5eq 2656 |
. . 3
⊢ (𝜑 → ℕ0 =
((0..^(#‘𝑀)) ∪
(ℤ≥‘(#‘𝑀)))) |
128 | | unidm 3718 |
. . . . 5
⊢ (𝑆 ∪ 𝑆) = 𝑆 |
129 | 128 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑆 ∪ 𝑆) = 𝑆) |
130 | 129 | eqcomd 2616 |
. . 3
⊢ (𝜑 → 𝑆 = (𝑆 ∪ 𝑆)) |
131 | 123, 127,
130 | feq123d 5947 |
. 2
⊢ (𝜑 → ((𝑀seqstr𝐹):ℕ0⟶𝑆 ↔ (𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))):((0..^(#‘𝑀)) ∪
(ℤ≥‘(#‘𝑀)))⟶(𝑆 ∪ 𝑆))) |
132 | 122, 131 | mpbird 246 |
1
⊢ (𝜑 → (𝑀seqstr𝐹):ℕ0⟶𝑆) |