Step | Hyp | Ref
| Expression |
1 | | df-splice 13159 |
. . 3
⊢ splice =
(𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr 〈0, (1st
‘(1st ‘𝑏))〉) ++ (2nd ‘𝑏)) ++ (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (#‘𝑠)〉))) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr 〈0, (1st
‘(1st ‘𝑏))〉) ++ (2nd ‘𝑏)) ++ (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (#‘𝑠)〉)))) |
3 | | simprl 790 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → 𝑠 = 𝑆) |
4 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑏 = 〈𝐹, 𝑇, 𝑅〉 → (1st ‘𝑏) = (1st
‘〈𝐹, 𝑇, 𝑅〉)) |
5 | 4 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑏 = 〈𝐹, 𝑇, 𝑅〉 → (1st
‘(1st ‘𝑏)) = (1st ‘(1st
‘〈𝐹, 𝑇, 𝑅〉))) |
6 | 5 | adantl 481 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → (1st
‘(1st ‘𝑏)) = (1st ‘(1st
‘〈𝐹, 𝑇, 𝑅〉))) |
7 | | ot1stg 7073 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)) = 𝐹) |
8 | 7 | adantl 481 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)) = 𝐹) |
9 | 6, 8 | sylan9eqr 2666 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → (1st
‘(1st ‘𝑏)) = 𝐹) |
10 | 9 | opeq2d 4347 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → 〈0, (1st
‘(1st ‘𝑏))〉 = 〈0, 𝐹〉) |
11 | 3, 10 | oveq12d 6567 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → (𝑠 substr 〈0, (1st
‘(1st ‘𝑏))〉) = (𝑆 substr 〈0, 𝐹〉)) |
12 | | fveq2 6103 |
. . . . . 6
⊢ (𝑏 = 〈𝐹, 𝑇, 𝑅〉 → (2nd ‘𝑏) = (2nd
‘〈𝐹, 𝑇, 𝑅〉)) |
13 | 12 | adantl 481 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → (2nd ‘𝑏) = (2nd
‘〈𝐹, 𝑇, 𝑅〉)) |
14 | | ot3rdg 7075 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑌 → (2nd ‘〈𝐹, 𝑇, 𝑅〉) = 𝑅) |
15 | 14 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (2nd ‘〈𝐹, 𝑇, 𝑅〉) = 𝑅) |
16 | 15 | adantl 481 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (2nd ‘〈𝐹, 𝑇, 𝑅〉) = 𝑅) |
17 | 13, 16 | sylan9eqr 2666 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → (2nd ‘𝑏) = 𝑅) |
18 | 11, 17 | oveq12d 6567 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → ((𝑠 substr 〈0, (1st
‘(1st ‘𝑏))〉) ++ (2nd ‘𝑏)) = ((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)) |
19 | 4 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑏 = 〈𝐹, 𝑇, 𝑅〉 → (2nd
‘(1st ‘𝑏)) = (2nd ‘(1st
‘〈𝐹, 𝑇, 𝑅〉))) |
20 | 19 | adantl 481 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → (2nd
‘(1st ‘𝑏)) = (2nd ‘(1st
‘〈𝐹, 𝑇, 𝑅〉))) |
21 | | ot2ndg 7074 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)) = 𝑇) |
22 | 21 | adantl 481 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)) = 𝑇) |
23 | 20, 22 | sylan9eqr 2666 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → (2nd
‘(1st ‘𝑏)) = 𝑇) |
24 | 3 | fveq2d 6107 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → (#‘𝑠) = (#‘𝑆)) |
25 | 23, 24 | opeq12d 4348 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → 〈(2nd
‘(1st ‘𝑏)), (#‘𝑠)〉 = 〈𝑇, (#‘𝑆)〉) |
26 | 3, 25 | oveq12d 6567 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (#‘𝑠)〉) = (𝑆 substr 〈𝑇, (#‘𝑆)〉)) |
27 | 18, 26 | oveq12d 6567 |
. 2
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉)) → (((𝑠 substr 〈0, (1st
‘(1st ‘𝑏))〉) ++ (2nd ‘𝑏)) ++ (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (#‘𝑠)〉)) = (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))) |
28 | | elex 3185 |
. . 3
⊢ (𝑆 ∈ 𝑉 → 𝑆 ∈ V) |
29 | 28 | adantr 480 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → 𝑆 ∈ V) |
30 | | otex 4860 |
. . 3
⊢
〈𝐹, 𝑇, 𝑅〉 ∈ V |
31 | 30 | a1i 11 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → 〈𝐹, 𝑇, 𝑅〉 ∈ V) |
32 | | ovex 6577 |
. . 3
⊢ (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉)) ∈ V |
33 | 32 | a1i 11 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉)) ∈ V) |
34 | 2, 27, 29, 31, 33 | ovmpt2d 6686 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))) |