Step |
Hyp |
Ref |
Expression |
1 |
|
rexanuz3.1 |
|- F/ j ph |
2 |
|
rexanuz3.2 |
|- Z = ( ZZ>= ` M ) |
3 |
|
rexanuz3.3 |
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ch ) |
4 |
|
rexanuz3.4 |
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ps ) |
5 |
|
rexanuz3.5 |
|- ( k = j -> ( ch <-> th ) ) |
6 |
|
rexanuz3.6 |
|- ( k = j -> ( ps <-> ta ) ) |
7 |
3 4
|
jca |
|- ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ch /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) ) |
8 |
2
|
rexanuz2 |
|- ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ch /\ ps ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) ch /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) ) |
9 |
7 8
|
sylibr |
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ch /\ ps ) ) |
10 |
2
|
eleq2i |
|- ( j e. Z <-> j e. ( ZZ>= ` M ) ) |
11 |
10
|
biimpi |
|- ( j e. Z -> j e. ( ZZ>= ` M ) ) |
12 |
|
eluzelz |
|- ( j e. ( ZZ>= ` M ) -> j e. ZZ ) |
13 |
|
uzid |
|- ( j e. ZZ -> j e. ( ZZ>= ` j ) ) |
14 |
11 12 13
|
3syl |
|- ( j e. Z -> j e. ( ZZ>= ` j ) ) |
15 |
14
|
adantr |
|- ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ch /\ ps ) ) -> j e. ( ZZ>= ` j ) ) |
16 |
|
simpr |
|- ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ch /\ ps ) ) -> A. k e. ( ZZ>= ` j ) ( ch /\ ps ) ) |
17 |
5 6
|
anbi12d |
|- ( k = j -> ( ( ch /\ ps ) <-> ( th /\ ta ) ) ) |
18 |
17
|
rspcva |
|- ( ( j e. ( ZZ>= ` j ) /\ A. k e. ( ZZ>= ` j ) ( ch /\ ps ) ) -> ( th /\ ta ) ) |
19 |
15 16 18
|
syl2anc |
|- ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ch /\ ps ) ) -> ( th /\ ta ) ) |
20 |
19
|
adantll |
|- ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ch /\ ps ) ) -> ( th /\ ta ) ) |
21 |
20
|
ex |
|- ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ch /\ ps ) -> ( th /\ ta ) ) ) |
22 |
21
|
ex |
|- ( ph -> ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ( ch /\ ps ) -> ( th /\ ta ) ) ) ) |
23 |
1 22
|
reximdai |
|- ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ch /\ ps ) -> E. j e. Z ( th /\ ta ) ) ) |
24 |
9 23
|
mpd |
|- ( ph -> E. j e. Z ( th /\ ta ) ) |