Metamath Proof Explorer

Theorem fin23lem36

Description: Lemma for fin23 . Weak order property of Y . (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypotheses fin23lem33.f 
|- F = { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }
fin23lem.f 
|- ( ph -> h : _om -1-1-> _V )
fin23lem.g 
|- ( ph -> U. ran h C_ G )
fin23lem.h 
|- ( ph -> A. j ( ( j : _om -1-1-> _V /\ U. ran j C_ G ) -> ( ( i ` j ) : _om -1-1-> _V /\ U. ran ( i ` j ) C. U. ran j ) ) )
fin23lem.i 
|- Y = ( rec ( i , h ) |` _om )
Assertion fin23lem36 
|- ( ( ( A e. _om /\ B e. _om ) /\ ( B C_ A /\ ph ) ) -> U. ran ( Y ` A ) C_ U. ran ( Y ` B ) )

Proof

Step Hyp Ref Expression
1 fin23lem33.f 
 |-  F = { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }
2 fin23lem.f 
 |-  ( ph -> h : _om -1-1-> _V )
3 fin23lem.g 
 |-  ( ph -> U. ran h C_ G )
4 fin23lem.h 
 |-  ( ph -> A. j ( ( j : _om -1-1-> _V /\ U. ran j C_ G ) -> ( ( i ` j ) : _om -1-1-> _V /\ U. ran ( i ` j ) C. U. ran j ) ) )
5 fin23lem.i 
 |-  Y = ( rec ( i , h ) |` _om )
6 fveq2 
 |-  ( a = B -> ( Y ` a ) = ( Y ` B ) )
7 6 rneqd 
 |-  ( a = B -> ran ( Y ` a ) = ran ( Y ` B ) )
8 7 unieqd 
 |-  ( a = B -> U. ran ( Y ` a ) = U. ran ( Y ` B ) )
9 8 sseq1d 
 |-  ( a = B -> ( U. ran ( Y ` a ) C_ U. ran ( Y ` B ) <-> U. ran ( Y ` B ) C_ U. ran ( Y ` B ) ) )
10 9 imbi2d 
 |-  ( a = B -> ( ( ph -> U. ran ( Y ` a ) C_ U. ran ( Y ` B ) ) <-> ( ph -> U. ran ( Y ` B ) C_ U. ran ( Y ` B ) ) ) )
11 fveq2 
 |-  ( a = b -> ( Y ` a ) = ( Y ` b ) )
12 11 rneqd 
 |-  ( a = b -> ran ( Y ` a ) = ran ( Y ` b ) )
13 12 unieqd 
 |-  ( a = b -> U. ran ( Y ` a ) = U. ran ( Y ` b ) )
14 13 sseq1d 
 |-  ( a = b -> ( U. ran ( Y ` a ) C_ U. ran ( Y ` B ) <-> U. ran ( Y ` b ) C_ U. ran ( Y ` B ) ) )
15 14 imbi2d 
 |-  ( a = b -> ( ( ph -> U. ran ( Y ` a ) C_ U. ran ( Y ` B ) ) <-> ( ph -> U. ran ( Y ` b ) C_ U. ran ( Y ` B ) ) ) )
16 fveq2 
 |-  ( a = suc b -> ( Y ` a ) = ( Y ` suc b ) )
17 16 rneqd 
 |-  ( a = suc b -> ran ( Y ` a ) = ran ( Y ` suc b ) )
18 17 unieqd 
 |-  ( a = suc b -> U. ran ( Y ` a ) = U. ran ( Y ` suc b ) )
19 18 sseq1d 
 |-  ( a = suc b -> ( U. ran ( Y ` a ) C_ U. ran ( Y ` B ) <-> U. ran ( Y ` suc b ) C_ U. ran ( Y ` B ) ) )
20 19 imbi2d 
 |-  ( a = suc b -> ( ( ph -> U. ran ( Y ` a ) C_ U. ran ( Y ` B ) ) <-> ( ph -> U. ran ( Y ` suc b ) C_ U. ran ( Y ` B ) ) ) )
21 fveq2 
 |-  ( a = A -> ( Y ` a ) = ( Y ` A ) )
22 21 rneqd 
 |-  ( a = A -> ran ( Y ` a ) = ran ( Y ` A ) )
23 22 unieqd 
 |-  ( a = A -> U. ran ( Y ` a ) = U. ran ( Y ` A ) )
24 23 sseq1d 
 |-  ( a = A -> ( U. ran ( Y ` a ) C_ U. ran ( Y ` B ) <-> U. ran ( Y ` A ) C_ U. ran ( Y ` B ) ) )
25 24 imbi2d 
 |-  ( a = A -> ( ( ph -> U. ran ( Y ` a ) C_ U. ran ( Y ` B ) ) <-> ( ph -> U. ran ( Y ` A ) C_ U. ran ( Y ` B ) ) ) )
26 ssid 
 |-  U. ran ( Y ` B ) C_ U. ran ( Y ` B )
27 26 2a1i 
 |-  ( B e. _om -> ( ph -> U. ran ( Y ` B ) C_ U. ran ( Y ` B ) ) )
28 simprr 
 |-  ( ( ( b e. _om /\ B e. _om ) /\ ( B C_ b /\ ph ) ) -> ph )
29 simpll 
 |-  ( ( ( b e. _om /\ B e. _om ) /\ ( B C_ b /\ ph ) ) -> b e. _om )
30 1 2 3 4 5 fin23lem35 
 |-  ( ( ph /\ b e. _om ) -> U. ran ( Y ` suc b ) C. U. ran ( Y ` b ) )
31 28 29 30 syl2anc 
 |-  ( ( ( b e. _om /\ B e. _om ) /\ ( B C_ b /\ ph ) ) -> U. ran ( Y ` suc b ) C. U. ran ( Y ` b ) )
32 31 pssssd 
 |-  ( ( ( b e. _om /\ B e. _om ) /\ ( B C_ b /\ ph ) ) -> U. ran ( Y ` suc b ) C_ U. ran ( Y ` b ) )
33 sstr2 
 |-  ( U. ran ( Y ` suc b ) C_ U. ran ( Y ` b ) -> ( U. ran ( Y ` b ) C_ U. ran ( Y ` B ) -> U. ran ( Y ` suc b ) C_ U. ran ( Y ` B ) ) )
34 32 33 syl 
 |-  ( ( ( b e. _om /\ B e. _om ) /\ ( B C_ b /\ ph ) ) -> ( U. ran ( Y ` b ) C_ U. ran ( Y ` B ) -> U. ran ( Y ` suc b ) C_ U. ran ( Y ` B ) ) )
35 34 expr 
 |-  ( ( ( b e. _om /\ B e. _om ) /\ B C_ b ) -> ( ph -> ( U. ran ( Y ` b ) C_ U. ran ( Y ` B ) -> U. ran ( Y ` suc b ) C_ U. ran ( Y ` B ) ) ) )
36 35 a2d 
 |-  ( ( ( b e. _om /\ B e. _om ) /\ B C_ b ) -> ( ( ph -> U. ran ( Y ` b ) C_ U. ran ( Y ` B ) ) -> ( ph -> U. ran ( Y ` suc b ) C_ U. ran ( Y ` B ) ) ) )
37 10 15 20 25 27 36 findsg 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ B C_ A ) -> ( ph -> U. ran ( Y ` A ) C_ U. ran ( Y ` B ) ) )
38 37 impr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( B C_ A /\ ph ) ) -> U. ran ( Y ` A ) C_ U. ran ( Y ` B ) )