Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sseqf Structured version   Visualization version   GIF version

Theorem sseqf 29582
Description: A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019.)
Hypotheses
Ref Expression
sseqval.1 (𝜑𝑆 ∈ V)
sseqval.2 (𝜑𝑀 ∈ Word 𝑆)
sseqval.3 𝑊 = (Word 𝑆 ∩ (# “ (ℤ‘(#‘𝑀))))
sseqval.4 (𝜑𝐹:𝑊𝑆)
Assertion
Ref Expression
sseqf (𝜑 → (𝑀seqstr𝐹):ℕ0𝑆)

Proof of Theorem sseqf
Dummy variables 𝑥 𝑦 𝑎 𝑏 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseqval.2 . . . 4 (𝜑𝑀 ∈ Word 𝑆)
2 wrdf 13106 . . . 4 (𝑀 ∈ Word 𝑆𝑀:(0..^(#‘𝑀))⟶𝑆)
31, 2syl 17 . . 3 (𝜑𝑀:(0..^(#‘𝑀))⟶𝑆)
4 vex 3170 . . . . . . . . 9 𝑤 ∈ V
54a1i 11 . . . . . . . 8 ((𝜑𝑤 ∈ (𝑊 ∖ {∅})) → 𝑤 ∈ V)
6 fvex 6093 . . . . . . . . 9 (𝑥‘((#‘𝑥) − 1)) ∈ V
7 df-lsw 13096 . . . . . . . . 9 lastS = (𝑥 ∈ V ↦ (𝑥‘((#‘𝑥) − 1)))
86, 7dmmpti 5917 . . . . . . . 8 dom lastS = V
95, 8syl6eleqr 2693 . . . . . . 7 ((𝜑𝑤 ∈ (𝑊 ∖ {∅})) → 𝑤 ∈ dom lastS )
10 eldifsn 4254 . . . . . . . . 9 (𝑤 ∈ (𝑊 ∖ {∅}) ↔ (𝑤𝑊𝑤 ≠ ∅))
11 sseqval.3 . . . . . . . . . . . 12 𝑊 = (Word 𝑆 ∩ (# “ (ℤ‘(#‘𝑀))))
12 inss1 3789 . . . . . . . . . . . 12 (Word 𝑆 ∩ (# “ (ℤ‘(#‘𝑀)))) ⊆ Word 𝑆
1311, 12eqsstri 3592 . . . . . . . . . . 11 𝑊 ⊆ Word 𝑆
1413sseli 3558 . . . . . . . . . 10 (𝑤𝑊𝑤 ∈ Word 𝑆)
15 lswcl 13149 . . . . . . . . . 10 ((𝑤 ∈ Word 𝑆𝑤 ≠ ∅) → ( lastS ‘𝑤) ∈ 𝑆)
1614, 15sylan 486 . . . . . . . . 9 ((𝑤𝑊𝑤 ≠ ∅) → ( lastS ‘𝑤) ∈ 𝑆)
1710, 16sylbi 205 . . . . . . . 8 (𝑤 ∈ (𝑊 ∖ {∅}) → ( lastS ‘𝑤) ∈ 𝑆)
1817adantl 480 . . . . . . 7 ((𝜑𝑤 ∈ (𝑊 ∖ {∅})) → ( lastS ‘𝑤) ∈ 𝑆)
199, 18jca 552 . . . . . 6 ((𝜑𝑤 ∈ (𝑊 ∖ {∅})) → (𝑤 ∈ dom lastS ∧ ( lastS ‘𝑤) ∈ 𝑆))
2019ralrimiva 2943 . . . . 5 (𝜑 → ∀𝑤 ∈ (𝑊 ∖ {∅})(𝑤 ∈ dom lastS ∧ ( lastS ‘𝑤) ∈ 𝑆))
216, 7fnmpti 5916 . . . . . 6 lastS Fn V
22 fnfun 5883 . . . . . 6 ( lastS Fn V → Fun lastS )
23 ffvresb 6281 . . . . . 6 (Fun lastS → (( lastS ↾ (𝑊 ∖ {∅})):(𝑊 ∖ {∅})⟶𝑆 ↔ ∀𝑤 ∈ (𝑊 ∖ {∅})(𝑤 ∈ dom lastS ∧ ( lastS ‘𝑤) ∈ 𝑆)))
2421, 22, 23mp2b 10 . . . . 5 (( lastS ↾ (𝑊 ∖ {∅})):(𝑊 ∖ {∅})⟶𝑆 ↔ ∀𝑤 ∈ (𝑊 ∖ {∅})(𝑤 ∈ dom lastS ∧ ( lastS ‘𝑤) ∈ 𝑆))
2520, 24sylibr 222 . . . 4 (𝜑 → ( lastS ↾ (𝑊 ∖ {∅})):(𝑊 ∖ {∅})⟶𝑆)
26 eqid 2604 . . . . 5 (ℤ‘(#‘𝑀)) = (ℤ‘(#‘𝑀))
27 lencl 13120 . . . . . . 7 (𝑀 ∈ Word 𝑆 → (#‘𝑀) ∈ ℕ0)
2827nn0zd 11307 . . . . . 6 (𝑀 ∈ Word 𝑆 → (#‘𝑀) ∈ ℤ)
291, 28syl 17 . . . . 5 (𝜑 → (#‘𝑀) ∈ ℤ)
30 ovex 6550 . . . . . . 7 (𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ V
31 simpr 475 . . . . . . . . 9 ((𝜑𝑎 ∈ (ℤ‘(#‘𝑀))) → 𝑎 ∈ (ℤ‘(#‘𝑀)))
321, 27syl 17 . . . . . . . . . . 11 (𝜑 → (#‘𝑀) ∈ ℕ0)
3332adantr 479 . . . . . . . . . 10 ((𝜑𝑎 ∈ (ℤ‘(#‘𝑀))) → (#‘𝑀) ∈ ℕ0)
34 elnn0uz 11552 . . . . . . . . . 10 ((#‘𝑀) ∈ ℕ0 ↔ (#‘𝑀) ∈ (ℤ‘0))
3533, 34sylib 206 . . . . . . . . 9 ((𝜑𝑎 ∈ (ℤ‘(#‘𝑀))) → (#‘𝑀) ∈ (ℤ‘0))
36 uztrn 11531 . . . . . . . . 9 ((𝑎 ∈ (ℤ‘(#‘𝑀)) ∧ (#‘𝑀) ∈ (ℤ‘0)) → 𝑎 ∈ (ℤ‘0))
3731, 35, 36syl2anc 690 . . . . . . . 8 ((𝜑𝑎 ∈ (ℤ‘(#‘𝑀))) → 𝑎 ∈ (ℤ‘0))
38 nn0uz 11549 . . . . . . . 8 0 = (ℤ‘0)
3937, 38syl6eleqr 2693 . . . . . . 7 ((𝜑𝑎 ∈ (ℤ‘(#‘𝑀))) → 𝑎 ∈ ℕ0)
40 fvconst2g 6345 . . . . . . 7 (((𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ V ∧ 𝑎 ∈ ℕ0) → ((ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})‘𝑎) = (𝑀 ++ ⟨“(𝐹𝑀)”⟩))
4130, 39, 40sylancr 693 . . . . . 6 ((𝜑𝑎 ∈ (ℤ‘(#‘𝑀))) → ((ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})‘𝑎) = (𝑀 ++ ⟨“(𝐹𝑀)”⟩))
42 sseqval.4 . . . . . . . . . . . . 13 (𝜑𝐹:𝑊𝑆)
43 sseqval.1 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ V)
4443, 1, 11, 42sseqmw 29581 . . . . . . . . . . . . 13 (𝜑𝑀𝑊)
4542, 44ffvelrnd 6248 . . . . . . . . . . . 12 (𝜑 → (𝐹𝑀) ∈ 𝑆)
4645s1cld 13177 . . . . . . . . . . 11 (𝜑 → ⟨“(𝐹𝑀)”⟩ ∈ Word 𝑆)
47 ccatcl 13153 . . . . . . . . . . 11 ((𝑀 ∈ Word 𝑆 ∧ ⟨“(𝐹𝑀)”⟩ ∈ Word 𝑆) → (𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ Word 𝑆)
481, 46, 47syl2anc 690 . . . . . . . . . 10 (𝜑 → (𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ Word 𝑆)
4930a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ V)
50 ccatws1len 13192 . . . . . . . . . . . . 13 ((𝑀 ∈ Word 𝑆 ∧ (𝐹𝑀) ∈ 𝑆) → (#‘(𝑀 ++ ⟨“(𝐹𝑀)”⟩)) = ((#‘𝑀) + 1))
511, 45, 50syl2anc 690 . . . . . . . . . . . 12 (𝜑 → (#‘(𝑀 ++ ⟨“(𝐹𝑀)”⟩)) = ((#‘𝑀) + 1))
52 uzid 11529 . . . . . . . . . . . . 13 ((#‘𝑀) ∈ ℤ → (#‘𝑀) ∈ (ℤ‘(#‘𝑀)))
53 peano2uz 11568 . . . . . . . . . . . . 13 ((#‘𝑀) ∈ (ℤ‘(#‘𝑀)) → ((#‘𝑀) + 1) ∈ (ℤ‘(#‘𝑀)))
5429, 52, 533syl 18 . . . . . . . . . . . 12 (𝜑 → ((#‘𝑀) + 1) ∈ (ℤ‘(#‘𝑀)))
5551, 54eqeltrd 2682 . . . . . . . . . . 11 (𝜑 → (#‘(𝑀 ++ ⟨“(𝐹𝑀)”⟩)) ∈ (ℤ‘(#‘𝑀)))
56 hashf 12936 . . . . . . . . . . . 12 #:V⟶(ℕ0 ∪ {+∞})
57 ffn 5939 . . . . . . . . . . . 12 (#:V⟶(ℕ0 ∪ {+∞}) → # Fn V)
58 elpreima 6225 . . . . . . . . . . . 12 (# Fn V → ((𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ (# “ (ℤ‘(#‘𝑀))) ↔ ((𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ V ∧ (#‘(𝑀 ++ ⟨“(𝐹𝑀)”⟩)) ∈ (ℤ‘(#‘𝑀)))))
5956, 57, 58mp2b 10 . . . . . . . . . . 11 ((𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ (# “ (ℤ‘(#‘𝑀))) ↔ ((𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ V ∧ (#‘(𝑀 ++ ⟨“(𝐹𝑀)”⟩)) ∈ (ℤ‘(#‘𝑀))))
6049, 55, 59sylanbrc 694 . . . . . . . . . 10 (𝜑 → (𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ (# “ (ℤ‘(#‘𝑀))))
6148, 60elind 3754 . . . . . . . . 9 (𝜑 → (𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ (Word 𝑆 ∩ (# “ (ℤ‘(#‘𝑀)))))
6261, 11syl6eleqr 2693 . . . . . . . 8 (𝜑 → (𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ 𝑊)
6362adantr 479 . . . . . . 7 ((𝜑𝑎 ∈ (ℤ‘(#‘𝑀))) → (𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ 𝑊)
641adantr 479 . . . . . . . 8 ((𝜑𝑎 ∈ (ℤ‘(#‘𝑀))) → 𝑀 ∈ Word 𝑆)
6542adantr 479 . . . . . . . . 9 ((𝜑𝑎 ∈ (ℤ‘(#‘𝑀))) → 𝐹:𝑊𝑆)
6644adantr 479 . . . . . . . . 9 ((𝜑𝑎 ∈ (ℤ‘(#‘𝑀))) → 𝑀𝑊)
6765, 66ffvelrnd 6248 . . . . . . . 8 ((𝜑𝑎 ∈ (ℤ‘(#‘𝑀))) → (𝐹𝑀) ∈ 𝑆)
68 ccatws1n0 13202 . . . . . . . 8 ((𝑀 ∈ Word 𝑆 ∧ (𝐹𝑀) ∈ 𝑆) → (𝑀 ++ ⟨“(𝐹𝑀)”⟩) ≠ ∅)
6964, 67, 68syl2anc 690 . . . . . . 7 ((𝜑𝑎 ∈ (ℤ‘(#‘𝑀))) → (𝑀 ++ ⟨“(𝐹𝑀)”⟩) ≠ ∅)
70 eldifsn 4254 . . . . . . 7 ((𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ (𝑊 ∖ {∅}) ↔ ((𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ 𝑊 ∧ (𝑀 ++ ⟨“(𝐹𝑀)”⟩) ≠ ∅))
7163, 69, 70sylanbrc 694 . . . . . 6 ((𝜑𝑎 ∈ (ℤ‘(#‘𝑀))) → (𝑀 ++ ⟨“(𝐹𝑀)”⟩) ∈ (𝑊 ∖ {∅}))
7241, 71eqeltrd 2682 . . . . 5 ((𝜑𝑎 ∈ (ℤ‘(#‘𝑀))) → ((ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})‘𝑎) ∈ (𝑊 ∖ {∅}))
73 eqidd 2605 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)) = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)))
74 simprl 789 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) ∧ (𝑥 = 𝑎𝑦 = 𝑏)) → 𝑥 = 𝑎)
7574fveq2d 6087 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) ∧ (𝑥 = 𝑎𝑦 = 𝑏)) → (𝐹𝑥) = (𝐹𝑎))
7675s1eqd 13175 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) ∧ (𝑥 = 𝑎𝑦 = 𝑏)) → ⟨“(𝐹𝑥)”⟩ = ⟨“(𝐹𝑎)”⟩)
7774, 76oveq12d 6540 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) ∧ (𝑥 = 𝑎𝑦 = 𝑏)) → (𝑥 ++ ⟨“(𝐹𝑥)”⟩) = (𝑎 ++ ⟨“(𝐹𝑎)”⟩))
78 vex 3170 . . . . . . . 8 𝑎 ∈ V
7978a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ V)
80 vex 3170 . . . . . . . 8 𝑏 ∈ V
8180a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑏 ∈ V)
82 ovex 6550 . . . . . . . 8 (𝑎 ++ ⟨“(𝐹𝑎)”⟩) ∈ V
8382a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ ⟨“(𝐹𝑎)”⟩) ∈ V)
8473, 77, 79, 81, 83ovmpt2d 6659 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩))𝑏) = (𝑎 ++ ⟨“(𝐹𝑎)”⟩))
85 eldifi 3688 . . . . . . . . . . . 12 (𝑎 ∈ (𝑊 ∖ {∅}) → 𝑎𝑊)
8685ad2antrl 759 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎𝑊)
8713, 86sseldi 3560 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ Word 𝑆)
8842adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝐹:𝑊𝑆)
8988, 86ffvelrnd 6248 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝐹𝑎) ∈ 𝑆)
9089s1cld 13177 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → ⟨“(𝐹𝑎)”⟩ ∈ Word 𝑆)
91 ccatcl 13153 . . . . . . . . . 10 ((𝑎 ∈ Word 𝑆 ∧ ⟨“(𝐹𝑎)”⟩ ∈ Word 𝑆) → (𝑎 ++ ⟨“(𝐹𝑎)”⟩) ∈ Word 𝑆)
9287, 90, 91syl2anc 690 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ ⟨“(𝐹𝑎)”⟩) ∈ Word 𝑆)
93 ccatws1len 13192 . . . . . . . . . . . 12 ((𝑎 ∈ Word 𝑆 ∧ (𝐹𝑎) ∈ 𝑆) → (#‘(𝑎 ++ ⟨“(𝐹𝑎)”⟩)) = ((#‘𝑎) + 1))
9487, 89, 93syl2anc 690 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (#‘(𝑎 ++ ⟨“(𝐹𝑎)”⟩)) = ((#‘𝑎) + 1))
9586, 11syl6eleq 2692 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ (Word 𝑆 ∩ (# “ (ℤ‘(#‘𝑀)))))
96 elin 3752 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (Word 𝑆 ∩ (# “ (ℤ‘(#‘𝑀)))) ↔ (𝑎 ∈ Word 𝑆𝑎 ∈ (# “ (ℤ‘(#‘𝑀)))))
9796simprbi 478 . . . . . . . . . . . . . . 15 (𝑎 ∈ (Word 𝑆 ∩ (# “ (ℤ‘(#‘𝑀)))) → 𝑎 ∈ (# “ (ℤ‘(#‘𝑀))))
9895, 97syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → 𝑎 ∈ (# “ (ℤ‘(#‘𝑀))))
99 elpreima 6225 . . . . . . . . . . . . . . 15 (# Fn V → (𝑎 ∈ (# “ (ℤ‘(#‘𝑀))) ↔ (𝑎 ∈ V ∧ (#‘𝑎) ∈ (ℤ‘(#‘𝑀)))))
10056, 57, 99mp2b 10 . . . . . . . . . . . . . 14 (𝑎 ∈ (# “ (ℤ‘(#‘𝑀))) ↔ (𝑎 ∈ V ∧ (#‘𝑎) ∈ (ℤ‘(#‘𝑀))))
10198, 100sylib 206 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ∈ V ∧ (#‘𝑎) ∈ (ℤ‘(#‘𝑀))))
102101simprd 477 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (#‘𝑎) ∈ (ℤ‘(#‘𝑀)))
103 peano2uz 11568 . . . . . . . . . . . 12 ((#‘𝑎) ∈ (ℤ‘(#‘𝑀)) → ((#‘𝑎) + 1) ∈ (ℤ‘(#‘𝑀)))
104102, 103syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → ((#‘𝑎) + 1) ∈ (ℤ‘(#‘𝑀)))
10594, 104eqeltrd 2682 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (#‘(𝑎 ++ ⟨“(𝐹𝑎)”⟩)) ∈ (ℤ‘(#‘𝑀)))
106 elpreima 6225 . . . . . . . . . . 11 (# Fn V → ((𝑎 ++ ⟨“(𝐹𝑎)”⟩) ∈ (# “ (ℤ‘(#‘𝑀))) ↔ ((𝑎 ++ ⟨“(𝐹𝑎)”⟩) ∈ V ∧ (#‘(𝑎 ++ ⟨“(𝐹𝑎)”⟩)) ∈ (ℤ‘(#‘𝑀)))))
10756, 57, 106mp2b 10 . . . . . . . . . 10 ((𝑎 ++ ⟨“(𝐹𝑎)”⟩) ∈ (# “ (ℤ‘(#‘𝑀))) ↔ ((𝑎 ++ ⟨“(𝐹𝑎)”⟩) ∈ V ∧ (#‘(𝑎 ++ ⟨“(𝐹𝑎)”⟩)) ∈ (ℤ‘(#‘𝑀))))
10883, 105, 107sylanbrc 694 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ ⟨“(𝐹𝑎)”⟩) ∈ (# “ (ℤ‘(#‘𝑀))))
10992, 108elind 3754 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ ⟨“(𝐹𝑎)”⟩) ∈ (Word 𝑆 ∩ (# “ (ℤ‘(#‘𝑀)))))
110109, 11syl6eleqr 2693 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ ⟨“(𝐹𝑎)”⟩) ∈ 𝑊)
111 ccatws1n0 13202 . . . . . . . 8 ((𝑎 ∈ Word 𝑆 ∧ (𝐹𝑎) ∈ 𝑆) → (𝑎 ++ ⟨“(𝐹𝑎)”⟩) ≠ ∅)
11287, 89, 111syl2anc 690 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ ⟨“(𝐹𝑎)”⟩) ≠ ∅)
113 eldifsn 4254 . . . . . . 7 ((𝑎 ++ ⟨“(𝐹𝑎)”⟩) ∈ (𝑊 ∖ {∅}) ↔ ((𝑎 ++ ⟨“(𝐹𝑎)”⟩) ∈ 𝑊 ∧ (𝑎 ++ ⟨“(𝐹𝑎)”⟩) ≠ ∅))
114110, 112, 113sylanbrc 694 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎 ++ ⟨“(𝐹𝑎)”⟩) ∈ (𝑊 ∖ {∅}))
11584, 114eqeltrd 2682 . . . . 5 ((𝜑 ∧ (𝑎 ∈ (𝑊 ∖ {∅}) ∧ 𝑏 ∈ (𝑊 ∖ {∅}))) → (𝑎(𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩))𝑏) ∈ (𝑊 ∖ {∅}))
11626, 29, 72, 115seqf 12634 . . . 4 (𝜑 → seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})):(ℤ‘(#‘𝑀))⟶(𝑊 ∖ {∅}))
117 fco2 5953 . . . 4 ((( lastS ↾ (𝑊 ∖ {∅})):(𝑊 ∖ {∅})⟶𝑆 ∧ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})):(ℤ‘(#‘𝑀))⟶(𝑊 ∖ {∅})) → ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)}))):(ℤ‘(#‘𝑀))⟶𝑆)
11825, 116, 117syl2anc 690 . . 3 (𝜑 → ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)}))):(ℤ‘(#‘𝑀))⟶𝑆)
119 fzouzdisj 12323 . . . 4 ((0..^(#‘𝑀)) ∩ (ℤ‘(#‘𝑀))) = ∅
120119a1i 11 . . 3 (𝜑 → ((0..^(#‘𝑀)) ∩ (ℤ‘(#‘𝑀))) = ∅)
121 fun 5960 . . 3 (((𝑀:(0..^(#‘𝑀))⟶𝑆 ∧ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)}))):(ℤ‘(#‘𝑀))⟶𝑆) ∧ ((0..^(#‘𝑀)) ∩ (ℤ‘(#‘𝑀))) = ∅) → (𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})))):((0..^(#‘𝑀)) ∪ (ℤ‘(#‘𝑀)))⟶(𝑆𝑆))
1223, 118, 120, 121syl21anc 1316 . 2 (𝜑 → (𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})))):((0..^(#‘𝑀)) ∪ (ℤ‘(#‘𝑀)))⟶(𝑆𝑆))
12343, 1, 11, 42sseqval 29578 . . 3 (𝜑 → (𝑀seqstr𝐹) = (𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})))))
124 fzouzsplit 12322 . . . . . 6 ((#‘𝑀) ∈ (ℤ‘0) → (ℤ‘0) = ((0..^(#‘𝑀)) ∪ (ℤ‘(#‘𝑀))))
12534, 124sylbi 205 . . . . 5 ((#‘𝑀) ∈ ℕ0 → (ℤ‘0) = ((0..^(#‘𝑀)) ∪ (ℤ‘(#‘𝑀))))
1261, 27, 1253syl 18 . . . 4 (𝜑 → (ℤ‘0) = ((0..^(#‘𝑀)) ∪ (ℤ‘(#‘𝑀))))
12738, 126syl5eq 2650 . . 3 (𝜑 → ℕ0 = ((0..^(#‘𝑀)) ∪ (ℤ‘(#‘𝑀))))
128 unidm 3712 . . . . 5 (𝑆𝑆) = 𝑆
129128a1i 11 . . . 4 (𝜑 → (𝑆𝑆) = 𝑆)
130129eqcomd 2610 . . 3 (𝜑𝑆 = (𝑆𝑆))
131123, 127, 130feq123d 5928 . 2 (𝜑 → ((𝑀seqstr𝐹):ℕ0𝑆 ↔ (𝑀 ∪ ( lastS ∘ seq(#‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹𝑀)”⟩)})))):((0..^(#‘𝑀)) ∪ (ℤ‘(#‘𝑀)))⟶(𝑆𝑆)))
132122, 131mpbird 245 1 (𝜑 → (𝑀seqstr𝐹):ℕ0𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1975  wne 2774  wral 2890  Vcvv 3167  cdif 3531  cun 3532  cin 3533  c0 3868  {csn 4119   × cxp 5021  ccnv 5022  dom cdm 5023  cres 5025  cima 5026  ccom 5027  Fun wfun 5779   Fn wfn 5780  wf 5781  cfv 5785  (class class class)co 6522  cmpt2 6524  0cc0 9787  1c1 9788   + caddc 9790  +∞cpnf 9922  cmin 10112  0cn0 11134  cz 11205  cuz 11514  ..^cfzo 12284  seqcseq 12613  #chash 12929  Word cword 13087   lastS clsw 13088   ++ cconcat 13089  ⟨“cs1 13090  seqstrcsseq 29573
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-rep 4688  ax-sep 4698  ax-nul 4707  ax-pow 4759  ax-pr 4823  ax-un 6819  ax-inf2 8393  ax-cnex 9843  ax-resscn 9844  ax-1cn 9845  ax-icn 9846  ax-addcl 9847  ax-addrcl 9848  ax-mulcl 9849  ax-mulrcl 9850  ax-mulcom 9851  ax-addass 9852  ax-mulass 9853  ax-distr 9854  ax-i2m1 9855  ax-1ne0 9856  ax-1rid 9857  ax-rnegex 9858  ax-rrecex 9859  ax-cnre 9860  ax-pre-lttri 9861  ax-pre-lttrn 9862  ax-pre-ltadd 9863  ax-pre-mulgt0 9864
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ne 2776  df-nel 2777  df-ral 2895  df-rex 2896  df-reu 2897  df-rab 2899  df-v 3169  df-sbc 3397  df-csb 3494  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-pss 3550  df-nul 3869  df-if 4031  df-pw 4104  df-sn 4120  df-pr 4122  df-tp 4124  df-op 4126  df-uni 4362  df-int 4400  df-iun 4446  df-br 4573  df-opab 4633  df-mpt 4634  df-tr 4670  df-eprel 4934  df-id 4938  df-po 4944  df-so 4945  df-fr 4982  df-we 4984  df-xp 5029  df-rel 5030  df-cnv 5031  df-co 5032  df-dm 5033  df-rn 5034  df-res 5035  df-ima 5036  df-pred 5578  df-ord 5624  df-on 5625  df-lim 5626  df-suc 5627  df-iota 5749  df-fun 5787  df-fn 5788  df-f 5789  df-f1 5790  df-fo 5791  df-f1o 5792  df-fv 5793  df-riota 6484  df-ov 6525  df-oprab 6526  df-mpt2 6527  df-om 6930  df-1st 7031  df-2nd 7032  df-wrecs 7266  df-recs 7327  df-rdg 7365  df-1o 7419  df-oadd 7423  df-er 7601  df-map 7718  df-pm 7719  df-en 7814  df-dom 7815  df-sdom 7816  df-fin 7817  df-card 8620  df-pnf 9927  df-mnf 9928  df-xr 9929  df-ltxr 9930  df-le 9931  df-sub 10114  df-neg 10115  df-nn 10863  df-n0 11135  df-z 11206  df-uz 11515  df-fz 12148  df-fzo 12285  df-seq 12614  df-hash 12930  df-word 13095  df-lsw 13096  df-concat 13097  df-s1 13098  df-sseq 29574
This theorem is referenced by:  sseqp1  29585  fibp1  29591
  Copyright terms: Public domain W3C validator