Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
|- ( a = (/) -> ( ( M Sat E ) ` a ) = ( ( M Sat E ) ` (/) ) ) |
2 |
1
|
rneqd |
|- ( a = (/) -> ran ( ( M Sat E ) ` a ) = ran ( ( M Sat E ) ` (/) ) ) |
3 |
2
|
eleq2d |
|- ( a = (/) -> ( n e. ran ( ( M Sat E ) ` a ) <-> n e. ran ( ( M Sat E ) ` (/) ) ) ) |
4 |
3
|
imbi1d |
|- ( a = (/) -> ( ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) <-> ( n e. ran ( ( M Sat E ) ` (/) ) -> n e. ~P ( M ^m _om ) ) ) ) |
5 |
4
|
imbi2d |
|- ( a = (/) -> ( ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) ) <-> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` (/) ) -> n e. ~P ( M ^m _om ) ) ) ) ) |
6 |
|
fveq2 |
|- ( a = b -> ( ( M Sat E ) ` a ) = ( ( M Sat E ) ` b ) ) |
7 |
6
|
rneqd |
|- ( a = b -> ran ( ( M Sat E ) ` a ) = ran ( ( M Sat E ) ` b ) ) |
8 |
7
|
eleq2d |
|- ( a = b -> ( n e. ran ( ( M Sat E ) ` a ) <-> n e. ran ( ( M Sat E ) ` b ) ) ) |
9 |
8
|
imbi1d |
|- ( a = b -> ( ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) <-> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) |
10 |
9
|
imbi2d |
|- ( a = b -> ( ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) ) <-> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) ) |
11 |
|
fveq2 |
|- ( a = suc b -> ( ( M Sat E ) ` a ) = ( ( M Sat E ) ` suc b ) ) |
12 |
11
|
rneqd |
|- ( a = suc b -> ran ( ( M Sat E ) ` a ) = ran ( ( M Sat E ) ` suc b ) ) |
13 |
12
|
eleq2d |
|- ( a = suc b -> ( n e. ran ( ( M Sat E ) ` a ) <-> n e. ran ( ( M Sat E ) ` suc b ) ) ) |
14 |
13
|
imbi1d |
|- ( a = suc b -> ( ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) <-> ( n e. ran ( ( M Sat E ) ` suc b ) -> n e. ~P ( M ^m _om ) ) ) ) |
15 |
14
|
imbi2d |
|- ( a = suc b -> ( ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) ) <-> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` suc b ) -> n e. ~P ( M ^m _om ) ) ) ) ) |
16 |
|
fveq2 |
|- ( a = N -> ( ( M Sat E ) ` a ) = ( ( M Sat E ) ` N ) ) |
17 |
16
|
rneqd |
|- ( a = N -> ran ( ( M Sat E ) ` a ) = ran ( ( M Sat E ) ` N ) ) |
18 |
17
|
eleq2d |
|- ( a = N -> ( n e. ran ( ( M Sat E ) ` a ) <-> n e. ran ( ( M Sat E ) ` N ) ) ) |
19 |
18
|
imbi1d |
|- ( a = N -> ( ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) <-> ( n e. ran ( ( M Sat E ) ` N ) -> n e. ~P ( M ^m _om ) ) ) ) |
20 |
19
|
imbi2d |
|- ( a = N -> ( ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) ) <-> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` N ) -> n e. ~P ( M ^m _om ) ) ) ) ) |
21 |
|
eqid |
|- ( M Sat E ) = ( M Sat E ) |
22 |
21
|
satfv0 |
|- ( ( M e. V /\ E e. W ) -> ( ( M Sat E ) ` (/) ) = { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } ) |
23 |
22
|
rneqd |
|- ( ( M e. V /\ E e. W ) -> ran ( ( M Sat E ) ` (/) ) = ran { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } ) |
24 |
23
|
eleq2d |
|- ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` (/) ) <-> n e. ran { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } ) ) |
25 |
|
rnopab |
|- ran { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } = { y | E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } |
26 |
25
|
eleq2i |
|- ( n e. ran { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } <-> n e. { y | E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } ) |
27 |
|
vex |
|- n e. _V |
28 |
|
eqeq1 |
|- ( y = n -> ( y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } <-> n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) ) |
29 |
28
|
anbi2d |
|- ( y = n -> ( ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) <-> ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) ) ) |
30 |
29
|
2rexbidv |
|- ( y = n -> ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) <-> E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) ) ) |
31 |
30
|
exbidv |
|- ( y = n -> ( E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) <-> E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) ) ) |
32 |
27 31
|
elab |
|- ( n e. { y | E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } <-> E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) ) |
33 |
|
ovex |
|- ( M ^m _om ) e. _V |
34 |
|
ssrab2 |
|- { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } C_ ( M ^m _om ) |
35 |
33 34
|
elpwi2 |
|- { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } e. ~P ( M ^m _om ) |
36 |
|
eleq1 |
|- ( n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } -> ( n e. ~P ( M ^m _om ) <-> { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } e. ~P ( M ^m _om ) ) ) |
37 |
35 36
|
mpbiri |
|- ( n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } -> n e. ~P ( M ^m _om ) ) |
38 |
37
|
adantl |
|- ( ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> n e. ~P ( M ^m _om ) ) |
39 |
38
|
a1i |
|- ( ( i e. _om /\ j e. _om ) -> ( ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> n e. ~P ( M ^m _om ) ) ) |
40 |
39
|
rexlimivv |
|- ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> n e. ~P ( M ^m _om ) ) |
41 |
40
|
exlimiv |
|- ( E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> n e. ~P ( M ^m _om ) ) |
42 |
32 41
|
sylbi |
|- ( n e. { y | E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } -> n e. ~P ( M ^m _om ) ) |
43 |
42
|
a1i |
|- ( ( M e. V /\ E e. W ) -> ( n e. { y | E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } -> n e. ~P ( M ^m _om ) ) ) |
44 |
26 43
|
syl5bi |
|- ( ( M e. V /\ E e. W ) -> ( n e. ran { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } -> n e. ~P ( M ^m _om ) ) ) |
45 |
24 44
|
sylbid |
|- ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` (/) ) -> n e. ~P ( M ^m _om ) ) ) |
46 |
21
|
satfvsuc |
|- ( ( M e. V /\ E e. W /\ b e. _om ) -> ( ( M Sat E ) ` suc b ) = ( ( ( M Sat E ) ` b ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) |
47 |
46
|
3expa |
|- ( ( ( M e. V /\ E e. W ) /\ b e. _om ) -> ( ( M Sat E ) ` suc b ) = ( ( ( M Sat E ) ` b ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) |
48 |
47
|
rneqd |
|- ( ( ( M e. V /\ E e. W ) /\ b e. _om ) -> ran ( ( M Sat E ) ` suc b ) = ran ( ( ( M Sat E ) ` b ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) |
49 |
|
rnun |
|- ran ( ( ( M Sat E ) ` b ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) = ( ran ( ( M Sat E ) ` b ) u. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) |
50 |
48 49
|
eqtrdi |
|- ( ( ( M e. V /\ E e. W ) /\ b e. _om ) -> ran ( ( M Sat E ) ` suc b ) = ( ran ( ( M Sat E ) ` b ) u. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) |
51 |
50
|
eleq2d |
|- ( ( ( M e. V /\ E e. W ) /\ b e. _om ) -> ( n e. ran ( ( M Sat E ) ` suc b ) <-> n e. ( ran ( ( M Sat E ) ` b ) u. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) ) |
52 |
|
elun |
|- ( n e. ( ran ( ( M Sat E ) ` b ) u. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> ( n e. ran ( ( M Sat E ) ` b ) \/ n e. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) |
53 |
|
rnopab |
|- ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } = { y | E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } |
54 |
53
|
eleq2i |
|- ( n e. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } <-> n e. { y | E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) |
55 |
|
eqeq1 |
|- ( y = n -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) <-> n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) |
56 |
55
|
anbi2d |
|- ( y = n -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) ) |
57 |
56
|
rexbidv |
|- ( y = n -> ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) ) |
58 |
|
eqeq1 |
|- ( y = n -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } <-> n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) |
59 |
58
|
anbi2d |
|- ( y = n -> ( ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) |
60 |
59
|
rexbidv |
|- ( y = n -> ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) |
61 |
57 60
|
orbi12d |
|- ( y = n -> ( ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) |
62 |
61
|
rexbidv |
|- ( y = n -> ( E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) |
63 |
62
|
exbidv |
|- ( y = n -> ( E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) |
64 |
27 63
|
elab |
|- ( n e. { y | E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } <-> E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) |
65 |
54 64
|
bitri |
|- ( n e. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } <-> E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) |
66 |
65
|
orbi2i |
|- ( ( n e. ran ( ( M Sat E ) ` b ) \/ n e. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> ( n e. ran ( ( M Sat E ) ` b ) \/ E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) |
67 |
52 66
|
bitri |
|- ( n e. ( ran ( ( M Sat E ) ` b ) u. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> ( n e. ran ( ( M Sat E ) ` b ) \/ E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) |
68 |
51 67
|
bitrdi |
|- ( ( ( M e. V /\ E e. W ) /\ b e. _om ) -> ( n e. ran ( ( M Sat E ) ` suc b ) <-> ( n e. ran ( ( M Sat E ) ` b ) \/ E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) ) |
69 |
68
|
expcom |
|- ( b e. _om -> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` suc b ) <-> ( n e. ran ( ( M Sat E ) ` b ) \/ E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) ) ) |
70 |
69
|
adantr |
|- ( ( b e. _om /\ ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) -> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` suc b ) <-> ( n e. ran ( ( M Sat E ) ` b ) \/ E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) ) ) |
71 |
70
|
imp |
|- ( ( ( b e. _om /\ ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) /\ ( M e. V /\ E e. W ) ) -> ( n e. ran ( ( M Sat E ) ` suc b ) <-> ( n e. ran ( ( M Sat E ) ` b ) \/ E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) ) |
72 |
|
simpr |
|- ( ( b e. _om /\ ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) -> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) |
73 |
72
|
imp |
|- ( ( ( b e. _om /\ ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) /\ ( M e. V /\ E e. W ) ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) |
74 |
|
difss |
|- ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) C_ ( M ^m _om ) |
75 |
33 74
|
elpwi2 |
|- ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) e. ~P ( M ^m _om ) |
76 |
|
eleq1 |
|- ( n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) -> ( n e. ~P ( M ^m _om ) <-> ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) e. ~P ( M ^m _om ) ) ) |
77 |
75 76
|
mpbiri |
|- ( n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) -> n e. ~P ( M ^m _om ) ) |
78 |
77
|
adantl |
|- ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> n e. ~P ( M ^m _om ) ) |
79 |
78
|
adantl |
|- ( ( v e. ( ( M Sat E ) ` b ) /\ ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) -> n e. ~P ( M ^m _om ) ) |
80 |
79
|
rexlimiva |
|- ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> n e. ~P ( M ^m _om ) ) |
81 |
|
ssrab2 |
|- { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } C_ ( M ^m _om ) |
82 |
33 81
|
elpwi2 |
|- { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } e. ~P ( M ^m _om ) |
83 |
|
eleq1 |
|- ( n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> ( n e. ~P ( M ^m _om ) <-> { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } e. ~P ( M ^m _om ) ) ) |
84 |
82 83
|
mpbiri |
|- ( n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> n e. ~P ( M ^m _om ) ) |
85 |
84
|
adantl |
|- ( ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) -> n e. ~P ( M ^m _om ) ) |
86 |
85
|
a1i |
|- ( i e. _om -> ( ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) -> n e. ~P ( M ^m _om ) ) ) |
87 |
86
|
rexlimiv |
|- ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) -> n e. ~P ( M ^m _om ) ) |
88 |
80 87
|
jaoi |
|- ( ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> n e. ~P ( M ^m _om ) ) |
89 |
88
|
a1i |
|- ( u e. ( ( M Sat E ) ` b ) -> ( ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> n e. ~P ( M ^m _om ) ) ) |
90 |
89
|
rexlimiv |
|- ( E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> n e. ~P ( M ^m _om ) ) |
91 |
90
|
exlimiv |
|- ( E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> n e. ~P ( M ^m _om ) ) |
92 |
91
|
a1i |
|- ( ( ( b e. _om /\ ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) /\ ( M e. V /\ E e. W ) ) -> ( E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> n e. ~P ( M ^m _om ) ) ) |
93 |
73 92
|
jaod |
|- ( ( ( b e. _om /\ ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) /\ ( M e. V /\ E e. W ) ) -> ( ( n e. ran ( ( M Sat E ) ` b ) \/ E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) -> n e. ~P ( M ^m _om ) ) ) |
94 |
71 93
|
sylbid |
|- ( ( ( b e. _om /\ ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) /\ ( M e. V /\ E e. W ) ) -> ( n e. ran ( ( M Sat E ) ` suc b ) -> n e. ~P ( M ^m _om ) ) ) |
95 |
94
|
exp31 |
|- ( b e. _om -> ( ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) -> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` suc b ) -> n e. ~P ( M ^m _om ) ) ) ) ) |
96 |
5 10 15 20 45 95
|
finds |
|- ( N e. _om -> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` N ) -> n e. ~P ( M ^m _om ) ) ) ) |
97 |
96
|
com12 |
|- ( ( M e. V /\ E e. W ) -> ( N e. _om -> ( n e. ran ( ( M Sat E ) ` N ) -> n e. ~P ( M ^m _om ) ) ) ) |
98 |
97
|
3impia |
|- ( ( M e. V /\ E e. W /\ N e. _om ) -> ( n e. ran ( ( M Sat E ) ` N ) -> n e. ~P ( M ^m _om ) ) ) |
99 |
98
|
ssrdv |
|- ( ( M e. V /\ E e. W /\ N e. _om ) -> ran ( ( M Sat E ) ` N ) C_ ~P ( M ^m _om ) ) |