Theorem rexanuz2

Description: Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013)

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

Proof

Step	Hyp	Ref	Expression
1		rexuz3.1	|- Z = ( ZZ>= ` M )
2		eluzel2	|- ( j e. ( ZZ>= ` M ) -> M e. ZZ )
3	2 1	eleq2s	|- ( j e. Z -> M e. ZZ )
4	3	a1d	|- ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ( ph /\ ps ) -> M e. ZZ ) )
5	4	rexlimiv	|- ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) -> M e. ZZ )
6	3	a1d	|- ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ph -> M e. ZZ ) )
7	6	rexlimiv	|- ( E. j e. Z A. k e. ( ZZ>= ` j ) ph -> M e. ZZ )
8	7	adantr	|- ( ( E. j e. Z A. k e. ( ZZ>= ` j ) ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) -> M e. ZZ )
9	1	rexuz3	|- ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ph /\ ps ) ) )
10		rexanuz	|- ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <-> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ph /\ E. j e. ZZ A. k e. ( ZZ>= ` j ) ps ) )
11	1	rexuz3	|- ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ph ) )
12	1	rexuz3	|- ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ps <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ps ) )
13	11 12	anbi12d	|- ( M e. ZZ -> ( ( E. j e. Z A. k e. ( ZZ>= ` j ) ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) <-> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ph /\ E. j e. ZZ A. k e. ( ZZ>= ` j ) ps ) ) )
14	10 13	bitr4id	|- ( M e. ZZ -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) ) )
15	9 14	bitrd	|- ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) ) )
16	5 8 15	pm5.21nii	|- ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) )