Step |
Hyp |
Ref |
Expression |
1 |
|
eleq2 |
|- ( x = z -> ( 1 e. x <-> 1 e. z ) ) |
2 |
|
eleq2 |
|- ( x = z -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. z ) ) |
3 |
2
|
raleqbi1dv |
|- ( x = z -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. z ( y + 1 ) e. z ) ) |
4 |
1 3
|
anbi12d |
|- ( x = z -> ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) <-> ( 1 e. z /\ A. y e. z ( y + 1 ) e. z ) ) ) |
5 |
|
dfnn2 |
|- NN = |^| { z | ( 1 e. z /\ A. y e. z ( y + 1 ) e. z ) } |
6 |
5
|
eqeq2i |
|- ( x = NN <-> x = |^| { z | ( 1 e. z /\ A. y e. z ( y + 1 ) e. z ) } ) |
7 |
|
eleq2 |
|- ( x = NN -> ( 1 e. x <-> 1 e. NN ) ) |
8 |
|
eleq2 |
|- ( x = NN -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. NN ) ) |
9 |
8
|
raleqbi1dv |
|- ( x = NN -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. NN ( y + 1 ) e. NN ) ) |
10 |
7 9
|
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 ) ) ) |
11 |
6 10
|
sylbir |
|- ( x = |^| { z | ( 1 e. z /\ A. y e. z ( y + 1 ) e. z ) } -> ( ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) <-> ( 1 e. NN /\ A. y e. NN ( y + 1 ) e. NN ) ) ) |
12 |
|
nnssre |
|- NN C_ RR |
13 |
5 12
|
eqsstrri |
|- |^| { z | ( 1 e. z /\ A. y e. z ( y + 1 ) e. z ) } C_ RR |
14 |
|
1nn |
|- 1 e. NN |
15 |
|
peano2nn |
|- ( y e. NN -> ( y + 1 ) e. NN ) |
16 |
15
|
rgen |
|- A. y e. NN ( y + 1 ) e. NN |
17 |
14 16
|
pm3.2i |
|- ( 1 e. NN /\ A. y e. NN ( y + 1 ) e. NN ) |
18 |
13 17
|
pm3.2i |
|- ( |^| { z | ( 1 e. z /\ A. y e. z ( y + 1 ) e. z ) } C_ RR /\ ( 1 e. NN /\ A. y e. NN ( y + 1 ) e. NN ) ) |
19 |
4 11 18
|
intabs |
|- |^| { x | ( x C_ RR /\ ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) ) } = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } |
20 |
|
3anass |
|- ( ( x C_ RR /\ 1 e. x /\ A. y e. x ( y + 1 ) e. x ) <-> ( x C_ RR /\ ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) ) ) |
21 |
20
|
abbii |
|- { x | ( x C_ RR /\ 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } = { x | ( x C_ RR /\ ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) ) } |
22 |
21
|
inteqi |
|- |^| { x | ( x C_ RR /\ 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } = |^| { x | ( x C_ RR /\ ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) ) } |
23 |
|
dfnn2 |
|- NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } |
24 |
19 22 23
|
3eqtr4ri |
|- NN = |^| { x | ( x C_ RR /\ 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } |