| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-sseq 34387 | . . 3
⊢
seqstr = (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝑓‘𝑥)”〉)), (ℕ0
× {(𝑚 ++
〈“(𝑓‘𝑚)”〉)}))))) | 
| 2 | 1 | a1i 11 | . 2
⊢ (𝜑 → seqstr = (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝑓‘𝑥)”〉)), (ℕ0
× {(𝑚 ++
〈“(𝑓‘𝑚)”〉)})))))) | 
| 3 |  | simprl 770 | . . 3
⊢ ((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) → 𝑚 = 𝑀) | 
| 4 | 3 | fveq2d 6909 | . . . . 5
⊢ ((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) → (♯‘𝑚) = (♯‘𝑀)) | 
| 5 |  | simp1rr 1239 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝑓 = 𝐹) | 
| 6 | 5 | fveq1d 6907 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑓‘𝑥) = (𝐹‘𝑥)) | 
| 7 | 6 | s1eqd 14640 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V) → 〈“(𝑓‘𝑥)”〉 = 〈“(𝐹‘𝑥)”〉) | 
| 8 | 7 | oveq2d 7448 | . . . . . 6
⊢ (((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ++ 〈“(𝑓‘𝑥)”〉) = (𝑥 ++ 〈“(𝐹‘𝑥)”〉)) | 
| 9 | 8 | mpoeq3dva 7511 | . . . . 5
⊢ ((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) → (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝑓‘𝑥)”〉)) = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉))) | 
| 10 |  | simprr 772 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) → 𝑓 = 𝐹) | 
| 11 | 10, 3 | fveq12d 6912 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) → (𝑓‘𝑚) = (𝐹‘𝑀)) | 
| 12 | 11 | s1eqd 14640 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) → 〈“(𝑓‘𝑚)”〉 = 〈“(𝐹‘𝑀)”〉) | 
| 13 | 3, 12 | oveq12d 7450 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) → (𝑚 ++ 〈“(𝑓‘𝑚)”〉) = (𝑀 ++ 〈“(𝐹‘𝑀)”〉)) | 
| 14 | 13 | sneqd 4637 | . . . . . 6
⊢ ((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) → {(𝑚 ++ 〈“(𝑓‘𝑚)”〉)} = {(𝑀 ++ 〈“(𝐹‘𝑀)”〉)}) | 
| 15 | 14 | xpeq2d 5714 | . . . . 5
⊢ ((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) → (ℕ0 ×
{(𝑚 ++ 〈“(𝑓‘𝑚)”〉)}) = (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) | 
| 16 | 4, 9, 15 | seqeq123d 14052 | . . . 4
⊢ ((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) → seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝑓‘𝑥)”〉)), (ℕ0
× {(𝑚 ++
〈“(𝑓‘𝑚)”〉)})) =
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) | 
| 17 | 16 | coeq2d 5872 | . . 3
⊢ ((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) → (lastS ∘
seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝑓‘𝑥)”〉)), (ℕ0
× {(𝑚 ++
〈“(𝑓‘𝑚)”〉)}))) = (lastS
∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))) | 
| 18 | 3, 17 | uneq12d 4168 | . 2
⊢ ((𝜑 ∧ (𝑚 = 𝑀 ∧ 𝑓 = 𝐹)) → (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝑓‘𝑥)”〉)), (ℕ0
× {(𝑚 ++
〈“(𝑓‘𝑚)”〉)})))) = (𝑀 ∪ (lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))))) | 
| 19 |  | sseqval.2 | . . 3
⊢ (𝜑 → 𝑀 ∈ Word 𝑆) | 
| 20 |  | elex 3500 | . . 3
⊢ (𝑀 ∈ Word 𝑆 → 𝑀 ∈ V) | 
| 21 | 19, 20 | syl 17 | . 2
⊢ (𝜑 → 𝑀 ∈ V) | 
| 22 |  | sseqval.4 | . . 3
⊢ (𝜑 → 𝐹:𝑊⟶𝑆) | 
| 23 |  | sseqval.3 | . . . 4
⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “
(ℤ≥‘(♯‘𝑀)))) | 
| 24 |  | sseqval.1 | . . . . 5
⊢ (𝜑 → 𝑆 ∈ V) | 
| 25 |  | wrdexg 14563 | . . . . 5
⊢ (𝑆 ∈ V → Word 𝑆 ∈ V) | 
| 26 |  | inex1g 5318 | . . . . 5
⊢ (Word
𝑆 ∈ V → (Word
𝑆 ∩ (◡♯ “
(ℤ≥‘(♯‘𝑀)))) ∈ V) | 
| 27 | 24, 25, 26 | 3syl 18 | . . . 4
⊢ (𝜑 → (Word 𝑆 ∩ (◡♯ “
(ℤ≥‘(♯‘𝑀)))) ∈ V) | 
| 28 | 23, 27 | eqeltrid 2844 | . . 3
⊢ (𝜑 → 𝑊 ∈ V) | 
| 29 | 22, 28 | fexd 7248 | . 2
⊢ (𝜑 → 𝐹 ∈ V) | 
| 30 |  | df-lsw 14602 | . . . . . 6
⊢ lastS =
(𝑥 ∈ V ↦ (𝑥‘((♯‘𝑥) − 1))) | 
| 31 | 30 | funmpt2 6604 | . . . . 5
⊢ Fun
lastS | 
| 32 | 31 | a1i 11 | . . . 4
⊢ (𝜑 → Fun
lastS) | 
| 33 |  | seqex 14045 | . . . . 5
⊢
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) ∈
V | 
| 34 | 33 | a1i 11 | . . . 4
⊢ (𝜑 → seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) ∈
V) | 
| 35 |  | cofunexg 7974 | . . . 4
⊢ ((Fun
lastS ∧ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})) ∈ V)
→ (lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) ∈
V) | 
| 36 | 32, 34, 35 | syl2anc 584 | . . 3
⊢ (𝜑 → (lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) ∈
V) | 
| 37 |  | unexg 7764 | . . 3
⊢ ((𝑀 ∈ V ∧ (lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))) ∈ V)
→ (𝑀 ∪ (lastS
∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))) ∈
V) | 
| 38 | 21, 36, 37 | syl2anc 584 | . 2
⊢ (𝜑 → (𝑀 ∪ (lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)})))) ∈
V) | 
| 39 | 2, 18, 21, 29, 38 | ovmpod 7586 | 1
⊢ (𝜑 → (𝑀seqstr𝐹) = (𝑀 ∪ (lastS ∘
seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ 〈“(𝐹‘𝑥)”〉)), (ℕ0
× {(𝑀 ++
〈“(𝐹‘𝑀)”〉)}))))) |