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