Metamath Proof Explorer

Theorem fin23lem39

Description: Lemma for fin23 . Thus, we have that g could not have been in F after all. (Contributed by Stefan O'Rear, 4-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 fin23lem39 
|- ( ph -> -. G e. F )

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 fin23lem38 
 |-  ( ph -> -. |^| ran ( c e. _om |-> U. ran ( Y ` c ) ) e. ran ( c e. _om |-> U. ran ( Y ` c ) ) )
7 1 2 3 4 5 fin23lem35 
 |-  ( ( ph /\ e e. _om ) -> U. ran ( Y ` suc e ) C. U. ran ( Y ` e ) )
8 7 pssssd 
 |-  ( ( ph /\ e e. _om ) -> U. ran ( Y ` suc e ) C_ U. ran ( Y ` e ) )
9 peano2 
 |-  ( e e. _om -> suc e e. _om )
10 fveq2 
 |-  ( c = suc e -> ( Y ` c ) = ( Y ` suc e ) )
11 10 rneqd 
 |-  ( c = suc e -> ran ( Y ` c ) = ran ( Y ` suc e ) )
12 11 unieqd 
 |-  ( c = suc e -> U. ran ( Y ` c ) = U. ran ( Y ` suc e ) )
13 eqid 
 |-  ( c e. _om |-> U. ran ( Y ` c ) ) = ( c e. _om |-> U. ran ( Y ` c ) )
14 fvex 
 |-  ( Y ` suc e ) e. _V
15 14 rnex 
 |-  ran ( Y ` suc e ) e. _V
16 15 uniex 
 |-  U. ran ( Y ` suc e ) e. _V
17 12 13 16 fvmpt 
 |-  ( suc e e. _om -> ( ( c e. _om |-> U. ran ( Y ` c ) ) ` suc e ) = U. ran ( Y ` suc e ) )
18 9 17 syl 
 |-  ( e e. _om -> ( ( c e. _om |-> U. ran ( Y ` c ) ) ` suc e ) = U. ran ( Y ` suc e ) )
19 fveq2 
 |-  ( c = e -> ( Y ` c ) = ( Y ` e ) )
20 19 rneqd 
 |-  ( c = e -> ran ( Y ` c ) = ran ( Y ` e ) )
21 20 unieqd 
 |-  ( c = e -> U. ran ( Y ` c ) = U. ran ( Y ` e ) )
22 fvex 
 |-  ( Y ` e ) e. _V
23 22 rnex 
 |-  ran ( Y ` e ) e. _V
24 23 uniex 
 |-  U. ran ( Y ` e ) e. _V
25 21 13 24 fvmpt 
 |-  ( e e. _om -> ( ( c e. _om |-> U. ran ( Y ` c ) ) ` e ) = U. ran ( Y ` e ) )
26 18 25 sseq12d 
 |-  ( e e. _om -> ( ( ( c e. _om |-> U. ran ( Y ` c ) ) ` suc e ) C_ ( ( c e. _om |-> U. ran ( Y ` c ) ) ` e ) <-> U. ran ( Y ` suc e ) C_ U. ran ( Y ` e ) ) )
27 26 adantl 
 |-  ( ( ph /\ e e. _om ) -> ( ( ( c e. _om |-> U. ran ( Y ` c ) ) ` suc e ) C_ ( ( c e. _om |-> U. ran ( Y ` c ) ) ` e ) <-> U. ran ( Y ` suc e ) C_ U. ran ( Y ` e ) ) )
28 8 27 mpbird 
 |-  ( ( ph /\ e e. _om ) -> ( ( c e. _om |-> U. ran ( Y ` c ) ) ` suc e ) C_ ( ( c e. _om |-> U. ran ( Y ` c ) ) ` e ) )
29 28 ralrimiva 
 |-  ( ph -> A. e e. _om ( ( c e. _om |-> U. ran ( Y ` c ) ) ` suc e ) C_ ( ( c e. _om |-> U. ran ( Y ` c ) ) ` e ) )
30 29 adantr 
 |-  ( ( ph /\ G e. F ) -> A. e e. _om ( ( c e. _om |-> U. ran ( Y ` c ) ) ` suc e ) C_ ( ( c e. _om |-> U. ran ( Y ` c ) ) ` e ) )
31 fveq1 
 |-  ( d = ( c e. _om |-> U. ran ( Y ` c ) ) -> ( d ` suc e ) = ( ( c e. _om |-> U. ran ( Y ` c ) ) ` suc e ) )
32 fveq1 
 |-  ( d = ( c e. _om |-> U. ran ( Y ` c ) ) -> ( d ` e ) = ( ( c e. _om |-> U. ran ( Y ` c ) ) ` e ) )
33 31 32 sseq12d 
 |-  ( d = ( c e. _om |-> U. ran ( Y ` c ) ) -> ( ( d ` suc e ) C_ ( d ` e ) <-> ( ( c e. _om |-> U. ran ( Y ` c ) ) ` suc e ) C_ ( ( c e. _om |-> U. ran ( Y ` c ) ) ` e ) ) )
34 33 ralbidv 
 |-  ( d = ( c e. _om |-> U. ran ( Y ` c ) ) -> ( A. e e. _om ( d ` suc e ) C_ ( d ` e ) <-> A. e e. _om ( ( c e. _om |-> U. ran ( Y ` c ) ) ` suc e ) C_ ( ( c e. _om |-> U. ran ( Y ` c ) ) ` e ) ) )
35 rneq 
 |-  ( d = ( c e. _om |-> U. ran ( Y ` c ) ) -> ran d = ran ( c e. _om |-> U. ran ( Y ` c ) ) )
36 35 inteqd 
 |-  ( d = ( c e. _om |-> U. ran ( Y ` c ) ) -> |^| ran d = |^| ran ( c e. _om |-> U. ran ( Y ` c ) ) )
37 36 35 eleq12d 
 |-  ( d = ( c e. _om |-> U. ran ( Y ` c ) ) -> ( |^| ran d e. ran d <-> |^| ran ( c e. _om |-> U. ran ( Y ` c ) ) e. ran ( c e. _om |-> U. ran ( Y ` c ) ) ) )
38 34 37 imbi12d 
 |-  ( d = ( c e. _om |-> U. ran ( Y ` c ) ) -> ( ( A. e e. _om ( d ` suc e ) C_ ( d ` e ) -> |^| ran d e. ran d ) <-> ( A. e e. _om ( ( c e. _om |-> U. ran ( Y ` c ) ) ` suc e ) C_ ( ( c e. _om |-> U. ran ( Y ` c ) ) ` e ) -> |^| ran ( c e. _om |-> U. ran ( Y ` c ) ) e. ran ( c e. _om |-> U. ran ( Y ` c ) ) ) ) )
39 1 isfin3ds 
 |-  ( G e. F -> ( G e. F <-> A. d e. ( ~P G ^m _om ) ( A. e e. _om ( d ` suc e ) C_ ( d ` e ) -> |^| ran d e. ran d ) ) )
40 39 ibi 
 |-  ( G e. F -> A. d e. ( ~P G ^m _om ) ( A. e e. _om ( d ` suc e ) C_ ( d ` e ) -> |^| ran d e. ran d ) )
41 40 adantl 
 |-  ( ( ph /\ G e. F ) -> A. d e. ( ~P G ^m _om ) ( A. e e. _om ( d ` suc e ) C_ ( d ` e ) -> |^| ran d e. ran d ) )
42 1 2 3 4 5 fin23lem34 
 |-  ( ( ph /\ c e. _om ) -> ( ( Y ` c ) : _om -1-1-> _V /\ U. ran ( Y ` c ) C_ G ) )
43 42 simprd 
 |-  ( ( ph /\ c e. _om ) -> U. ran ( Y ` c ) C_ G )
44 43 adantlr 
 |-  ( ( ( ph /\ G e. F ) /\ c e. _om ) -> U. ran ( Y ` c ) C_ G )
45 elpw2g 
 |-  ( G e. F -> ( U. ran ( Y ` c ) e. ~P G <-> U. ran ( Y ` c ) C_ G ) )
46 45 ad2antlr 
 |-  ( ( ( ph /\ G e. F ) /\ c e. _om ) -> ( U. ran ( Y ` c ) e. ~P G <-> U. ran ( Y ` c ) C_ G ) )
47 44 46 mpbird 
 |-  ( ( ( ph /\ G e. F ) /\ c e. _om ) -> U. ran ( Y ` c ) e. ~P G )
48 47 fmpttd 
 |-  ( ( ph /\ G e. F ) -> ( c e. _om |-> U. ran ( Y ` c ) ) : _om --> ~P G )
49 pwexg 
 |-  ( G e. F -> ~P G e. _V )
50 vex 
 |-  h e. _V
51 f1f 
 |-  ( h : _om -1-1-> _V -> h : _om --> _V )
52 dmfex 
 |-  ( ( h e. _V /\ h : _om --> _V ) -> _om e. _V )
53 50 51 52 sylancr 
 |-  ( h : _om -1-1-> _V -> _om e. _V )
54 2 53 syl 
 |-  ( ph -> _om e. _V )
55 elmapg 
 |-  ( ( ~P G e. _V /\ _om e. _V ) -> ( ( c e. _om |-> U. ran ( Y ` c ) ) e. ( ~P G ^m _om ) <-> ( c e. _om |-> U. ran ( Y ` c ) ) : _om --> ~P G ) )
56 49 54 55 syl2anr 
 |-  ( ( ph /\ G e. F ) -> ( ( c e. _om |-> U. ran ( Y ` c ) ) e. ( ~P G ^m _om ) <-> ( c e. _om |-> U. ran ( Y ` c ) ) : _om --> ~P G ) )
57 48 56 mpbird 
 |-  ( ( ph /\ G e. F ) -> ( c e. _om |-> U. ran ( Y ` c ) ) e. ( ~P G ^m _om ) )
58 38 41 57 rspcdva 
 |-  ( ( ph /\ G e. F ) -> ( A. e e. _om ( ( c e. _om |-> U. ran ( Y ` c ) ) ` suc e ) C_ ( ( c e. _om |-> U. ran ( Y ` c ) ) ` e ) -> |^| ran ( c e. _om |-> U. ran ( Y ` c ) ) e. ran ( c e. _om |-> U. ran ( Y ` c ) ) ) )
59 30 58 mpd 
 |-  ( ( ph /\ G e. F ) -> |^| ran ( c e. _om |-> U. ran ( Y ` c ) ) e. ran ( c e. _om |-> U. ran ( Y ` c ) ) )
60 6 59 mtand 
 |-  ( ph -> -. G e. F )