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 ) ) ) ) |