| Step |
Hyp |
Ref |
Expression |
| 1 |
|
efgval.w |
|- W = ( _I ` Word ( I X. 2o ) ) |
| 2 |
|
efgval.r |
|- .~ = ( ~FG ` I ) |
| 3 |
|
efgval2.m |
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) |
| 4 |
|
efgval2.t |
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) ) |
| 5 |
|
efgred.d |
|- D = ( W \ U_ x e. W ran ( T ` x ) ) |
| 6 |
|
efgred.s |
|- S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) ) |
| 7 |
|
eqid |
|- { <. i , j >. | E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) } = { <. i , j >. | E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) } |
| 8 |
1 2 3 4 5 6 7
|
efgrelexlemb |
|- .~ C_ { <. i , j >. | E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) } |
| 9 |
8
|
ssbri |
|- ( A .~ B -> A { <. i , j >. | E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) } B ) |
| 10 |
1 2 3 4 5 6 7
|
efgrelexlema |
|- ( A { <. i , j >. | E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) } B <-> E. a e. ( `' S " { A } ) E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) ) |
| 11 |
9 10
|
sylib |
|- ( A .~ B -> E. a e. ( `' S " { A } ) E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) ) |