Metamath Proof Explorer

Theorem axdc4uz

Description: A version of axdc4 that works on an upper set of integers instead of _om . (Contributed by Mario Carneiro, 8-Jan-2014)

Ref Expression
Hypotheses axdc4uz.1 
|- M e. ZZ
axdc4uz.2 
|- Z = ( ZZ>= ` M )
Assertion axdc4uz 
|- ( ( A e. V /\ 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 eleq2 
 |-  ( f = A -> ( C e. f <-> C e. A ) )
4 xpeq2 
 |-  ( f = A -> ( Z X. f ) = ( Z X. A ) )
5 pweq 
 |-  ( f = A -> ~P f = ~P A )
6 5 difeq1d 
 |-  ( f = A -> ( ~P f \ { (/) } ) = ( ~P A \ { (/) } ) )
7 4 6 feq23d 
 |-  ( f = A -> ( F : ( Z X. f ) --> ( ~P f \ { (/) } ) <-> F : ( Z X. A ) --> ( ~P A \ { (/) } ) ) )
8 3 7 anbi12d 
 |-  ( f = A -> ( ( C e. f /\ F : ( Z X. f ) --> ( ~P f \ { (/) } ) ) <-> ( C e. A /\ F : ( Z X. A ) --> ( ~P A \ { (/) } ) ) ) )
9 feq3 
 |-  ( f = A -> ( g : Z --> f <-> g : Z --> A ) )
10 9 3anbi1d 
 |-  ( f = A -> ( ( g : Z --> f /\ ( g ` M ) = C /\ A. k e. Z ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) <-> ( g : Z --> A /\ ( g ` M ) = C /\ A. k e. Z ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) ) )
11 10 exbidv 
 |-  ( f = A -> ( E. g ( g : Z --> f /\ ( g ` M ) = C /\ A. k e. Z ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) <-> E. g ( g : Z --> A /\ ( g ` M ) = C /\ A. k e. Z ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) ) )
12 8 11 imbi12d 
 |-  ( f = A -> ( ( ( C e. f /\ F : ( Z X. f ) --> ( ~P f \ { (/) } ) ) -> E. g ( g : Z --> f /\ ( g ` M ) = C /\ A. k e. Z ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) ) <-> ( ( 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 ) ) ) ) ) )
13 vex 
 |-  f e. _V
14 eqid 
 |-  ( rec ( ( y e. _V |-> ( y + 1 ) ) , M ) |` _om ) = ( rec ( ( y e. _V |-> ( y + 1 ) ) , M ) |` _om )
15 eqid 
 |-  ( n e. _om , x e. f |-> ( ( ( rec ( ( y e. _V |-> ( y + 1 ) ) , M ) |` _om ) ` n ) F x ) ) = ( n e. _om , x e. f |-> ( ( ( rec ( ( y e. _V |-> ( y + 1 ) ) , M ) |` _om ) ` n ) F x ) )
16 1 2 13 14 15 axdc4uzlem 
 |-  ( ( C e. f /\ F : ( Z X. f ) --> ( ~P f \ { (/) } ) ) -> E. g ( g : Z --> f /\ ( g ` M ) = C /\ A. k e. Z ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) )
17 12 16 vtoclg 
 |-  ( A e. V -> ( ( 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 ) ) ) ) )
18 17 3impib 
 |-  ( ( A e. V /\ 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 ) ) ) )