Step |
Hyp |
Ref |
Expression |
0 |
|
cefg |
⊢ ~FG |
1 |
|
vi |
⊢ 𝑖 |
2 |
|
cvv |
⊢ V |
3 |
|
vr |
⊢ 𝑟 |
4 |
3
|
cv |
⊢ 𝑟 |
5 |
1
|
cv |
⊢ 𝑖 |
6 |
|
c2o |
⊢ 2o |
7 |
5 6
|
cxp |
⊢ ( 𝑖 × 2o ) |
8 |
7
|
cword |
⊢ Word ( 𝑖 × 2o ) |
9 |
8 4
|
wer |
⊢ 𝑟 Er Word ( 𝑖 × 2o ) |
10 |
|
vx |
⊢ 𝑥 |
11 |
|
vn |
⊢ 𝑛 |
12 |
|
cc0 |
⊢ 0 |
13 |
|
cfz |
⊢ ... |
14 |
|
chash |
⊢ ♯ |
15 |
10
|
cv |
⊢ 𝑥 |
16 |
15 14
|
cfv |
⊢ ( ♯ ‘ 𝑥 ) |
17 |
12 16 13
|
co |
⊢ ( 0 ... ( ♯ ‘ 𝑥 ) ) |
18 |
|
vy |
⊢ 𝑦 |
19 |
|
vz |
⊢ 𝑧 |
20 |
|
csplice |
⊢ splice |
21 |
11
|
cv |
⊢ 𝑛 |
22 |
18
|
cv |
⊢ 𝑦 |
23 |
19
|
cv |
⊢ 𝑧 |
24 |
22 23
|
cop |
⊢ 〈 𝑦 , 𝑧 〉 |
25 |
|
c1o |
⊢ 1o |
26 |
25 23
|
cdif |
⊢ ( 1o ∖ 𝑧 ) |
27 |
22 26
|
cop |
⊢ 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 |
28 |
24 27
|
cs2 |
⊢ 〈“ 〈 𝑦 , 𝑧 〉 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ”〉 |
29 |
21 21 28
|
cotp |
⊢ 〈 𝑛 , 𝑛 , 〈“ 〈 𝑦 , 𝑧 〉 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ”〉 〉 |
30 |
15 29 20
|
co |
⊢ ( 𝑥 splice 〈 𝑛 , 𝑛 , 〈“ 〈 𝑦 , 𝑧 〉 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ”〉 〉 ) |
31 |
15 30 4
|
wbr |
⊢ 𝑥 𝑟 ( 𝑥 splice 〈 𝑛 , 𝑛 , 〈“ 〈 𝑦 , 𝑧 〉 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ”〉 〉 ) |
32 |
31 19 6
|
wral |
⊢ ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice 〈 𝑛 , 𝑛 , 〈“ 〈 𝑦 , 𝑧 〉 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ”〉 〉 ) |
33 |
32 18 5
|
wral |
⊢ ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice 〈 𝑛 , 𝑛 , 〈“ 〈 𝑦 , 𝑧 〉 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ”〉 〉 ) |
34 |
33 11 17
|
wral |
⊢ ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice 〈 𝑛 , 𝑛 , 〈“ 〈 𝑦 , 𝑧 〉 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ”〉 〉 ) |
35 |
34 10 8
|
wral |
⊢ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice 〈 𝑛 , 𝑛 , 〈“ 〈 𝑦 , 𝑧 〉 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ”〉 〉 ) |
36 |
9 35
|
wa |
⊢ ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice 〈 𝑛 , 𝑛 , 〈“ 〈 𝑦 , 𝑧 〉 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ”〉 〉 ) ) |
37 |
36 3
|
cab |
⊢ { 𝑟 ∣ ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice 〈 𝑛 , 𝑛 , 〈“ 〈 𝑦 , 𝑧 〉 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ”〉 〉 ) ) } |
38 |
37
|
cint |
⊢ ∩ { 𝑟 ∣ ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice 〈 𝑛 , 𝑛 , 〈“ 〈 𝑦 , 𝑧 〉 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ”〉 〉 ) ) } |
39 |
1 2 38
|
cmpt |
⊢ ( 𝑖 ∈ V ↦ ∩ { 𝑟 ∣ ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice 〈 𝑛 , 𝑛 , 〈“ 〈 𝑦 , 𝑧 〉 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ”〉 〉 ) ) } ) |
40 |
0 39
|
wceq |
⊢ ~FG = ( 𝑖 ∈ V ↦ ∩ { 𝑟 ∣ ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦 ∈ 𝑖 ∀ 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice 〈 𝑛 , 𝑛 , 〈“ 〈 𝑦 , 𝑧 〉 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ”〉 〉 ) ) } ) |