This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r19.29uz

Description: A version of 19.29 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 rexuz3.1 
 |-  Z = ( ZZ>= ` M )
2 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
3 2 ex 
 |-  ( j e. Z -> ( k e. ( ZZ>= ` j ) -> k e. Z ) )
4 pm3.2 
 |-  ( ph -> ( ps -> ( ph /\ ps ) ) )
5 4 a1i 
 |-  ( j e. Z -> ( ph -> ( ps -> ( ph /\ ps ) ) ) )
6 3 5 imim12d 
 |-  ( j e. Z -> ( ( k e. Z -> ph ) -> ( k e. ( ZZ>= ` j ) -> ( ps -> ( ph /\ ps ) ) ) ) )
7 6 ralimdv2 
 |-  ( j e. Z -> ( A. k e. Z ph -> A. k e. ( ZZ>= ` j ) ( ps -> ( ph /\ ps ) ) ) )
8 7 impcom 
 |-  ( ( A. k e. Z ph /\ j e. Z ) -> A. k e. ( ZZ>= ` j ) ( ps -> ( ph /\ ps ) ) )
9 ralim 
 |-  ( A. k e. ( ZZ>= ` j ) ( ps -> ( ph /\ ps ) ) -> ( A. k e. ( ZZ>= ` j ) ps -> A. k e. ( ZZ>= ` j ) ( ph /\ ps ) ) )
10 8 9 syl 
 |-  ( ( A. k e. Z ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ps -> A. k e. ( ZZ>= ` j ) ( ph /\ ps ) ) )
11 10 reximdva 
 |-  ( A. k e. Z ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ps -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) ) )
12 11 imp 
 |-  ( ( A. k e. Z ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) )