Step |
Hyp |
Ref |
Expression |
1 |
|
eleq1 |
|- ( N = if ( N e. ZZ , N , 1 ) -> ( N e. A <-> if ( N e. ZZ , N , 1 ) e. A ) ) |
2 |
1
|
anbi1d |
|- ( N = if ( N e. ZZ , N , 1 ) -> ( ( N e. A /\ A. x e. A ( x + 1 ) e. A ) <-> ( if ( N e. ZZ , N , 1 ) e. A /\ A. x e. A ( x + 1 ) e. A ) ) ) |
3 |
|
breq1 |
|- ( N = if ( N e. ZZ , N , 1 ) -> ( N <_ k <-> if ( N e. ZZ , N , 1 ) <_ k ) ) |
4 |
3
|
rabbidv |
|- ( N = if ( N e. ZZ , N , 1 ) -> { k e. ZZ | N <_ k } = { k e. ZZ | if ( N e. ZZ , N , 1 ) <_ k } ) |
5 |
4
|
sseq1d |
|- ( N = if ( N e. ZZ , N , 1 ) -> ( { k e. ZZ | N <_ k } C_ A <-> { k e. ZZ | if ( N e. ZZ , N , 1 ) <_ k } C_ A ) ) |
6 |
2 5
|
imbi12d |
|- ( N = if ( N e. ZZ , N , 1 ) -> ( ( ( N e. A /\ A. x e. A ( x + 1 ) e. A ) -> { k e. ZZ | N <_ k } C_ A ) <-> ( ( if ( N e. ZZ , N , 1 ) e. A /\ A. x e. A ( x + 1 ) e. A ) -> { k e. ZZ | if ( N e. ZZ , N , 1 ) <_ k } C_ A ) ) ) |
7 |
|
1z |
|- 1 e. ZZ |
8 |
7
|
elimel |
|- if ( N e. ZZ , N , 1 ) e. ZZ |
9 |
8
|
peano5uzi |
|- ( ( if ( N e. ZZ , N , 1 ) e. A /\ A. x e. A ( x + 1 ) e. A ) -> { k e. ZZ | if ( N e. ZZ , N , 1 ) <_ k } C_ A ) |
10 |
6 9
|
dedth |
|- ( N e. ZZ -> ( ( N e. A /\ A. x e. A ( x + 1 ) e. A ) -> { k e. ZZ | N <_ k } C_ A ) ) |