Metamath Proof Explorer

Theorem fin23lem35

Description: Lemma for fin23 . Strict 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 fin23lem35 
|- ( ( ph /\ A e. _om ) -> U. ran ( Y ` suc A ) C. U. ran ( Y ` A ) )

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 1 2 3 4 5 fin23lem34 
 |-  ( ( ph /\ A e. _om ) -> ( ( Y ` A ) : _om -1-1-> _V /\ U. ran ( Y ` A ) C_ G ) )
7 fvex 
 |-  ( Y ` A ) e. _V
8 f1eq1 
 |-  ( j = ( Y ` A ) -> ( j : _om -1-1-> _V <-> ( Y ` A ) : _om -1-1-> _V ) )
9 rneq 
 |-  ( j = ( Y ` A ) -> ran j = ran ( Y ` A ) )
10 9 unieqd 
 |-  ( j = ( Y ` A ) -> U. ran j = U. ran ( Y ` A ) )
11 10 sseq1d 
 |-  ( j = ( Y ` A ) -> ( U. ran j C_ G <-> U. ran ( Y ` A ) C_ G ) )
12 8 11 anbi12d 
 |-  ( j = ( Y ` A ) -> ( ( j : _om -1-1-> _V /\ U. ran j C_ G ) <-> ( ( Y ` A ) : _om -1-1-> _V /\ U. ran ( Y ` A ) C_ G ) ) )
13 fveq2 
 |-  ( j = ( Y ` A ) -> ( i ` j ) = ( i ` ( Y ` A ) ) )
14 f1eq1 
 |-  ( ( i ` j ) = ( i ` ( Y ` A ) ) -> ( ( i ` j ) : _om -1-1-> _V <-> ( i ` ( Y ` A ) ) : _om -1-1-> _V ) )
15 13 14 syl 
 |-  ( j = ( Y ` A ) -> ( ( i ` j ) : _om -1-1-> _V <-> ( i ` ( Y ` A ) ) : _om -1-1-> _V ) )
16 13 rneqd 
 |-  ( j = ( Y ` A ) -> ran ( i ` j ) = ran ( i ` ( Y ` A ) ) )
17 16 unieqd 
 |-  ( j = ( Y ` A ) -> U. ran ( i ` j ) = U. ran ( i ` ( Y ` A ) ) )
18 17 10 psseq12d 
 |-  ( j = ( Y ` A ) -> ( U. ran ( i ` j ) C. U. ran j <-> U. ran ( i ` ( Y ` A ) ) C. U. ran ( Y ` A ) ) )
19 15 18 anbi12d 
 |-  ( j = ( Y ` A ) -> ( ( ( i ` j ) : _om -1-1-> _V /\ U. ran ( i ` j ) C. U. ran j ) <-> ( ( i ` ( Y ` A ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` A ) ) C. U. ran ( Y ` A ) ) ) )
20 12 19 imbi12d 
 |-  ( j = ( Y ` A ) -> ( ( ( j : _om -1-1-> _V /\ U. ran j C_ G ) -> ( ( i ` j ) : _om -1-1-> _V /\ U. ran ( i ` j ) C. U. ran j ) ) <-> ( ( ( Y ` A ) : _om -1-1-> _V /\ U. ran ( Y ` A ) C_ G ) -> ( ( i ` ( Y ` A ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` A ) ) C. U. ran ( Y ` A ) ) ) ) )
21 7 20 spcv 
 |-  ( 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 ) ) -> ( ( ( Y ` A ) : _om -1-1-> _V /\ U. ran ( Y ` A ) C_ G ) -> ( ( i ` ( Y ` A ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` A ) ) C. U. ran ( Y ` A ) ) ) )
22 4 21 syl 
 |-  ( ph -> ( ( ( Y ` A ) : _om -1-1-> _V /\ U. ran ( Y ` A ) C_ G ) -> ( ( i ` ( Y ` A ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` A ) ) C. U. ran ( Y ` A ) ) ) )
23 22 adantr 
 |-  ( ( ph /\ A e. _om ) -> ( ( ( Y ` A ) : _om -1-1-> _V /\ U. ran ( Y ` A ) C_ G ) -> ( ( i ` ( Y ` A ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` A ) ) C. U. ran ( Y ` A ) ) ) )
24 6 23 mpd 
 |-  ( ( ph /\ A e. _om ) -> ( ( i ` ( Y ` A ) ) : _om -1-1-> _V /\ U. ran ( i ` ( Y ` A ) ) C. U. ran ( Y ` A ) ) )
25 24 simprd 
 |-  ( ( ph /\ A e. _om ) -> U. ran ( i ` ( Y ` A ) ) C. U. ran ( Y ` A ) )
26 frsuc 
 |-  ( A e. _om -> ( ( rec ( i , h ) |` _om ) ` suc A ) = ( i ` ( ( rec ( i , h ) |` _om ) ` A ) ) )
27 26 adantl 
 |-  ( ( ph /\ A e. _om ) -> ( ( rec ( i , h ) |` _om ) ` suc A ) = ( i ` ( ( rec ( i , h ) |` _om ) ` A ) ) )
28 5 fveq1i 
 |-  ( Y ` suc A ) = ( ( rec ( i , h ) |` _om ) ` suc A )
29 5 fveq1i 
 |-  ( Y ` A ) = ( ( rec ( i , h ) |` _om ) ` A )
30 29 fveq2i 
 |-  ( i ` ( Y ` A ) ) = ( i ` ( ( rec ( i , h ) |` _om ) ` A ) )
31 27 28 30 3eqtr4g 
 |-  ( ( ph /\ A e. _om ) -> ( Y ` suc A ) = ( i ` ( Y ` A ) ) )
32 31 rneqd 
 |-  ( ( ph /\ A e. _om ) -> ran ( Y ` suc A ) = ran ( i ` ( Y ` A ) ) )
33 32 unieqd 
 |-  ( ( ph /\ A e. _om ) -> U. ran ( Y ` suc A ) = U. ran ( i ` ( Y ` A ) ) )
34 33 psseq1d 
 |-  ( ( ph /\ A e. _om ) -> ( U. ran ( Y ` suc A ) C. U. ran ( Y ` A ) <-> U. ran ( i ` ( Y ` A ) ) C. U. ran ( Y ` A ) ) )
35 25 34 mpbird 
 |-  ( ( ph /\ A e. _om ) -> U. ran ( Y ` suc A ) C. U. ran ( Y ` A ) )