# Metamath Proof Explorer

## Theorem r19.2uz

Description: A version of r19.2z for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014)

Ref Expression
Hypothesis rexuz3.1
`|- Z = ( ZZ>= ` M )`
Assertion r19.2uz
`|- ( E. j e. Z A. k e. ( ZZ>= ` j ) ph -> E. k e. Z ph )`

### Proof

Step Hyp Ref Expression
1 rexuz3.1
` |-  Z = ( ZZ>= ` M )`
2 eluzelz
` |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )`
3 uzid
` |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )`
4 ne0i
` |-  ( j e. ( ZZ>= ` j ) -> ( ZZ>= ` j ) =/= (/) )`
5 2 3 4 3syl
` |-  ( j e. ( ZZ>= ` M ) -> ( ZZ>= ` j ) =/= (/) )`
6 5 1 eleq2s
` |-  ( j e. Z -> ( ZZ>= ` j ) =/= (/) )`
7 r19.2z
` |-  ( ( ( ZZ>= ` j ) =/= (/) /\ A. k e. ( ZZ>= ` j ) ph ) -> E. k e. ( ZZ>= ` j ) ph )`
8 6 7 sylan
` |-  ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ph ) -> E. k e. ( ZZ>= ` j ) ph )`
9 1 uztrn2
` |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )`
10 9 ex
` |-  ( j e. Z -> ( k e. ( ZZ>= ` j ) -> k e. Z ) )`
11 10 anim1d
` |-  ( j e. Z -> ( ( k e. ( ZZ>= ` j ) /\ ph ) -> ( k e. Z /\ ph ) ) )`
12 11 reximdv2
` |-  ( j e. Z -> ( E. k e. ( ZZ>= ` j ) ph -> E. k e. Z ph ) )`
13 12 imp
` |-  ( ( j e. Z /\ E. k e. ( ZZ>= ` j ) ph ) -> E. k e. Z ph )`
14 8 13 syldan
` |-  ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ph ) -> E. k e. Z ph )`
15 14 rexlimiva
` |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ph -> E. k e. Z ph )`