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 )