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 ) )