Step |
Hyp |
Ref |
Expression |
1 |
|
ackbij.f |
|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) ) |
2 |
|
ackbij.g |
|- G = ( x e. _V |-> ( y e. ~P dom x |-> ( F ` ( x " y ) ) ) ) |
3 |
|
fveq2 |
|- ( a = B -> ( rec ( G , (/) ) ` a ) = ( rec ( G , (/) ) ` B ) ) |
4 |
3
|
sseq2d |
|- ( a = B -> ( ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` a ) <-> ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` B ) ) ) |
5 |
|
fveq2 |
|- ( a = b -> ( rec ( G , (/) ) ` a ) = ( rec ( G , (/) ) ` b ) ) |
6 |
5
|
sseq2d |
|- ( a = b -> ( ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` a ) <-> ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` b ) ) ) |
7 |
|
fveq2 |
|- ( a = suc b -> ( rec ( G , (/) ) ` a ) = ( rec ( G , (/) ) ` suc b ) ) |
8 |
7
|
sseq2d |
|- ( a = suc b -> ( ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` a ) <-> ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` suc b ) ) ) |
9 |
|
fveq2 |
|- ( a = A -> ( rec ( G , (/) ) ` a ) = ( rec ( G , (/) ) ` A ) ) |
10 |
9
|
sseq2d |
|- ( a = A -> ( ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` a ) <-> ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` A ) ) ) |
11 |
|
ssidd |
|- ( B e. _om -> ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` B ) ) |
12 |
1 2
|
ackbij2lem3 |
|- ( b e. _om -> ( rec ( G , (/) ) ` b ) C_ ( rec ( G , (/) ) ` suc b ) ) |
13 |
12
|
ad2antrr |
|- ( ( ( b e. _om /\ B e. _om ) /\ B C_ b ) -> ( rec ( G , (/) ) ` b ) C_ ( rec ( G , (/) ) ` suc b ) ) |
14 |
|
sstr2 |
|- ( ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` b ) -> ( ( rec ( G , (/) ) ` b ) C_ ( rec ( G , (/) ) ` suc b ) -> ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` suc b ) ) ) |
15 |
13 14
|
syl5com |
|- ( ( ( b e. _om /\ B e. _om ) /\ B C_ b ) -> ( ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` b ) -> ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` suc b ) ) ) |
16 |
4 6 8 10 11 15
|
findsg |
|- ( ( ( A e. _om /\ B e. _om ) /\ B C_ A ) -> ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` A ) ) |