Step |
Hyp |
Ref |
Expression |
1 |
|
efgval.w |
⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) ) |
2 |
|
efgval.r |
⊢ ∼ = ( ~FG ‘ 𝐼 ) |
3 |
|
0ex |
⊢ ∅ ∈ V |
4 |
3
|
prid1 |
⊢ ∅ ∈ { ∅ , 1o } |
5 |
|
df2o3 |
⊢ 2o = { ∅ , 1o } |
6 |
4 5
|
eleqtrri |
⊢ ∅ ∈ 2o |
7 |
1 2
|
efgi |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ ( 𝐽 ∈ 𝐼 ∧ ∅ ∈ 2o ) ) → 𝐴 ∼ ( 𝐴 splice 〈 𝑁 , 𝑁 , 〈“ 〈 𝐽 , ∅ 〉 〈 𝐽 , ( 1o ∖ ∅ ) 〉 ”〉 〉 ) ) |
8 |
6 7
|
mpanr2 |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝐽 ∈ 𝐼 ) → 𝐴 ∼ ( 𝐴 splice 〈 𝑁 , 𝑁 , 〈“ 〈 𝐽 , ∅ 〉 〈 𝐽 , ( 1o ∖ ∅ ) 〉 ”〉 〉 ) ) |
9 |
8
|
3impa |
⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝐽 ∈ 𝐼 ) → 𝐴 ∼ ( 𝐴 splice 〈 𝑁 , 𝑁 , 〈“ 〈 𝐽 , ∅ 〉 〈 𝐽 , ( 1o ∖ ∅ ) 〉 ”〉 〉 ) ) |
10 |
|
tru |
⊢ ⊤ |
11 |
|
eqidd |
⊢ ( ⊤ → 〈 𝐽 , ∅ 〉 = 〈 𝐽 , ∅ 〉 ) |
12 |
|
dif0 |
⊢ ( 1o ∖ ∅ ) = 1o |
13 |
12
|
opeq2i |
⊢ 〈 𝐽 , ( 1o ∖ ∅ ) 〉 = 〈 𝐽 , 1o 〉 |
14 |
13
|
a1i |
⊢ ( ⊤ → 〈 𝐽 , ( 1o ∖ ∅ ) 〉 = 〈 𝐽 , 1o 〉 ) |
15 |
11 14
|
s2eqd |
⊢ ( ⊤ → 〈“ 〈 𝐽 , ∅ 〉 〈 𝐽 , ( 1o ∖ ∅ ) 〉 ”〉 = 〈“ 〈 𝐽 , ∅ 〉 〈 𝐽 , 1o 〉 ”〉 ) |
16 |
|
oteq3 |
⊢ ( 〈“ 〈 𝐽 , ∅ 〉 〈 𝐽 , ( 1o ∖ ∅ ) 〉 ”〉 = 〈“ 〈 𝐽 , ∅ 〉 〈 𝐽 , 1o 〉 ”〉 → 〈 𝑁 , 𝑁 , 〈“ 〈 𝐽 , ∅ 〉 〈 𝐽 , ( 1o ∖ ∅ ) 〉 ”〉 〉 = 〈 𝑁 , 𝑁 , 〈“ 〈 𝐽 , ∅ 〉 〈 𝐽 , 1o 〉 ”〉 〉 ) |
17 |
10 15 16
|
mp2b |
⊢ 〈 𝑁 , 𝑁 , 〈“ 〈 𝐽 , ∅ 〉 〈 𝐽 , ( 1o ∖ ∅ ) 〉 ”〉 〉 = 〈 𝑁 , 𝑁 , 〈“ 〈 𝐽 , ∅ 〉 〈 𝐽 , 1o 〉 ”〉 〉 |
18 |
17
|
oveq2i |
⊢ ( 𝐴 splice 〈 𝑁 , 𝑁 , 〈“ 〈 𝐽 , ∅ 〉 〈 𝐽 , ( 1o ∖ ∅ ) 〉 ”〉 〉 ) = ( 𝐴 splice 〈 𝑁 , 𝑁 , 〈“ 〈 𝐽 , ∅ 〉 〈 𝐽 , 1o 〉 ”〉 〉 ) |
19 |
9 18
|
breqtrdi |
⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝐽 ∈ 𝐼 ) → 𝐴 ∼ ( 𝐴 splice 〈 𝑁 , 𝑁 , 〈“ 〈 𝐽 , ∅ 〉 〈 𝐽 , 1o 〉 ”〉 〉 ) ) |