Step |
Hyp |
Ref |
Expression |
1 |
|
dfuzi.1 |
|- N e. ZZ |
2 |
|
ssintab |
|- ( { z e. ZZ | N <_ z } C_ |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> A. x ( ( N e. x /\ A. y e. x ( y + 1 ) e. x ) -> { z e. ZZ | N <_ z } C_ x ) ) |
3 |
1
|
peano5uzi |
|- ( ( N e. x /\ A. y e. x ( y + 1 ) e. x ) -> { z e. ZZ | N <_ z } C_ x ) |
4 |
2 3
|
mpgbir |
|- { z e. ZZ | N <_ z } C_ |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) } |
5 |
1
|
zrei |
|- N e. RR |
6 |
5
|
leidi |
|- N <_ N |
7 |
|
breq2 |
|- ( z = N -> ( N <_ z <-> N <_ N ) ) |
8 |
7
|
elrab |
|- ( N e. { z e. ZZ | N <_ z } <-> ( N e. ZZ /\ N <_ N ) ) |
9 |
1 6 8
|
mpbir2an |
|- N e. { z e. ZZ | N <_ z } |
10 |
|
peano2uz2 |
|- ( ( N e. ZZ /\ y e. { z e. ZZ | N <_ z } ) -> ( y + 1 ) e. { z e. ZZ | N <_ z } ) |
11 |
1 10
|
mpan |
|- ( y e. { z e. ZZ | N <_ z } -> ( y + 1 ) e. { z e. ZZ | N <_ z } ) |
12 |
11
|
rgen |
|- A. y e. { z e. ZZ | N <_ z } ( y + 1 ) e. { z e. ZZ | N <_ z } |
13 |
|
zex |
|- ZZ e. _V |
14 |
13
|
rabex |
|- { z e. ZZ | N <_ z } e. _V |
15 |
|
eleq2 |
|- ( x = { z e. ZZ | N <_ z } -> ( N e. x <-> N e. { z e. ZZ | N <_ z } ) ) |
16 |
|
eleq2 |
|- ( x = { z e. ZZ | N <_ z } -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. { z e. ZZ | N <_ z } ) ) |
17 |
16
|
raleqbi1dv |
|- ( x = { z e. ZZ | N <_ z } -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. { z e. ZZ | N <_ z } ( y + 1 ) e. { z e. ZZ | N <_ z } ) ) |
18 |
15 17
|
anbi12d |
|- ( x = { z e. ZZ | N <_ z } -> ( ( N e. x /\ A. y e. x ( y + 1 ) e. x ) <-> ( N e. { z e. ZZ | N <_ z } /\ A. y e. { z e. ZZ | N <_ z } ( y + 1 ) e. { z e. ZZ | N <_ z } ) ) ) |
19 |
14 18
|
elab |
|- ( { z e. ZZ | N <_ z } e. { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> ( N e. { z e. ZZ | N <_ z } /\ A. y e. { z e. ZZ | N <_ z } ( y + 1 ) e. { z e. ZZ | N <_ z } ) ) |
20 |
9 12 19
|
mpbir2an |
|- { z e. ZZ | N <_ z } e. { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) } |
21 |
|
intss1 |
|- ( { z e. ZZ | N <_ z } e. { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) } -> |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) } C_ { z e. ZZ | N <_ z } ) |
22 |
20 21
|
ax-mp |
|- |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) } C_ { z e. ZZ | N <_ z } |
23 |
4 22
|
eqssi |
|- { z e. ZZ | N <_ z } = |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) } |