Step | Hyp | Ref
| Expression |
1 | | df-splice 14645 |
. . 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 770 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → 𝑠 = 𝑆) |
4 | | 2fveq3 6852 |
. . . . . . 7
⊢ (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (1st
‘(1st ‘𝑏)) = (1st ‘(1st
‘⟨𝐹, 𝑇, 𝑅⟩))) |
5 | 4 | adantl 483 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (1st
‘(1st ‘𝑏)) = (1st ‘(1st
‘⟨𝐹, 𝑇, 𝑅⟩))) |
6 | | ot1stg 7940 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝐹) |
7 | 6 | adantl 483 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝐹) |
8 | 5, 7 | sylan9eqr 2799 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (1st
‘(1st ‘𝑏)) = 𝐹) |
9 | 3, 8 | oveq12d 7380 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (𝑠 prefix (1st
‘(1st ‘𝑏))) = (𝑆 prefix 𝐹)) |
10 | | fveq2 6847 |
. . . . . 6
⊢ (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (2nd ‘𝑏) = (2nd
‘⟨𝐹, 𝑇, 𝑅⟩)) |
11 | 10 | adantl 483 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (2nd ‘𝑏) = (2nd
‘⟨𝐹, 𝑇, 𝑅⟩)) |
12 | | ot3rdg 7942 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑌 → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅) |
13 | 12 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅) |
14 | 13 | adantl 483 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅) |
15 | 11, 14 | sylan9eqr 2799 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (2nd ‘𝑏) = 𝑅) |
16 | 9, 15 | oveq12d 7380 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → ((𝑠 prefix (1st
‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) = ((𝑆 prefix 𝐹) ++ 𝑅)) |
17 | | 2fveq3 6852 |
. . . . . . 7
⊢ (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (2nd
‘(1st ‘𝑏)) = (2nd ‘(1st
‘⟨𝐹, 𝑇, 𝑅⟩))) |
18 | 17 | adantl 483 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (2nd
‘(1st ‘𝑏)) = (2nd ‘(1st
‘⟨𝐹, 𝑇, 𝑅⟩))) |
19 | | ot2ndg 7941 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (2nd
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝑇) |
20 | 19 | adantl 483 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (2nd
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝑇) |
21 | 18, 20 | sylan9eqr 2799 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (2nd
‘(1st ‘𝑏)) = 𝑇) |
22 | 3 | fveq2d 6851 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (♯‘𝑠) = (♯‘𝑆)) |
23 | 21, 22 | opeq12d 4843 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → ⟨(2nd
‘(1st ‘𝑏)), (♯‘𝑠)⟩ = ⟨𝑇, (♯‘𝑆)⟩) |
24 | 3, 23 | oveq12d 7380 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (𝑠 substr ⟨(2nd
‘(1st ‘𝑏)), (♯‘𝑠)⟩) = (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)) |
25 | 16, 24 | oveq12d 7380 |
. 2
⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (((𝑠 prefix (1st
‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd
‘(1st ‘𝑏)), (♯‘𝑠)⟩)) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))) |
26 | | elex 3466 |
. . 3
⊢ (𝑆 ∈ 𝑉 → 𝑆 ∈ V) |
27 | 26 | adantr 482 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → 𝑆 ∈ V) |
28 | | otex 5427 |
. . 3
⊢
⟨𝐹, 𝑇, 𝑅⟩ ∈ V |
29 | 28 | a1i 11 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → ⟨𝐹, 𝑇, 𝑅⟩ ∈ V) |
30 | | ovexd 7397 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)) ∈ V) |
31 | 2, 25, 27, 29, 30 | ovmpod 7512 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))) |