Step |
Hyp |
Ref |
Expression |
1 |
|
0ex |
|- (/) e. _V |
2 |
|
satf |
|- ( ( (/) e. _V /\ (/) e. _V ) -> ( (/) Sat (/) ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) , { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) } ) |` suc _om ) ) |
3 |
1 1 2
|
mp2an |
|- ( (/) Sat (/) ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) , { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) } ) |` suc _om ) |
4 |
|
peano1 |
|- (/) e. _om |
5 |
4
|
ne0ii |
|- _om =/= (/) |
6 |
|
map0b |
|- ( _om =/= (/) -> ( (/) ^m _om ) = (/) ) |
7 |
5 6
|
ax-mp |
|- ( (/) ^m _om ) = (/) |
8 |
7
|
difeq1i |
|- ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) = ( (/) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) |
9 |
|
0dif |
|- ( (/) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) = (/) |
10 |
8 9
|
eqtri |
|- ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) = (/) |
11 |
10
|
eqeq2i |
|- ( y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) <-> y = (/) ) |
12 |
11
|
anbi2i |
|- ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) ) |
13 |
12
|
rexbii |
|- ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) ) |
14 |
|
r19.41v |
|- ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) <-> ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) ) |
15 |
13 14
|
bitri |
|- ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) ) |
16 |
7
|
rabeqi |
|- { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } = { a e. (/) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } |
17 |
|
rab0 |
|- { a e. (/) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } = (/) |
18 |
16 17
|
eqtri |
|- { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } = (/) |
19 |
18
|
eqeq2i |
|- ( y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } <-> y = (/) ) |
20 |
19
|
anbi2i |
|- ( ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> ( x = A.g i ( 1st ` u ) /\ y = (/) ) ) |
21 |
20
|
rexbii |
|- ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = (/) ) ) |
22 |
|
r19.41v |
|- ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = (/) ) <-> ( E. i e. _om x = A.g i ( 1st ` u ) /\ y = (/) ) ) |
23 |
21 22
|
bitri |
|- ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> ( E. i e. _om x = A.g i ( 1st ` u ) /\ y = (/) ) ) |
24 |
15 23
|
orbi12i |
|- ( ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) \/ ( E. i e. _om x = A.g i ( 1st ` u ) /\ y = (/) ) ) ) |
25 |
24
|
rexbii |
|- ( E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> E. u e. f ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) \/ ( E. i e. _om x = A.g i ( 1st ` u ) /\ y = (/) ) ) ) |
26 |
|
andir |
|- ( ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) /\ y = (/) ) <-> ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) \/ ( E. i e. _om x = A.g i ( 1st ` u ) /\ y = (/) ) ) ) |
27 |
26
|
bicomi |
|- ( ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) \/ ( E. i e. _om x = A.g i ( 1st ` u ) /\ y = (/) ) ) <-> ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) /\ y = (/) ) ) |
28 |
27
|
rexbii |
|- ( E. u e. f ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = (/) ) \/ ( E. i e. _om x = A.g i ( 1st ` u ) /\ y = (/) ) ) <-> E. u e. f ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) /\ y = (/) ) ) |
29 |
|
r19.41v |
|- ( E. u e. f ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) /\ y = (/) ) <-> ( E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) /\ y = (/) ) ) |
30 |
25 28 29
|
3bitri |
|- ( E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) /\ y = (/) ) ) |
31 |
30
|
biancomi |
|- ( E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) |
32 |
31
|
opabbii |
|- { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } = { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } |
33 |
32
|
uneq2i |
|- ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) = ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) |
34 |
33
|
mpteq2i |
|- ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) = ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) |
35 |
7
|
rabeqi |
|- { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } = { a e. (/) | ( a ` i ) (/) ( a ` j ) } |
36 |
|
rab0 |
|- { a e. (/) | ( a ` i ) (/) ( a ` j ) } = (/) |
37 |
35 36
|
eqtri |
|- { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } = (/) |
38 |
37
|
eqeq2i |
|- ( y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } <-> y = (/) ) |
39 |
38
|
anbi2i |
|- ( ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) <-> ( x = ( i e.g j ) /\ y = (/) ) ) |
40 |
39
|
2rexbii |
|- ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) <-> E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = (/) ) ) |
41 |
|
r19.41vv |
|- ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = (/) ) <-> ( E. i e. _om E. j e. _om x = ( i e.g j ) /\ y = (/) ) ) |
42 |
40 41
|
bitri |
|- ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) <-> ( E. i e. _om E. j e. _om x = ( i e.g j ) /\ y = (/) ) ) |
43 |
42
|
biancomi |
|- ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) <-> ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) ) |
44 |
43
|
opabbii |
|- { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) } = { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } |
45 |
|
rdgeq12 |
|- ( ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) = ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) /\ { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) } = { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) -> rec ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) , { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) } ) = rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ) |
46 |
34 44 45
|
mp2an |
|- rec ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) , { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) } ) = rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) |
47 |
46
|
reseq1i |
|- ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | E. u e. f ( E. v e. f ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( (/) ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( (/) ^m _om ) | A. z e. (/) ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) , { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( (/) ^m _om ) | ( a ` i ) (/) ( a ` j ) } ) } ) |` suc _om ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) |` suc _om ) |
48 |
3 47
|
eqtri |
|- ( (/) Sat (/) ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) |` suc _om ) |