Metamath Proof Explorer

Theorem axdc4uzlem

Description: Lemma for axdc4uz . (Contributed by Mario Carneiro, 8-Jan-2014) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypotheses axdc4uz.1 
|- M e. ZZ
axdc4uz.2 
|- Z = ( ZZ>= ` M )
axdc4uz.3 
|- A e. _V
axdc4uz.4 
|- G = ( rec ( ( y e. _V |-> ( y + 1 ) ) , M ) |` _om )
axdc4uz.5 
|- H = ( n e. _om , x e. A |-> ( ( G ` n ) F x ) )
Assertion axdc4uzlem 
|- ( ( C e. A /\ F : ( Z X. A ) --> ( ~P A \ { (/) } ) ) -> E. g ( g : Z --> A /\ ( g ` M ) = C /\ A. k e. Z ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) )

Proof

Step Hyp Ref Expression
1 axdc4uz.1 
 |-  M e. ZZ
2 axdc4uz.2 
 |-  Z = ( ZZ>= ` M )
3 axdc4uz.3 
 |-  A e. _V
4 axdc4uz.4 
 |-  G = ( rec ( ( y e. _V |-> ( y + 1 ) ) , M ) |` _om )
5 axdc4uz.5 
 |-  H = ( n e. _om , x e. A |-> ( ( G ` n ) F x ) )
6 1 4 om2uzf1oi 
 |-  G : _om -1-1-onto-> ( ZZ>= ` M )
7 f1oeq3 
 |-  ( Z = ( ZZ>= ` M ) -> ( G : _om -1-1-onto-> Z <-> G : _om -1-1-onto-> ( ZZ>= ` M ) ) )
8 2 7 ax-mp 
 |-  ( G : _om -1-1-onto-> Z <-> G : _om -1-1-onto-> ( ZZ>= ` M ) )
9 6 8 mpbir 
 |-  G : _om -1-1-onto-> Z
10 f1of 
 |-  ( G : _om -1-1-onto-> Z -> G : _om --> Z )
11 9 10 ax-mp 
 |-  G : _om --> Z
12 11 ffvelrni 
 |-  ( n e. _om -> ( G ` n ) e. Z )
13 fovrn 
 |-  ( ( F : ( Z X. A ) --> ( ~P A \ { (/) } ) /\ ( G ` n ) e. Z /\ x e. A ) -> ( ( G ` n ) F x ) e. ( ~P A \ { (/) } ) )
14 12 13 syl3an2 
 |-  ( ( F : ( Z X. A ) --> ( ~P A \ { (/) } ) /\ n e. _om /\ x e. A ) -> ( ( G ` n ) F x ) e. ( ~P A \ { (/) } ) )
15 14 3expb 
 |-  ( ( F : ( Z X. A ) --> ( ~P A \ { (/) } ) /\ ( n e. _om /\ x e. A ) ) -> ( ( G ` n ) F x ) e. ( ~P A \ { (/) } ) )
16 15 ralrimivva 
 |-  ( F : ( Z X. A ) --> ( ~P A \ { (/) } ) -> A. n e. _om A. x e. A ( ( G ` n ) F x ) e. ( ~P A \ { (/) } ) )
17 5 fmpo 
 |-  ( A. n e. _om A. x e. A ( ( G ` n ) F x ) e. ( ~P A \ { (/) } ) <-> H : ( _om X. A ) --> ( ~P A \ { (/) } ) )
18 16 17 sylib 
 |-  ( F : ( Z X. A ) --> ( ~P A \ { (/) } ) -> H : ( _om X. A ) --> ( ~P A \ { (/) } ) )
19 3 axdc4 
 |-  ( ( C e. A /\ H : ( _om X. A ) --> ( ~P A \ { (/) } ) ) -> E. f ( f : _om --> A /\ ( f ` (/) ) = C /\ A. m e. _om ( f ` suc m ) e. ( m H ( f ` m ) ) ) )
20 18 19 sylan2 
 |-  ( ( C e. A /\ F : ( Z X. A ) --> ( ~P A \ { (/) } ) ) -> E. f ( f : _om --> A /\ ( f ` (/) ) = C /\ A. m e. _om ( f ` suc m ) e. ( m H ( f ` m ) ) ) )
21 f1ocnv 
 |-  ( G : _om -1-1-onto-> Z -> `' G : Z -1-1-onto-> _om )
22 f1of 
 |-  ( `' G : Z -1-1-onto-> _om -> `' G : Z --> _om )
23 9 21 22 mp2b 
 |-  `' G : Z --> _om
24 fco 
 |-  ( ( f : _om --> A /\ `' G : Z --> _om ) -> ( f o. `' G ) : Z --> A )
25 23 24 mpan2 
 |-  ( f : _om --> A -> ( f o. `' G ) : Z --> A )
26 25 3ad2ant1 
 |-  ( ( f : _om --> A /\ ( f ` (/) ) = C /\ A. m e. _om ( f ` suc m ) e. ( m H ( f ` m ) ) ) -> ( f o. `' G ) : Z --> A )
27 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
28 1 27 ax-mp 
 |-  M e. ( ZZ>= ` M )
29 28 2 eleqtrri 
 |-  M e. Z
30 fvco3 
 |-  ( ( `' G : Z --> _om /\ M e. Z ) -> ( ( f o. `' G ) ` M ) = ( f ` ( `' G ` M ) ) )
31 23 29 30 mp2an 
 |-  ( ( f o. `' G ) ` M ) = ( f ` ( `' G ` M ) )
32 1 4 om2uz0i 
 |-  ( G ` (/) ) = M
33 peano1 
 |-  (/) e. _om
34 f1ocnvfv 
 |-  ( ( G : _om -1-1-onto-> Z /\ (/) e. _om ) -> ( ( G ` (/) ) = M -> ( `' G ` M ) = (/) ) )
35 9 33 34 mp2an 
 |-  ( ( G ` (/) ) = M -> ( `' G ` M ) = (/) )
36 32 35 ax-mp 
 |-  ( `' G ` M ) = (/)
37 36 fveq2i 
 |-  ( f ` ( `' G ` M ) ) = ( f ` (/) )
38 31 37 eqtri 
 |-  ( ( f o. `' G ) ` M ) = ( f ` (/) )
39 simp2 
 |-  ( ( f : _om --> A /\ ( f ` (/) ) = C /\ A. m e. _om ( f ` suc m ) e. ( m H ( f ` m ) ) ) -> ( f ` (/) ) = C )
40 38 39 syl5eq 
 |-  ( ( f : _om --> A /\ ( f ` (/) ) = C /\ A. m e. _om ( f ` suc m ) e. ( m H ( f ` m ) ) ) -> ( ( f o. `' G ) ` M ) = C )
41 23 ffvelrni 
 |-  ( k e. Z -> ( `' G ` k ) e. _om )
42 41 adantl 
 |-  ( ( f : _om --> A /\ k e. Z ) -> ( `' G ` k ) e. _om )
43 suceq 
 |-  ( m = ( `' G ` k ) -> suc m = suc ( `' G ` k ) )
44 43 fveq2d 
 |-  ( m = ( `' G ` k ) -> ( f ` suc m ) = ( f ` suc ( `' G ` k ) ) )
45 id 
 |-  ( m = ( `' G ` k ) -> m = ( `' G ` k ) )
46 fveq2 
 |-  ( m = ( `' G ` k ) -> ( f ` m ) = ( f ` ( `' G ` k ) ) )
47 45 46 oveq12d 
 |-  ( m = ( `' G ` k ) -> ( m H ( f ` m ) ) = ( ( `' G ` k ) H ( f ` ( `' G ` k ) ) ) )
48 44 47 eleq12d 
 |-  ( m = ( `' G ` k ) -> ( ( f ` suc m ) e. ( m H ( f ` m ) ) <-> ( f ` suc ( `' G ` k ) ) e. ( ( `' G ` k ) H ( f ` ( `' G ` k ) ) ) ) )
49 48 rspcv 
 |-  ( ( `' G ` k ) e. _om -> ( A. m e. _om ( f ` suc m ) e. ( m H ( f ` m ) ) -> ( f ` suc ( `' G ` k ) ) e. ( ( `' G ` k ) H ( f ` ( `' G ` k ) ) ) ) )
50 42 49 syl 
 |-  ( ( f : _om --> A /\ k e. Z ) -> ( A. m e. _om ( f ` suc m ) e. ( m H ( f ` m ) ) -> ( f ` suc ( `' G ` k ) ) e. ( ( `' G ` k ) H ( f ` ( `' G ` k ) ) ) ) )
51 2 peano2uzs 
 |-  ( k e. Z -> ( k + 1 ) e. Z )
52 fvco3 
 |-  ( ( `' G : Z --> _om /\ ( k + 1 ) e. Z ) -> ( ( f o. `' G ) ` ( k + 1 ) ) = ( f ` ( `' G ` ( k + 1 ) ) ) )
53 23 51 52 sylancr 
 |-  ( k e. Z -> ( ( f o. `' G ) ` ( k + 1 ) ) = ( f ` ( `' G ` ( k + 1 ) ) ) )
54 1 4 om2uzsuci 
 |-  ( ( `' G ` k ) e. _om -> ( G ` suc ( `' G ` k ) ) = ( ( G ` ( `' G ` k ) ) + 1 ) )
55 41 54 syl 
 |-  ( k e. Z -> ( G ` suc ( `' G ` k ) ) = ( ( G ` ( `' G ` k ) ) + 1 ) )
56 f1ocnvfv2 
 |-  ( ( G : _om -1-1-onto-> Z /\ k e. Z ) -> ( G ` ( `' G ` k ) ) = k )
57 9 56 mpan 
 |-  ( k e. Z -> ( G ` ( `' G ` k ) ) = k )
58 57 oveq1d 
 |-  ( k e. Z -> ( ( G ` ( `' G ` k ) ) + 1 ) = ( k + 1 ) )
59 55 58 eqtrd 
 |-  ( k e. Z -> ( G ` suc ( `' G ` k ) ) = ( k + 1 ) )
60 peano2 
 |-  ( ( `' G ` k ) e. _om -> suc ( `' G ` k ) e. _om )
61 41 60 syl 
 |-  ( k e. Z -> suc ( `' G ` k ) e. _om )
62 f1ocnvfv 
 |-  ( ( G : _om -1-1-onto-> Z /\ suc ( `' G ` k ) e. _om ) -> ( ( G ` suc ( `' G ` k ) ) = ( k + 1 ) -> ( `' G ` ( k + 1 ) ) = suc ( `' G ` k ) ) )
63 9 61 62 sylancr 
 |-  ( k e. Z -> ( ( G ` suc ( `' G ` k ) ) = ( k + 1 ) -> ( `' G ` ( k + 1 ) ) = suc ( `' G ` k ) ) )
64 59 63 mpd 
 |-  ( k e. Z -> ( `' G ` ( k + 1 ) ) = suc ( `' G ` k ) )
65 64 fveq2d 
 |-  ( k e. Z -> ( f ` ( `' G ` ( k + 1 ) ) ) = ( f ` suc ( `' G ` k ) ) )
66 53 65 eqtr2d 
 |-  ( k e. Z -> ( f ` suc ( `' G ` k ) ) = ( ( f o. `' G ) ` ( k + 1 ) ) )
67 66 adantl 
 |-  ( ( f : _om --> A /\ k e. Z ) -> ( f ` suc ( `' G ` k ) ) = ( ( f o. `' G ) ` ( k + 1 ) ) )
68 ffvelrn 
 |-  ( ( f : _om --> A /\ ( `' G ` k ) e. _om ) -> ( f ` ( `' G ` k ) ) e. A )
69 41 68 sylan2 
 |-  ( ( f : _om --> A /\ k e. Z ) -> ( f ` ( `' G ` k ) ) e. A )
70 fveq2 
 |-  ( n = ( `' G ` k ) -> ( G ` n ) = ( G ` ( `' G ` k ) ) )
71 70 oveq1d 
 |-  ( n = ( `' G ` k ) -> ( ( G ` n ) F x ) = ( ( G ` ( `' G ` k ) ) F x ) )
72 oveq2 
 |-  ( x = ( f ` ( `' G ` k ) ) -> ( ( G ` ( `' G ` k ) ) F x ) = ( ( G ` ( `' G ` k ) ) F ( f ` ( `' G ` k ) ) ) )
73 ovex 
 |-  ( ( G ` ( `' G ` k ) ) F ( f ` ( `' G ` k ) ) ) e. _V
74 71 72 5 73 ovmpo 
 |-  ( ( ( `' G ` k ) e. _om /\ ( f ` ( `' G ` k ) ) e. A ) -> ( ( `' G ` k ) H ( f ` ( `' G ` k ) ) ) = ( ( G ` ( `' G ` k ) ) F ( f ` ( `' G ` k ) ) ) )
75 42 69 74 syl2anc 
 |-  ( ( f : _om --> A /\ k e. Z ) -> ( ( `' G ` k ) H ( f ` ( `' G ` k ) ) ) = ( ( G ` ( `' G ` k ) ) F ( f ` ( `' G ` k ) ) ) )
76 fvco3 
 |-  ( ( `' G : Z --> _om /\ k e. Z ) -> ( ( f o. `' G ) ` k ) = ( f ` ( `' G ` k ) ) )
77 23 76 mpan 
 |-  ( k e. Z -> ( ( f o. `' G ) ` k ) = ( f ` ( `' G ` k ) ) )
78 77 eqcomd 
 |-  ( k e. Z -> ( f ` ( `' G ` k ) ) = ( ( f o. `' G ) ` k ) )
79 57 78 oveq12d 
 |-  ( k e. Z -> ( ( G ` ( `' G ` k ) ) F ( f ` ( `' G ` k ) ) ) = ( k F ( ( f o. `' G ) ` k ) ) )
80 79 adantl 
 |-  ( ( f : _om --> A /\ k e. Z ) -> ( ( G ` ( `' G ` k ) ) F ( f ` ( `' G ` k ) ) ) = ( k F ( ( f o. `' G ) ` k ) ) )
81 75 80 eqtrd 
 |-  ( ( f : _om --> A /\ k e. Z ) -> ( ( `' G ` k ) H ( f ` ( `' G ` k ) ) ) = ( k F ( ( f o. `' G ) ` k ) ) )
82 67 81 eleq12d 
 |-  ( ( f : _om --> A /\ k e. Z ) -> ( ( f ` suc ( `' G ` k ) ) e. ( ( `' G ` k ) H ( f ` ( `' G ` k ) ) ) <-> ( ( f o. `' G ) ` ( k + 1 ) ) e. ( k F ( ( f o. `' G ) ` k ) ) ) )
83 50 82 sylibd 
 |-  ( ( f : _om --> A /\ k e. Z ) -> ( A. m e. _om ( f ` suc m ) e. ( m H ( f ` m ) ) -> ( ( f o. `' G ) ` ( k + 1 ) ) e. ( k F ( ( f o. `' G ) ` k ) ) ) )
84 83 impancom 
 |-  ( ( f : _om --> A /\ A. m e. _om ( f ` suc m ) e. ( m H ( f ` m ) ) ) -> ( k e. Z -> ( ( f o. `' G ) ` ( k + 1 ) ) e. ( k F ( ( f o. `' G ) ` k ) ) ) )
85 84 ralrimiv 
 |-  ( ( f : _om --> A /\ A. m e. _om ( f ` suc m ) e. ( m H ( f ` m ) ) ) -> A. k e. Z ( ( f o. `' G ) ` ( k + 1 ) ) e. ( k F ( ( f o. `' G ) ` k ) ) )
86 85 3adant2 
 |-  ( ( f : _om --> A /\ ( f ` (/) ) = C /\ A. m e. _om ( f ` suc m ) e. ( m H ( f ` m ) ) ) -> A. k e. Z ( ( f o. `' G ) ` ( k + 1 ) ) e. ( k F ( ( f o. `' G ) ` k ) ) )
87 vex 
 |-  f e. _V
88 rdgfun 
 |-  Fun rec ( ( y e. _V |-> ( y + 1 ) ) , M )
89 omex 
 |-  _om e. _V
90 resfunexg 
 |-  ( ( Fun rec ( ( y e. _V |-> ( y + 1 ) ) , M ) /\ _om e. _V ) -> ( rec ( ( y e. _V |-> ( y + 1 ) ) , M ) |` _om ) e. _V )
91 88 89 90 mp2an 
 |-  ( rec ( ( y e. _V |-> ( y + 1 ) ) , M ) |` _om ) e. _V
92 4 91 eqeltri 
 |-  G e. _V
93 92 cnvex 
 |-  `' G e. _V
94 87 93 coex 
 |-  ( f o. `' G ) e. _V
95 feq1 
 |-  ( g = ( f o. `' G ) -> ( g : Z --> A <-> ( f o. `' G ) : Z --> A ) )
96 fveq1 
 |-  ( g = ( f o. `' G ) -> ( g ` M ) = ( ( f o. `' G ) ` M ) )
97 96 eqeq1d 
 |-  ( g = ( f o. `' G ) -> ( ( g ` M ) = C <-> ( ( f o. `' G ) ` M ) = C ) )
98 fveq1 
 |-  ( g = ( f o. `' G ) -> ( g ` ( k + 1 ) ) = ( ( f o. `' G ) ` ( k + 1 ) ) )
99 fveq1 
 |-  ( g = ( f o. `' G ) -> ( g ` k ) = ( ( f o. `' G ) ` k ) )
100 99 oveq2d 
 |-  ( g = ( f o. `' G ) -> ( k F ( g ` k ) ) = ( k F ( ( f o. `' G ) ` k ) ) )
101 98 100 eleq12d 
 |-  ( g = ( f o. `' G ) -> ( ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) <-> ( ( f o. `' G ) ` ( k + 1 ) ) e. ( k F ( ( f o. `' G ) ` k ) ) ) )
102 101 ralbidv 
 |-  ( g = ( f o. `' G ) -> ( A. k e. Z ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) <-> A. k e. Z ( ( f o. `' G ) ` ( k + 1 ) ) e. ( k F ( ( f o. `' G ) ` k ) ) ) )
103 95 97 102 3anbi123d 
 |-  ( g = ( f o. `' G ) -> ( ( g : Z --> A /\ ( g ` M ) = C /\ A. k e. Z ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) <-> ( ( f o. `' G ) : Z --> A /\ ( ( f o. `' G ) ` M ) = C /\ A. k e. Z ( ( f o. `' G ) ` ( k + 1 ) ) e. ( k F ( ( f o. `' G ) ` k ) ) ) ) )
104 94 103 spcev 
 |-  ( ( ( f o. `' G ) : Z --> A /\ ( ( f o. `' G ) ` M ) = C /\ A. k e. Z ( ( f o. `' G ) ` ( k + 1 ) ) e. ( k F ( ( f o. `' G ) ` k ) ) ) -> E. g ( g : Z --> A /\ ( g ` M ) = C /\ A. k e. Z ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) )
105 26 40 86 104 syl3anc 
 |-  ( ( f : _om --> A /\ ( f ` (/) ) = C /\ A. m e. _om ( f ` suc m ) e. ( m H ( f ` m ) ) ) -> E. g ( g : Z --> A /\ ( g ` M ) = C /\ A. k e. Z ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) )
106 105 exlimiv 
 |-  ( E. f ( f : _om --> A /\ ( f ` (/) ) = C /\ A. m e. _om ( f ` suc m ) e. ( m H ( f ` m ) ) ) -> E. g ( g : Z --> A /\ ( g ` M ) = C /\ A. k e. Z ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) )
107 20 106 syl 
 |-  ( ( C e. A /\ F : ( Z X. A ) --> ( ~P A \ { (/) } ) ) -> E. g ( g : Z --> A /\ ( g ` M ) = C /\ A. k e. Z ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) )