Step |
Hyp |
Ref |
Expression |
1 |
|
fin23lem.a |
|- U = seqom ( ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t ) |
2 |
|
fveq2 |
|- ( b = B -> ( U ` b ) = ( U ` B ) ) |
3 |
2
|
sseq1d |
|- ( b = B -> ( ( U ` b ) C_ ( U ` B ) <-> ( U ` B ) C_ ( U ` B ) ) ) |
4 |
|
fveq2 |
|- ( b = a -> ( U ` b ) = ( U ` a ) ) |
5 |
4
|
sseq1d |
|- ( b = a -> ( ( U ` b ) C_ ( U ` B ) <-> ( U ` a ) C_ ( U ` B ) ) ) |
6 |
|
fveq2 |
|- ( b = suc a -> ( U ` b ) = ( U ` suc a ) ) |
7 |
6
|
sseq1d |
|- ( b = suc a -> ( ( U ` b ) C_ ( U ` B ) <-> ( U ` suc a ) C_ ( U ` B ) ) ) |
8 |
|
fveq2 |
|- ( b = A -> ( U ` b ) = ( U ` A ) ) |
9 |
8
|
sseq1d |
|- ( b = A -> ( ( U ` b ) C_ ( U ` B ) <-> ( U ` A ) C_ ( U ` B ) ) ) |
10 |
|
ssidd |
|- ( B e. _om -> ( U ` B ) C_ ( U ` B ) ) |
11 |
1
|
fin23lem13 |
|- ( a e. _om -> ( U ` suc a ) C_ ( U ` a ) ) |
12 |
11
|
ad2antrr |
|- ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) -> ( U ` suc a ) C_ ( U ` a ) ) |
13 |
|
sstr2 |
|- ( ( U ` suc a ) C_ ( U ` a ) -> ( ( U ` a ) C_ ( U ` B ) -> ( U ` suc a ) C_ ( U ` B ) ) ) |
14 |
12 13
|
syl |
|- ( ( ( a e. _om /\ B e. _om ) /\ B C_ a ) -> ( ( U ` a ) C_ ( U ` B ) -> ( U ` suc a ) C_ ( U ` B ) ) ) |
15 |
3 5 7 9 10 14
|
findsg |
|- ( ( ( A e. _om /\ B e. _om ) /\ B C_ A ) -> ( U ` A ) C_ ( U ` B ) ) |