Step | Hyp | Ref
| Expression |
1 | | sseqval.2 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ Word 𝑆) |
2 | | wrdf 14074 |
. . . 4
⊢ (𝑀 ∈ Word 𝑆 → 𝑀:(0..^(♯‘𝑀))⟶𝑆) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝑀:(0..^(♯‘𝑀))⟶𝑆) |
4 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑤 ∈ V |
5 | 4 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑊 ∖ {∅})) → 𝑤 ∈ V) |
6 | | fvex 6730 |
. . . . . . . . 9
⊢ (𝑥‘((♯‘𝑥) − 1)) ∈
V |
7 | | df-lsw 14118 |
. . . . . . . . 9
⊢ lastS =
(𝑥 ∈ V ↦ (𝑥‘((♯‘𝑥) − 1))) |
8 | 6, 7 | dmmpti 6522 |
. . . . . . . 8
⊢ dom lastS
= V |
9 | 5, 8 | eleqtrrdi 2849 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑊 ∖ {∅})) → 𝑤 ∈ dom
lastS) |
10 | | eldifsn 4700 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝑊 ∖ {∅}) ↔ (𝑤 ∈ 𝑊 ∧ 𝑤 ≠ ∅)) |
11 | | sseqval.3 |
. . . . . . . . . . . 12
⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “
(ℤ≥‘(♯‘𝑀)))) |
12 | | inss1 4143 |
. . . . . . . . . . . 12
⊢ (Word
𝑆 ∩ (◡♯ “
(ℤ≥‘(♯‘𝑀)))) ⊆ Word 𝑆 |
13 | 11, 12 | eqsstri 3935 |
. . . . . . . . . . 11
⊢ 𝑊 ⊆ Word 𝑆 |
14 | 13 | sseli 3896 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝑊 → 𝑤 ∈ Word 𝑆) |
15 | | lswcl 14123 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ Word 𝑆 ∧ 𝑤 ≠ ∅) → (lastS‘𝑤) ∈ 𝑆) |
16 | 14, 15 | sylan 583 |
. . . . . . . . 9
⊢ ((𝑤 ∈ 𝑊 ∧ 𝑤 ≠ ∅) → (lastS‘𝑤) ∈ 𝑆) |
17 | 10, 16 | sylbi 220 |
. . . . . . . 8
⊢ (𝑤 ∈ (𝑊 ∖ {∅}) →
(lastS‘𝑤) ∈
𝑆) |
18 | 17 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑊 ∖ {∅})) →
(lastS‘𝑤) ∈
𝑆) |
19 | 9, 18 | jca 515 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (𝑊 ∖ {∅})) → (𝑤 ∈ dom lastS ∧
(lastS‘𝑤) ∈
𝑆)) |
20 | 19 | ralrimiva 3105 |
. . . . 5
⊢ (𝜑 → ∀𝑤 ∈ (𝑊 ∖ {∅})(𝑤 ∈ dom lastS ∧ (lastS‘𝑤) ∈ 𝑆)) |
21 | 6, 7 | fnmpti 6521 |
. . . . . 6
⊢ lastS Fn
V |
22 | | fnfun 6479 |
. . . . . 6
⊢ (lastS Fn
V → Fun lastS) |
23 | | ffvresb 6941 |
. . . . . 6
⊢ (Fun
lastS → ((lastS ↾ (𝑊 ∖ {∅})):(𝑊 ∖ {∅})⟶𝑆 ↔ ∀𝑤 ∈ (𝑊 ∖ {∅})(𝑤 ∈ dom lastS ∧ (lastS‘𝑤) ∈ 𝑆))) |
24 | 21, 22, 23 | mp2b 10 |
. . . . 5
⊢ ((lastS
↾ (𝑊 ∖
{∅})):(𝑊 ∖
{∅})⟶𝑆 ↔
∀𝑤 ∈ (𝑊 ∖ {∅})(𝑤 ∈ dom lastS ∧
(lastS‘𝑤) ∈
𝑆)) |
25 | 20, 24 | sylibr 237 |
. . . 4
⊢ (𝜑 → (lastS ↾ (𝑊 ∖ {∅})):(𝑊 ∖ {∅})⟶𝑆) |
26 | | eqid 2737 |
. . . . 5
⊢
(ℤ≥‘(♯‘𝑀)) =
(ℤ≥‘(♯‘𝑀)) |
27 | | lencl 14088 |
. . . . . . 7
⊢ (𝑀 ∈ Word 𝑆 → (♯‘𝑀) ∈
ℕ0) |
28 | 27 | nn0zd 12280 |
. . . . . 6
⊢ (𝑀 ∈ Word 𝑆 → (♯‘𝑀) ∈ ℤ) |
29 | 1, 28 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘𝑀) ∈
ℤ) |
30 | | ovex 7246 |
. . . . . . 7
⊢ (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ V |
31 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(♯‘𝑀))) → 𝑎 ∈
(ℤ≥‘(♯‘𝑀))) |
32 | 1, 27 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝑀) ∈
ℕ0) |
33 | 32 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(♯‘𝑀))) → (♯‘𝑀) ∈
ℕ0) |
34 | | elnn0uz 12479 |
. . . . . . . . . 10
⊢
((♯‘𝑀)
∈ ℕ0 ↔ (♯‘𝑀) ∈
(ℤ≥‘0)) |
35 | 33, 34 | sylib 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(♯‘𝑀))) → (♯‘𝑀) ∈
(ℤ≥‘0)) |
36 | | uztrn 12456 |
. . . . . . . . 9
⊢ ((𝑎 ∈
(ℤ≥‘(♯‘𝑀)) ∧ (♯‘𝑀) ∈ (ℤ≥‘0))
→ 𝑎 ∈
(ℤ≥‘0)) |
37 | 31, 35, 36 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(♯‘𝑀))) → 𝑎 ∈
(ℤ≥‘0)) |
38 | | nn0uz 12476 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
39 | 37, 38 | eleqtrrdi 2849 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(♯‘𝑀))) → 𝑎 ∈ ℕ0) |
40 | | fvconst2g 7017 |
. . . . . . 7
⊢ (((𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ V ∧ 𝑎 ∈ ℕ0)
→ ((ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘𝑎) = (𝑀 ++ 〈“(𝐹‘𝑀)”〉)) |
41 | 30, 39, 40 | sylancr 590 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(♯‘𝑀))) → ((ℕ0 ×
{(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘𝑎) = (𝑀 ++ 〈“(𝐹‘𝑀)”〉)) |
42 | | sseqval.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝑊⟶𝑆) |
43 | | sseqval.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ V) |
44 | 43, 1, 11, 42 | sseqmw 32070 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ 𝑊) |
45 | 42, 44 | ffvelrnd 6905 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝑆) |
46 | 45 | s1cld 14160 |
. . . . . . . . . . 11
⊢ (𝜑 → 〈“(𝐹‘𝑀)”〉 ∈ Word 𝑆) |
47 | | ccatcl 14129 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ Word 𝑆 ∧ 〈“(𝐹‘𝑀)”〉 ∈ Word 𝑆) → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ Word 𝑆) |
48 | 1, 46, 47 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ Word 𝑆) |
49 | 30 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ V) |
50 | | ccatws1len 14177 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ Word 𝑆 → (♯‘(𝑀 ++ 〈“(𝐹‘𝑀)”〉)) = ((♯‘𝑀) + 1)) |
51 | 1, 50 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(𝑀 ++ 〈“(𝐹‘𝑀)”〉)) = ((♯‘𝑀) + 1)) |
52 | | uzid 12453 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑀)
∈ ℤ → (♯‘𝑀) ∈
(ℤ≥‘(♯‘𝑀))) |
53 | | peano2uz 12497 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑀)
∈ (ℤ≥‘(♯‘𝑀)) → ((♯‘𝑀) + 1) ∈
(ℤ≥‘(♯‘𝑀))) |
54 | 29, 52, 53 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘𝑀) + 1) ∈
(ℤ≥‘(♯‘𝑀))) |
55 | 51, 54 | eqeltrd 2838 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘(𝑀 ++ 〈“(𝐹‘𝑀)”〉)) ∈
(ℤ≥‘(♯‘𝑀))) |
56 | | hashf 13904 |
. . . . . . . . . . . 12
⊢
♯:V⟶(ℕ0 ∪ {+∞}) |
57 | | ffn 6545 |
. . . . . . . . . . . 12
⊢
(♯:V⟶(ℕ0 ∪ {+∞}) → ♯
Fn V) |
58 | | elpreima 6878 |
. . . . . . . . . . . 12
⊢ (♯
Fn V → ((𝑀 ++
〈“(𝐹‘𝑀)”〉) ∈ (◡♯ “
(ℤ≥‘(♯‘𝑀))) ↔ ((𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ V ∧
(♯‘(𝑀 ++
〈“(𝐹‘𝑀)”〉)) ∈
(ℤ≥‘(♯‘𝑀))))) |
59 | 56, 57, 58 | mp2b 10 |
. . . . . . . . . . 11
⊢ ((𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ (◡♯ “
(ℤ≥‘(♯‘𝑀))) ↔ ((𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ V ∧
(♯‘(𝑀 ++
〈“(𝐹‘𝑀)”〉)) ∈
(ℤ≥‘(♯‘𝑀)))) |
60 | 49, 55, 59 | sylanbrc 586 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ (◡♯ “
(ℤ≥‘(♯‘𝑀)))) |
61 | 48, 60 | elind 4108 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ (Word 𝑆 ∩ (◡♯ “
(ℤ≥‘(♯‘𝑀))))) |
62 | 61, 11 | eleqtrrdi 2849 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ 𝑊) |
63 | 62 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(♯‘𝑀))) → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ 𝑊) |
64 | | ccatws1n0 14194 |
. . . . . . . . 9
⊢ (𝑀 ∈ Word 𝑆 → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ≠
∅) |
65 | 1, 64 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ≠
∅) |
66 | 65 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(♯‘𝑀))) → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ≠
∅) |
67 | | eldifsn 4700 |
. . . . . . 7
⊢ ((𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ (𝑊 ∖ {∅}) ↔ ((𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ 𝑊 ∧ (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ≠
∅)) |
68 | 63, 66, 67 | sylanbrc 586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(♯‘𝑀))) → (𝑀 ++ 〈“(𝐹‘𝑀)”〉) ∈ (𝑊 ∖ {∅})) |
69 | 41, 68 | eqeltrd 2838 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈
(ℤ≥‘(♯‘𝑀))) → ((ℕ0 ×
{(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})‘𝑎) ∈ (𝑊 ∖ {∅})) |
70 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)) = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))) |
71 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → 𝑥 = 𝑎) |
72 | 71 | fveq2d 6721 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → (𝐹‘𝑥) = (𝐹‘𝑎)) |
73 | 72 | s1eqd 14158 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → 〈“(𝐹‘𝑥)”〉 = 〈“(𝐹‘𝑎)”〉) |
74 | 71, 73 | oveq12d 7231 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → (𝑥 ++ 〈“(𝐹‘𝑥)”〉) = (𝑎 ++ 〈“(𝐹‘𝑎)”〉)) |
75 | | vex 3412 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
76 | 75 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ V) |
77 | | vex 3412 |
. . . . . . . 8
⊢ 𝑏 ∈ V |
78 | 77 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑏 ∈ V) |
79 | | ovex 7246 |
. . . . . . . 8
⊢ (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ V |
80 | 79 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ V) |
81 | 70, 74, 76, 78, 80 | ovmpod 7361 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))𝑏) = (𝑎 ++ 〈“(𝐹‘𝑎)”〉)) |
82 | | eldifi 4041 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (𝑊 ∖ {∅}) → 𝑎 ∈ 𝑊) |
83 | 82 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ 𝑊) |
84 | 13, 83 | sseldi 3899 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ Word 𝑆) |
85 | 42 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝐹:𝑊⟶𝑆) |
86 | 85, 83 | ffvelrnd 6905 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝐹‘𝑎) ∈ 𝑆) |
87 | 86 | s1cld 14160 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) →
〈“(𝐹‘𝑎)”〉 ∈ Word 𝑆) |
88 | | ccatcl 14129 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ Word 𝑆 ∧ 〈“(𝐹‘𝑎)”〉 ∈ Word 𝑆) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ Word 𝑆) |
89 | 84, 87, 88 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ Word 𝑆) |
90 | 13, 82 | sseldi 3899 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (𝑊 ∖ {∅}) → 𝑎 ∈ Word 𝑆) |
91 | 90 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ Word 𝑆) |
92 | | ccatws1len 14177 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ Word 𝑆 → (♯‘(𝑎 ++ 〈“(𝐹‘𝑎)”〉)) = ((♯‘𝑎) + 1)) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) →
(♯‘(𝑎 ++
〈“(𝐹‘𝑎)”〉)) =
((♯‘𝑎) +
1)) |
94 | 83, 11 | eleqtrdi 2848 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ (Word 𝑆 ∩ (◡♯ “
(ℤ≥‘(♯‘𝑀))))) |
95 | 94 | elin2d 4113 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ (◡♯ “
(ℤ≥‘(♯‘𝑀)))) |
96 | | elpreima 6878 |
. . . . . . . . . . . . . 14
⊢ (♯
Fn V → (𝑎 ∈
(◡♯ “
(ℤ≥‘(♯‘𝑀))) ↔ (𝑎 ∈ V ∧ (♯‘𝑎) ∈
(ℤ≥‘(♯‘𝑀))))) |
97 | 56, 57, 96 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (◡♯ “
(ℤ≥‘(♯‘𝑀))) ↔ (𝑎 ∈ V ∧ (♯‘𝑎) ∈
(ℤ≥‘(♯‘𝑀)))) |
98 | 95, 97 | sylib 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ∈ V ∧
(♯‘𝑎) ∈
(ℤ≥‘(♯‘𝑀)))) |
99 | | peano2uz 12497 |
. . . . . . . . . . . 12
⊢
((♯‘𝑎)
∈ (ℤ≥‘(♯‘𝑀)) → ((♯‘𝑎) + 1) ∈
(ℤ≥‘(♯‘𝑀))) |
100 | 98, 99 | simpl2im 507 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) →
((♯‘𝑎) + 1)
∈ (ℤ≥‘(♯‘𝑀))) |
101 | 93, 100 | eqeltrd 2838 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) →
(♯‘(𝑎 ++
〈“(𝐹‘𝑎)”〉)) ∈
(ℤ≥‘(♯‘𝑀))) |
102 | | elpreima 6878 |
. . . . . . . . . . 11
⊢ (♯
Fn V → ((𝑎 ++
〈“(𝐹‘𝑎)”〉) ∈ (◡♯ “
(ℤ≥‘(♯‘𝑀))) ↔ ((𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ V ∧
(♯‘(𝑎 ++
〈“(𝐹‘𝑎)”〉)) ∈
(ℤ≥‘(♯‘𝑀))))) |
103 | 56, 57, 102 | mp2b 10 |
. . . . . . . . . 10
⊢ ((𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ (◡♯ “
(ℤ≥‘(♯‘𝑀))) ↔ ((𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ V ∧
(♯‘(𝑎 ++
〈“(𝐹‘𝑎)”〉)) ∈
(ℤ≥‘(♯‘𝑀)))) |
104 | 80, 101, 103 | sylanbrc 586 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ (◡♯ “
(ℤ≥‘(♯‘𝑀)))) |
105 | 89, 104 | elind 4108 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ (Word 𝑆 ∩ (◡♯ “
(ℤ≥‘(♯‘𝑀))))) |
106 | 105, 11 | eleqtrrdi 2849 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ 𝑊) |
107 | | ccatws1n0 14194 |
. . . . . . . 8
⊢ (𝑎 ∈ Word 𝑆 → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ≠
∅) |
108 | 91, 107 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ≠
∅) |
109 | | eldifsn 4700 |
. . . . . . 7
⊢ ((𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ (𝑊 ∖ {∅}) ↔ ((𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ 𝑊 ∧ (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ≠
∅)) |
110 | 106, 108,
109 | sylanbrc 586 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ 〈“(𝐹‘𝑎)”〉) ∈ (𝑊 ∖ {∅})) |
111 | 81, 110 | eqeltrd 2838 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))𝑏) ∈ (𝑊 ∖ {∅})) |
112 | 26, 29, 69, 111 | seqf 13597 |
. . . 4
⊢ (𝜑 → seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})):(ℤ≥‘(♯‘𝑀))⟶(𝑊 ∖ {∅})) |
113 | | fco2 6572 |
. . . 4
⊢ (((lastS
↾ (𝑊 ∖
{∅})):(𝑊 ∖
{∅})⟶𝑆 ∧
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})):(ℤ≥‘(♯‘𝑀))⟶(𝑊 ∖ {∅})) → (lastS ∘ seq(♯‘𝑀)((𝑥
∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)}))):(ℤ≥‘(♯‘𝑀))⟶𝑆) |
114 | 25, 112, 113 | syl2anc 587 |
. . 3
⊢ (𝜑 → (lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))):(ℤ≥‘(♯‘𝑀))⟶𝑆) |
115 | | fzouzdisj 13278 |
. . . 4
⊢
((0..^(♯‘𝑀)) ∩
(ℤ≥‘(♯‘𝑀))) = ∅ |
116 | 115 | a1i 11 |
. . 3
⊢ (𝜑 → ((0..^(♯‘𝑀)) ∩
(ℤ≥‘(♯‘𝑀))) = ∅) |
117 | | fun 6581 |
. . 3
⊢ (((𝑀:(0..^(♯‘𝑀))⟶𝑆 ∧ (lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))):(ℤ≥‘(♯‘𝑀))⟶𝑆) ∧ ((0..^(♯‘𝑀)) ∩ (ℤ≥‘(♯‘𝑀))) = ∅) → (𝑀 ∪ (lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V,
𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0 × {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)})))):((0..^(♯‘𝑀)) ∪ (ℤ≥‘(♯‘𝑀)))⟶(𝑆 ∪ 𝑆)) |
118 | 3, 114, 116, 117 | syl21anc 838 |
. 2
⊢ (𝜑 → (𝑀 ∪ (lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))):((0..^(♯‘𝑀)) ∪
(ℤ≥‘(♯‘𝑀)))⟶(𝑆 ∪ 𝑆)) |
119 | 43, 1, 11, 42 | sseqval 32067 |
. . 3
⊢ (𝜑 → (𝑀seqstr𝐹) = (𝑀 ∪ (lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))))) |
120 | | fzouzsplit 13277 |
. . . . . 6
⊢
((♯‘𝑀)
∈ (ℤ≥‘0) → (ℤ≥‘0)
= ((0..^(♯‘𝑀))
∪ (ℤ≥‘(♯‘𝑀)))) |
121 | 34, 120 | sylbi 220 |
. . . . 5
⊢
((♯‘𝑀)
∈ ℕ0 → (ℤ≥‘0) =
((0..^(♯‘𝑀))
∪ (ℤ≥‘(♯‘𝑀)))) |
122 | 1, 27, 121 | 3syl 18 |
. . . 4
⊢ (𝜑 →
(ℤ≥‘0) = ((0..^(♯‘𝑀)) ∪
(ℤ≥‘(♯‘𝑀)))) |
123 | 38, 122 | syl5eq 2790 |
. . 3
⊢ (𝜑 → ℕ0 =
((0..^(♯‘𝑀))
∪ (ℤ≥‘(♯‘𝑀)))) |
124 | | unidm 4066 |
. . . . 5
⊢ (𝑆 ∪ 𝑆) = 𝑆 |
125 | 124 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑆 ∪ 𝑆) = 𝑆) |
126 | 125 | eqcomd 2743 |
. . 3
⊢ (𝜑 → 𝑆 = (𝑆 ∪ 𝑆)) |
127 | 119, 123,
126 | feq123d 6534 |
. 2
⊢ (𝜑 → ((𝑀seqstr𝐹):ℕ0⟶𝑆 ↔ (𝑀 ∪ (lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))):((0..^(♯‘𝑀)) ∪
(ℤ≥‘(♯‘𝑀)))⟶(𝑆 ∪ 𝑆))) |
128 | 118, 127 | mpbird 260 |
1
⊢ (𝜑 → (𝑀seqstr𝐹):ℕ0⟶𝑆) |