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

Metamath Proof Explorer

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