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 |
|
efgrelexlem.1 |
|- L = { <. i , j >. | E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) } |
8 |
7
|
bropaex12 |
|- ( A L B -> ( A e. _V /\ B e. _V ) ) |
9 |
|
n0i |
|- ( a e. ( `' S " { A } ) -> -. ( `' S " { A } ) = (/) ) |
10 |
|
snprc |
|- ( -. A e. _V <-> { A } = (/) ) |
11 |
|
imaeq2 |
|- ( { A } = (/) -> ( `' S " { A } ) = ( `' S " (/) ) ) |
12 |
10 11
|
sylbi |
|- ( -. A e. _V -> ( `' S " { A } ) = ( `' S " (/) ) ) |
13 |
|
ima0 |
|- ( `' S " (/) ) = (/) |
14 |
12 13
|
eqtrdi |
|- ( -. A e. _V -> ( `' S " { A } ) = (/) ) |
15 |
9 14
|
nsyl2 |
|- ( a e. ( `' S " { A } ) -> A e. _V ) |
16 |
|
n0i |
|- ( b e. ( `' S " { B } ) -> -. ( `' S " { B } ) = (/) ) |
17 |
|
snprc |
|- ( -. B e. _V <-> { B } = (/) ) |
18 |
|
imaeq2 |
|- ( { B } = (/) -> ( `' S " { B } ) = ( `' S " (/) ) ) |
19 |
17 18
|
sylbi |
|- ( -. B e. _V -> ( `' S " { B } ) = ( `' S " (/) ) ) |
20 |
19 13
|
eqtrdi |
|- ( -. B e. _V -> ( `' S " { B } ) = (/) ) |
21 |
16 20
|
nsyl2 |
|- ( b e. ( `' S " { B } ) -> B e. _V ) |
22 |
15 21
|
anim12i |
|- ( ( a e. ( `' S " { A } ) /\ b e. ( `' S " { B } ) ) -> ( A e. _V /\ B e. _V ) ) |
23 |
22
|
a1d |
|- ( ( a e. ( `' S " { A } ) /\ b e. ( `' S " { B } ) ) -> ( ( a ` 0 ) = ( b ` 0 ) -> ( A e. _V /\ B e. _V ) ) ) |
24 |
23
|
rexlimivv |
|- ( E. a e. ( `' S " { A } ) E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) -> ( A e. _V /\ B e. _V ) ) |
25 |
|
fveq1 |
|- ( c = a -> ( c ` 0 ) = ( a ` 0 ) ) |
26 |
25
|
eqeq1d |
|- ( c = a -> ( ( c ` 0 ) = ( d ` 0 ) <-> ( a ` 0 ) = ( d ` 0 ) ) ) |
27 |
|
fveq1 |
|- ( d = b -> ( d ` 0 ) = ( b ` 0 ) ) |
28 |
27
|
eqeq2d |
|- ( d = b -> ( ( a ` 0 ) = ( d ` 0 ) <-> ( a ` 0 ) = ( b ` 0 ) ) ) |
29 |
26 28
|
cbvrex2vw |
|- ( E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) <-> E. a e. ( `' S " { i } ) E. b e. ( `' S " { j } ) ( a ` 0 ) = ( b ` 0 ) ) |
30 |
|
sneq |
|- ( i = A -> { i } = { A } ) |
31 |
30
|
imaeq2d |
|- ( i = A -> ( `' S " { i } ) = ( `' S " { A } ) ) |
32 |
31
|
rexeqdv |
|- ( i = A -> ( E. a e. ( `' S " { i } ) E. b e. ( `' S " { j } ) ( a ` 0 ) = ( b ` 0 ) <-> E. a e. ( `' S " { A } ) E. b e. ( `' S " { j } ) ( a ` 0 ) = ( b ` 0 ) ) ) |
33 |
29 32
|
syl5bb |
|- ( i = A -> ( E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) <-> E. a e. ( `' S " { A } ) E. b e. ( `' S " { j } ) ( a ` 0 ) = ( b ` 0 ) ) ) |
34 |
|
sneq |
|- ( j = B -> { j } = { B } ) |
35 |
34
|
imaeq2d |
|- ( j = B -> ( `' S " { j } ) = ( `' S " { B } ) ) |
36 |
35
|
rexeqdv |
|- ( j = B -> ( E. b e. ( `' S " { j } ) ( a ` 0 ) = ( b ` 0 ) <-> E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) ) ) |
37 |
36
|
rexbidv |
|- ( j = B -> ( E. a e. ( `' S " { A } ) E. b e. ( `' S " { j } ) ( a ` 0 ) = ( b ` 0 ) <-> E. a e. ( `' S " { A } ) E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) ) ) |
38 |
33 37 7
|
brabg |
|- ( ( A e. _V /\ B e. _V ) -> ( A L B <-> E. a e. ( `' S " { A } ) E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) ) ) |
39 |
8 24 38
|
pm5.21nii |
|- ( A L B <-> E. a e. ( `' S " { A } ) E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) ) |