Step |
Hyp |
Ref |
Expression |
0 |
|
cefg |
|- ~FG |
1 |
|
vi |
|- i |
2 |
|
cvv |
|- _V |
3 |
|
vr |
|- r |
4 |
3
|
cv |
|- r |
5 |
1
|
cv |
|- i |
6 |
|
c2o |
|- 2o |
7 |
5 6
|
cxp |
|- ( i X. 2o ) |
8 |
7
|
cword |
|- Word ( i X. 2o ) |
9 |
8 4
|
wer |
|- r Er Word ( i X. 2o ) |
10 |
|
vx |
|- x |
11 |
|
vn |
|- n |
12 |
|
cc0 |
|- 0 |
13 |
|
cfz |
|- ... |
14 |
|
chash |
|- # |
15 |
10
|
cv |
|- x |
16 |
15 14
|
cfv |
|- ( # ` x ) |
17 |
12 16 13
|
co |
|- ( 0 ... ( # ` x ) ) |
18 |
|
vy |
|- y |
19 |
|
vz |
|- z |
20 |
|
csplice |
|- splice |
21 |
11
|
cv |
|- n |
22 |
18
|
cv |
|- y |
23 |
19
|
cv |
|- z |
24 |
22 23
|
cop |
|- <. y , z >. |
25 |
|
c1o |
|- 1o |
26 |
25 23
|
cdif |
|- ( 1o \ z ) |
27 |
22 26
|
cop |
|- <. y , ( 1o \ z ) >. |
28 |
24 27
|
cs2 |
|- <" <. y , z >. <. y , ( 1o \ z ) >. "> |
29 |
21 21 28
|
cotp |
|- <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. |
30 |
15 29 20
|
co |
|- ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) |
31 |
15 30 4
|
wbr |
|- x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) |
32 |
31 19 6
|
wral |
|- A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) |
33 |
32 18 5
|
wral |
|- A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) |
34 |
33 11 17
|
wral |
|- A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) |
35 |
34 10 8
|
wral |
|- A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) |
36 |
9 35
|
wa |
|- ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) |
37 |
36 3
|
cab |
|- { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } |
38 |
37
|
cint |
|- |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } |
39 |
1 2 38
|
cmpt |
|- ( i e. _V |-> |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } ) |
40 |
0 39
|
wceq |
|- ~FG = ( i e. _V |-> |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } ) |