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 )