Metamath Proof Explorer

Theorem rexanuz

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

Ref Expression
Assertion 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 ) )

Proof

Step Hyp Ref Expression
1 r19.26 
 |-  ( A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <-> ( A. k e. ( ZZ>= ` j ) ph /\ A. k e. ( ZZ>= ` j ) ps ) )
2 1 rexbii 
 |-  ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <-> E. j e. ZZ ( A. k e. ( ZZ>= ` j ) ph /\ A. k e. ( ZZ>= ` j ) ps ) )
3 r19.40 
 |-  ( E. j e. ZZ ( A. k e. ( ZZ>= ` j ) ph /\ 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 ) )
4 2 3 sylbi 
 |-  ( 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 ) )
5 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
6 ffn 
 |-  ( ZZ>= : ZZ --> ~P ZZ -> ZZ>= Fn ZZ )
7 raleq 
 |-  ( x = ( ZZ>= ` j ) -> ( A. k e. x ph <-> A. k e. ( ZZ>= ` j ) ph ) )
8 7 rexrn 
 |-  ( ZZ>= Fn ZZ -> ( E. x e. ran ZZ>= A. k e. x ph <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ph ) )
9 5 6 8 mp2b 
 |-  ( E. x e. ran ZZ>= A. k e. x ph <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ph )
10 raleq 
 |-  ( y = ( ZZ>= ` j ) -> ( A. k e. y ps <-> A. k e. ( ZZ>= ` j ) ps ) )
11 10 rexrn 
 |-  ( ZZ>= Fn ZZ -> ( E. y e. ran ZZ>= A. k e. y ps <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ps ) )
12 5 6 11 mp2b 
 |-  ( E. y e. ran ZZ>= A. k e. y ps <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ps )
13 uzin2 
 |-  ( ( x e. ran ZZ>= /\ y e. ran ZZ>= ) -> ( x i^i y ) e. ran ZZ>= )
14 inss1 
 |-  ( x i^i y ) C_ x
15 ssralv 
 |-  ( ( x i^i y ) C_ x -> ( A. k e. x ph -> A. k e. ( x i^i y ) ph ) )
16 14 15 ax-mp 
 |-  ( A. k e. x ph -> A. k e. ( x i^i y ) ph )
17 inss2 
 |-  ( x i^i y ) C_ y
18 ssralv 
 |-  ( ( x i^i y ) C_ y -> ( A. k e. y ps -> A. k e. ( x i^i y ) ps ) )
19 17 18 ax-mp 
 |-  ( A. k e. y ps -> A. k e. ( x i^i y ) ps )
20 16 19 anim12i 
 |-  ( ( A. k e. x ph /\ A. k e. y ps ) -> ( A. k e. ( x i^i y ) ph /\ A. k e. ( x i^i y ) ps ) )
21 r19.26 
 |-  ( A. k e. ( x i^i y ) ( ph /\ ps ) <-> ( A. k e. ( x i^i y ) ph /\ A. k e. ( x i^i y ) ps ) )
22 20 21 sylibr 
 |-  ( ( A. k e. x ph /\ A. k e. y ps ) -> A. k e. ( x i^i y ) ( ph /\ ps ) )
23 raleq 
 |-  ( z = ( x i^i y ) -> ( A. k e. z ( ph /\ ps ) <-> A. k e. ( x i^i y ) ( ph /\ ps ) ) )
24 23 rspcev 
 |-  ( ( ( x i^i y ) e. ran ZZ>= /\ A. k e. ( x i^i y ) ( ph /\ ps ) ) -> E. z e. ran ZZ>= A. k e. z ( ph /\ ps ) )
25 13 22 24 syl2an 
 |-  ( ( ( x e. ran ZZ>= /\ y e. ran ZZ>= ) /\ ( A. k e. x ph /\ A. k e. y ps ) ) -> E. z e. ran ZZ>= A. k e. z ( ph /\ ps ) )
26 25 an4s 
 |-  ( ( ( x e. ran ZZ>= /\ A. k e. x ph ) /\ ( y e. ran ZZ>= /\ A. k e. y ps ) ) -> E. z e. ran ZZ>= A. k e. z ( ph /\ ps ) )
27 26 rexlimdvaa 
 |-  ( ( x e. ran ZZ>= /\ A. k e. x ph ) -> ( E. y e. ran ZZ>= A. k e. y ps -> E. z e. ran ZZ>= A. k e. z ( ph /\ ps ) ) )
28 27 rexlimiva 
 |-  ( E. x e. ran ZZ>= A. k e. x ph -> ( E. y e. ran ZZ>= A. k e. y ps -> E. z e. ran ZZ>= A. k e. z ( ph /\ ps ) ) )
29 28 imp 
 |-  ( ( E. x e. ran ZZ>= A. k e. x ph /\ E. y e. ran ZZ>= A. k e. y ps ) -> E. z e. ran ZZ>= A. k e. z ( ph /\ ps ) )
30 raleq 
 |-  ( z = ( ZZ>= ` j ) -> ( A. k e. z ( ph /\ ps ) <-> A. k e. ( ZZ>= ` j ) ( ph /\ ps ) ) )
31 30 rexrn 
 |-  ( ZZ>= Fn ZZ -> ( E. z e. ran ZZ>= A. k e. z ( ph /\ ps ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ph /\ ps ) ) )
32 5 6 31 mp2b 
 |-  ( E. z e. ran ZZ>= A. k e. z ( ph /\ ps ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ph /\ ps ) )
33 29 32 sylib 
 |-  ( ( E. x e. ran ZZ>= A. k e. x ph /\ E. y e. ran ZZ>= A. k e. y ps ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ph /\ ps ) )
34 9 12 33 syl2anbr 
 |-  ( ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ph /\ E. j e. ZZ A. k e. ( ZZ>= ` j ) ps ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ph /\ ps ) )
35 4 34 impbii 
 |-  ( 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 ) )