| Step | Hyp | Ref
| Expression |
| 1 | | df-splice 14788 |
. . 3
⊢ splice =
(𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1st
‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) ++ (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (♯‘𝑠)〉))) |
| 2 | 1 | a1i 11 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1st
‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) ++ (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (♯‘𝑠)〉)))) |
| 3 | | simprl 771 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → 𝑠 = 𝑆) |
| 4 | | 2fveq3 6911 |
. . . . . . 7
⊢ (𝑏 = 〈𝐹, 𝑇, 𝑅〉 → (1st
‘(1st ‘𝑏)) = (1st ‘(1st
‘〈𝐹, 𝑇, 𝑅〉))) |
| 5 | 4 | adantl 481 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → (1st
‘(1st ‘𝑏)) = (1st ‘(1st
‘〈𝐹, 𝑇, 𝑅〉))) |
| 6 | | ot1stg 8028 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)) = 𝐹) |
| 7 | 6 | adantl 481 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)) = 𝐹) |
| 8 | 5, 7 | sylan9eqr 2799 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → (1st
‘(1st ‘𝑏)) = 𝐹) |
| 9 | 3, 8 | oveq12d 7449 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → (𝑠 prefix (1st
‘(1st ‘𝑏))) = (𝑆 prefix 𝐹)) |
| 10 | | fveq2 6906 |
. . . . . 6
⊢ (𝑏 = 〈𝐹, 𝑇, 𝑅〉 → (2nd ‘𝑏) = (2nd
‘〈𝐹, 𝑇, 𝑅〉)) |
| 11 | 10 | adantl 481 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → (2nd ‘𝑏) = (2nd
‘〈𝐹, 𝑇, 𝑅〉)) |
| 12 | | ot3rdg 8030 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑌 → (2nd ‘〈𝐹, 𝑇, 𝑅〉) = 𝑅) |
| 13 | 12 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (2nd ‘〈𝐹, 𝑇, 𝑅〉) = 𝑅) |
| 14 | 13 | adantl 481 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (2nd ‘〈𝐹, 𝑇, 𝑅〉) = 𝑅) |
| 15 | 11, 14 | sylan9eqr 2799 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → (2nd ‘𝑏) = 𝑅) |
| 16 | 9, 15 | oveq12d 7449 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → ((𝑠 prefix (1st
‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) = ((𝑆 prefix 𝐹) ++ 𝑅)) |
| 17 | | 2fveq3 6911 |
. . . . . . 7
⊢ (𝑏 = 〈𝐹, 𝑇, 𝑅〉 → (2nd
‘(1st ‘𝑏)) = (2nd ‘(1st
‘〈𝐹, 𝑇, 𝑅〉))) |
| 18 | 17 | adantl 481 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → (2nd
‘(1st ‘𝑏)) = (2nd ‘(1st
‘〈𝐹, 𝑇, 𝑅〉))) |
| 19 | | ot2ndg 8029 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)) = 𝑇) |
| 20 | 19 | adantl 481 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)) = 𝑇) |
| 21 | 18, 20 | sylan9eqr 2799 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → (2nd
‘(1st ‘𝑏)) = 𝑇) |
| 22 | 3 | fveq2d 6910 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → (♯‘𝑠) = (♯‘𝑆)) |
| 23 | 21, 22 | opeq12d 4881 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → 〈(2nd
‘(1st ‘𝑏)), (♯‘𝑠)〉 = 〈𝑇, (♯‘𝑆)〉) |
| 24 | 3, 23 | oveq12d 7449 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (♯‘𝑠)〉) = (𝑆 substr 〈𝑇, (♯‘𝑆)〉)) |
| 25 | 16, 24 | oveq12d 7449 |
. 2
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → (((𝑠 prefix (1st
‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) ++ (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (♯‘𝑠)〉)) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) |
| 26 | | elex 3501 |
. . 3
⊢ (𝑆 ∈ 𝑉 → 𝑆 ∈ V) |
| 27 | 26 | adantr 480 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → 𝑆 ∈ V) |
| 28 | | otex 5470 |
. . 3
⊢
〈𝐹, 𝑇, 𝑅〉 ∈ V |
| 29 | 28 | a1i 11 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → 〈𝐹, 𝑇, 𝑅〉 ∈ V) |
| 30 | | ovexd 7466 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉)) ∈ V) |
| 31 | 2, 25, 27, 29, 30 | ovmpod 7585 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) |