Metamath Proof Explorer

Theorem ackbij2lem4

Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Hypotheses ackbij.f 
|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
ackbij.g 
|- G = ( x e. _V |-> ( y e. ~P dom x |-> ( F ` ( x " y ) ) ) )
Assertion ackbij2lem4 
|- ( ( ( A e. _om /\ B e. _om ) /\ B C_ A ) -> ( rec ( G , (/) ) ` B ) C_ ( rec ( G , (/) ) ` A ) )

Proof

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 ) )