Step |
Hyp |
Ref |
Expression |
1 |
|
satfsschain.s |
|- S = ( M Sat E ) |
2 |
|
fveq2 |
|- ( b = B -> ( S ` b ) = ( S ` B ) ) |
3 |
2
|
sseq2d |
|- ( b = B -> ( ( S ` B ) C_ ( S ` b ) <-> ( S ` B ) C_ ( S ` B ) ) ) |
4 |
3
|
imbi2d |
|- ( b = B -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` b ) ) <-> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` B ) ) ) ) |
5 |
|
fveq2 |
|- ( b = a -> ( S ` b ) = ( S ` a ) ) |
6 |
5
|
sseq2d |
|- ( b = a -> ( ( S ` B ) C_ ( S ` b ) <-> ( S ` B ) C_ ( S ` a ) ) ) |
7 |
6
|
imbi2d |
|- ( b = a -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` b ) ) <-> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` a ) ) ) ) |
8 |
|
fveq2 |
|- ( b = suc a -> ( S ` b ) = ( S ` suc a ) ) |
9 |
8
|
sseq2d |
|- ( b = suc a -> ( ( S ` B ) C_ ( S ` b ) <-> ( S ` B ) C_ ( S ` suc a ) ) ) |
10 |
9
|
imbi2d |
|- ( b = suc a -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` b ) ) <-> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` suc a ) ) ) ) |
11 |
|
fveq2 |
|- ( b = A -> ( S ` b ) = ( S ` A ) ) |
12 |
11
|
sseq2d |
|- ( b = A -> ( ( S ` B ) C_ ( S ` b ) <-> ( S ` B ) C_ ( S ` A ) ) ) |
13 |
12
|
imbi2d |
|- ( b = A -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` b ) ) <-> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` A ) ) ) ) |
14 |
|
ssidd |
|- ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` B ) ) |
15 |
14
|
a1i |
|- ( B e. _om -> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` B ) ) ) |
16 |
|
pm2.27 |
|- ( ( M e. V /\ E e. W ) -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` a ) ) -> ( S ` B ) C_ ( S ` a ) ) ) |
17 |
16
|
adantl |
|- ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` a ) ) -> ( S ` B ) C_ ( S ` a ) ) ) |
18 |
|
simpr |
|- ( ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) /\ ( S ` B ) C_ ( S ` a ) ) -> ( S ` B ) C_ ( S ` a ) ) |
19 |
|
ssun1 |
|- ( S ` a ) C_ ( ( S ` a ) u. { <. x , y >. | E. u e. ( S ` a ) ( E. v e. ( S ` a ) ( 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 = { z e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( z |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) |
20 |
|
simpl |
|- ( ( M e. V /\ E e. W ) -> M e. V ) |
21 |
|
simpr |
|- ( ( M e. V /\ E e. W ) -> E e. W ) |
22 |
|
simplll |
|- ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) -> a e. _om ) |
23 |
1
|
satfvsuc |
|- ( ( M e. V /\ E e. W /\ a e. _om ) -> ( S ` suc a ) = ( ( S ` a ) u. { <. x , y >. | E. u e. ( S ` a ) ( E. v e. ( S ` a ) ( 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 = { z e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( z |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) |
24 |
20 21 22 23
|
syl2an23an |
|- ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) -> ( S ` suc a ) = ( ( S ` a ) u. { <. x , y >. | E. u e. ( S ` a ) ( E. v e. ( S ` a ) ( 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 = { z e. ( M ^m _om ) | A. k e. M ( { <. i , k >. } u. ( z |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) |
25 |
19 24
|
sseqtrrid |
|- ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) -> ( S ` a ) C_ ( S ` suc a ) ) |
26 |
25
|
adantr |
|- ( ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) /\ ( S ` B ) C_ ( S ` a ) ) -> ( S ` a ) C_ ( S ` suc a ) ) |
27 |
18 26
|
sstrd |
|- ( ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) /\ ( S ` B ) C_ ( S ` a ) ) -> ( S ` B ) C_ ( S ` suc a ) ) |
28 |
27
|
ex |
|- ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) -> ( ( S ` B ) C_ ( S ` a ) -> ( S ` B ) C_ ( S ` suc a ) ) ) |
29 |
17 28
|
syld |
|- ( ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) /\ ( M e. V /\ E e. W ) ) -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` a ) ) -> ( S ` B ) C_ ( S ` suc a ) ) ) |
30 |
29
|
ex |
|- ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) -> ( ( M e. V /\ E e. W ) -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` a ) ) -> ( S ` B ) C_ ( S ` suc a ) ) ) ) |
31 |
30
|
com23 |
|- ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) -> ( ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` a ) ) -> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` suc a ) ) ) ) |
32 |
4 7 10 13 15 31
|
findsg |
|- ( ( ( A e. _om /\ B e. _om ) /\ B C_ A ) -> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` A ) ) ) |
33 |
32
|
ex |
|- ( ( A e. _om /\ B e. _om ) -> ( B C_ A -> ( ( M e. V /\ E e. W ) -> ( S ` B ) C_ ( S ` A ) ) ) ) |
34 |
33
|
com23 |
|- ( ( A e. _om /\ B e. _om ) -> ( ( M e. V /\ E e. W ) -> ( B C_ A -> ( S ` B ) C_ ( S ` A ) ) ) ) |
35 |
34
|
impcom |
|- ( ( ( M e. V /\ E e. W ) /\ ( A e. _om /\ B e. _om ) ) -> ( B C_ A -> ( S ` B ) C_ ( S ` A ) ) ) |