Metamath Proof Explorer

Theorem fin23lem38

Description: Lemma for fin23 . The contradictory chain has no minimum. (Contributed by Stefan O'Rear, 2-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

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 fin23lem38 
|- ( ph -> -. |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) e. ran ( b e. _om |-> 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 peano2 
 |-  ( d e. _om -> suc d e. _om )
7 eqid 
 |-  U. ran ( Y ` suc d ) = U. ran ( Y ` suc d )
8 fveq2 
 |-  ( b = suc d -> ( Y ` b ) = ( Y ` suc d ) )
9 8 rneqd 
 |-  ( b = suc d -> ran ( Y ` b ) = ran ( Y ` suc d ) )
10 9 unieqd 
 |-  ( b = suc d -> U. ran ( Y ` b ) = U. ran ( Y ` suc d ) )
11 10 rspceeqv 
 |-  ( ( suc d e. _om /\ U. ran ( Y ` suc d ) = U. ran ( Y ` suc d ) ) -> E. b e. _om U. ran ( Y ` suc d ) = U. ran ( Y ` b ) )
12 7 11 mpan2 
 |-  ( suc d e. _om -> E. b e. _om U. ran ( Y ` suc d ) = U. ran ( Y ` b ) )
13 fvex 
 |-  ( Y ` suc d ) e. _V
14 13 rnex 
 |-  ran ( Y ` suc d ) e. _V
15 14 uniex 
 |-  U. ran ( Y ` suc d ) e. _V
16 eqid 
 |-  ( b e. _om |-> U. ran ( Y ` b ) ) = ( b e. _om |-> U. ran ( Y ` b ) )
17 16 elrnmpt 
 |-  ( U. ran ( Y ` suc d ) e. _V -> ( U. ran ( Y ` suc d ) e. ran ( b e. _om |-> U. ran ( Y ` b ) ) <-> E. b e. _om U. ran ( Y ` suc d ) = U. ran ( Y ` b ) ) )
18 15 17 ax-mp 
 |-  ( U. ran ( Y ` suc d ) e. ran ( b e. _om |-> U. ran ( Y ` b ) ) <-> E. b e. _om U. ran ( Y ` suc d ) = U. ran ( Y ` b ) )
19 12 18 sylibr 
 |-  ( suc d e. _om -> U. ran ( Y ` suc d ) e. ran ( b e. _om |-> U. ran ( Y ` b ) ) )
20 6 19 syl 
 |-  ( d e. _om -> U. ran ( Y ` suc d ) e. ran ( b e. _om |-> U. ran ( Y ` b ) ) )
21 20 adantl 
 |-  ( ( ph /\ d e. _om ) -> U. ran ( Y ` suc d ) e. ran ( b e. _om |-> U. ran ( Y ` b ) ) )
22 intss1 
 |-  ( U. ran ( Y ` suc d ) e. ran ( b e. _om |-> U. ran ( Y ` b ) ) -> |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) C_ U. ran ( Y ` suc d ) )
23 21 22 syl 
 |-  ( ( ph /\ d e. _om ) -> |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) C_ U. ran ( Y ` suc d ) )
24 1 2 3 4 5 fin23lem35 
 |-  ( ( ph /\ d e. _om ) -> U. ran ( Y ` suc d ) C. U. ran ( Y ` d ) )
25 23 24 sspsstrd 
 |-  ( ( ph /\ d e. _om ) -> |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) C. U. ran ( Y ` d ) )
26 dfpss2 
 |-  ( |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) C. U. ran ( Y ` d ) <-> ( |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) C_ U. ran ( Y ` d ) /\ -. |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) = U. ran ( Y ` d ) ) )
27 26 simprbi 
 |-  ( |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) C. U. ran ( Y ` d ) -> -. |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) = U. ran ( Y ` d ) )
28 25 27 syl 
 |-  ( ( ph /\ d e. _om ) -> -. |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) = U. ran ( Y ` d ) )
29 28 nrexdv 
 |-  ( ph -> -. E. d e. _om |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) = U. ran ( Y ` d ) )
30 fveq2 
 |-  ( b = d -> ( Y ` b ) = ( Y ` d ) )
31 30 rneqd 
 |-  ( b = d -> ran ( Y ` b ) = ran ( Y ` d ) )
32 31 unieqd 
 |-  ( b = d -> U. ran ( Y ` b ) = U. ran ( Y ` d ) )
33 32 cbvmptv 
 |-  ( b e. _om |-> U. ran ( Y ` b ) ) = ( d e. _om |-> U. ran ( Y ` d ) )
34 33 elrnmpt 
 |-  ( |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) e. ran ( b e. _om |-> U. ran ( Y ` b ) ) -> ( |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) e. ran ( b e. _om |-> U. ran ( Y ` b ) ) <-> E. d e. _om |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) = U. ran ( Y ` d ) ) )
35 34 ibi 
 |-  ( |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) e. ran ( b e. _om |-> U. ran ( Y ` b ) ) -> E. d e. _om |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) = U. ran ( Y ` d ) )
36 29 35 nsyl 
 |-  ( ph -> -. |^| ran ( b e. _om |-> U. ran ( Y ` b ) ) e. ran ( b e. _om |-> U. ran ( Y ` b ) ) )