Step |
Hyp |
Ref |
Expression |
1 |
|
1ex |
|- 1 e. _V |
2 |
1
|
elintab |
|- ( 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> A. x ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> 1 e. x ) ) |
3 |
|
simpl |
|- ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> 1 e. x ) |
4 |
2 3
|
mpgbir |
|- 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } |
5 |
|
oveq1 |
|- ( y = z -> ( y + 1 ) = ( z + 1 ) ) |
6 |
5
|
eleq1d |
|- ( y = z -> ( ( y + 1 ) e. x <-> ( z + 1 ) e. x ) ) |
7 |
6
|
rspccv |
|- ( A. y e. x ( y + 1 ) e. x -> ( z e. x -> ( z + 1 ) e. x ) ) |
8 |
7
|
adantl |
|- ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> ( z e. x -> ( z + 1 ) e. x ) ) |
9 |
8
|
a2i |
|- ( ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> z e. x ) -> ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> ( z + 1 ) e. x ) ) |
10 |
9
|
alimi |
|- ( A. x ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> z e. x ) -> A. x ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> ( z + 1 ) e. x ) ) |
11 |
|
vex |
|- z e. _V |
12 |
11
|
elintab |
|- ( z e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> A. x ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> z e. x ) ) |
13 |
|
ovex |
|- ( z + 1 ) e. _V |
14 |
13
|
elintab |
|- ( ( z + 1 ) e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> A. x ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) -> ( z + 1 ) e. x ) ) |
15 |
10 12 14
|
3imtr4i |
|- ( z e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } -> ( z + 1 ) e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } ) |
16 |
15
|
rgen |
|- A. z e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } ( z + 1 ) e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } |
17 |
|
peano5nni |
|- ( ( 1 e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } /\ A. z e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } ( z + 1 ) e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } ) -> NN C_ |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } ) |
18 |
4 16 17
|
mp2an |
|- NN C_ |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } |
19 |
|
1nn |
|- 1 e. NN |
20 |
|
peano2nn |
|- ( y e. NN -> ( y + 1 ) e. NN ) |
21 |
20
|
rgen |
|- A. y e. NN ( y + 1 ) e. NN |
22 |
|
nnex |
|- NN e. _V |
23 |
|
eleq2 |
|- ( x = NN -> ( 1 e. x <-> 1 e. NN ) ) |
24 |
|
eleq2 |
|- ( x = NN -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. NN ) ) |
25 |
24
|
raleqbi1dv |
|- ( x = NN -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. NN ( y + 1 ) e. NN ) ) |
26 |
23 25
|
anbi12d |
|- ( x = NN -> ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) <-> ( 1 e. NN /\ A. y e. NN ( y + 1 ) e. NN ) ) ) |
27 |
22 26
|
elab |
|- ( NN e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> ( 1 e. NN /\ A. y e. NN ( y + 1 ) e. NN ) ) |
28 |
19 21 27
|
mpbir2an |
|- NN e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } |
29 |
|
intss1 |
|- ( NN e. { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } -> |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } C_ NN ) |
30 |
28 29
|
ax-mp |
|- |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } C_ NN |
31 |
18 30
|
eqssi |
|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } |