Step |
Hyp |
Ref |
Expression |
1 |
|
indstr.1 |
|- ( x = y -> ( ph <-> ps ) ) |
2 |
|
indstr.2 |
|- ( x e. NN -> ( A. y e. NN ( y < x -> ps ) -> ph ) ) |
3 |
|
pm3.24 |
|- -. ( ph /\ -. ph ) |
4 |
|
nnre |
|- ( x e. NN -> x e. RR ) |
5 |
|
nnre |
|- ( y e. NN -> y e. RR ) |
6 |
|
lenlt |
|- ( ( x e. RR /\ y e. RR ) -> ( x <_ y <-> -. y < x ) ) |
7 |
4 5 6
|
syl2an |
|- ( ( x e. NN /\ y e. NN ) -> ( x <_ y <-> -. y < x ) ) |
8 |
7
|
imbi2d |
|- ( ( x e. NN /\ y e. NN ) -> ( ( -. ps -> x <_ y ) <-> ( -. ps -> -. y < x ) ) ) |
9 |
|
con34b |
|- ( ( y < x -> ps ) <-> ( -. ps -> -. y < x ) ) |
10 |
8 9
|
bitr4di |
|- ( ( x e. NN /\ y e. NN ) -> ( ( -. ps -> x <_ y ) <-> ( y < x -> ps ) ) ) |
11 |
10
|
ralbidva |
|- ( x e. NN -> ( A. y e. NN ( -. ps -> x <_ y ) <-> A. y e. NN ( y < x -> ps ) ) ) |
12 |
11 2
|
sylbid |
|- ( x e. NN -> ( A. y e. NN ( -. ps -> x <_ y ) -> ph ) ) |
13 |
12
|
anim2d |
|- ( x e. NN -> ( ( -. ph /\ A. y e. NN ( -. ps -> x <_ y ) ) -> ( -. ph /\ ph ) ) ) |
14 |
|
ancom |
|- ( ( -. ph /\ ph ) <-> ( ph /\ -. ph ) ) |
15 |
13 14
|
syl6ib |
|- ( x e. NN -> ( ( -. ph /\ A. y e. NN ( -. ps -> x <_ y ) ) -> ( ph /\ -. ph ) ) ) |
16 |
3 15
|
mtoi |
|- ( x e. NN -> -. ( -. ph /\ A. y e. NN ( -. ps -> x <_ y ) ) ) |
17 |
16
|
nrex |
|- -. E. x e. NN ( -. ph /\ A. y e. NN ( -. ps -> x <_ y ) ) |
18 |
1
|
notbid |
|- ( x = y -> ( -. ph <-> -. ps ) ) |
19 |
18
|
nnwos |
|- ( E. x e. NN -. ph -> E. x e. NN ( -. ph /\ A. y e. NN ( -. ps -> x <_ y ) ) ) |
20 |
17 19
|
mto |
|- -. E. x e. NN -. ph |
21 |
|
dfral2 |
|- ( A. x e. NN ph <-> -. E. x e. NN -. ph ) |
22 |
20 21
|
mpbir |
|- A. x e. NN ph |
23 |
22
|
rspec |
|- ( x e. NN -> ph ) |