Metamath Proof Explorer

Theorem rexuz3

Description: Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013)

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

Proof

Step Hyp Ref Expression
1 rexuz3.1 
 |-  Z = ( ZZ>= ` M )
2 ralel 
 |-  A. k e. Z k e. Z
3 fveq2 
 |-  ( j = M -> ( ZZ>= ` j ) = ( ZZ>= ` M ) )
4 3 1 eqtr4di 
 |-  ( j = M -> ( ZZ>= ` j ) = Z )
5 4 raleqdv 
 |-  ( j = M -> ( A. k e. ( ZZ>= ` j ) k e. Z <-> A. k e. Z k e. Z ) )
6 5 rspcev 
 |-  ( ( M e. ZZ /\ A. k e. Z k e. Z ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) k e. Z )
7 2 6 mpan2 
 |-  ( M e. ZZ -> E. j e. ZZ A. k e. ( ZZ>= ` j ) k e. Z )
8 7 biantrurd 
 |-  ( M e. ZZ -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ph <-> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) k e. Z /\ E. j e. ZZ A. k e. ( ZZ>= ` j ) ph ) ) )
9 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
10 9 a1d 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( ph -> k e. Z ) )
11 10 ancrd 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( ph -> ( k e. Z /\ ph ) ) )
12 11 ralimdva 
 |-  ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ph -> A. k e. ( ZZ>= ` j ) ( k e. Z /\ ph ) ) )
13 eluzelz 
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
14 13 1 eleq2s 
 |-  ( j e. Z -> j e. ZZ )
15 12 14 jctild 
 |-  ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ph -> ( j e. ZZ /\ A. k e. ( ZZ>= ` j ) ( k e. Z /\ ph ) ) ) )
16 15 imp 
 |-  ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ph ) -> ( j e. ZZ /\ A. k e. ( ZZ>= ` j ) ( k e. Z /\ ph ) ) )
17 uzid 
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
18 simpl 
 |-  ( ( k e. Z /\ ph ) -> k e. Z )
19 18 ralimi 
 |-  ( A. k e. ( ZZ>= ` j ) ( k e. Z /\ ph ) -> A. k e. ( ZZ>= ` j ) k e. Z )
20 eleq1w 
 |-  ( k = j -> ( k e. Z <-> j e. Z ) )
21 20 rspcva 
 |-  ( ( j e. ( ZZ>= ` j ) /\ A. k e. ( ZZ>= ` j ) k e. Z ) -> j e. Z )
22 17 19 21 syl2an 
 |-  ( ( j e. ZZ /\ A. k e. ( ZZ>= ` j ) ( k e. Z /\ ph ) ) -> j e. Z )
23 simpr 
 |-  ( ( k e. Z /\ ph ) -> ph )
24 23 ralimi 
 |-  ( A. k e. ( ZZ>= ` j ) ( k e. Z /\ ph ) -> A. k e. ( ZZ>= ` j ) ph )
25 24 adantl 
 |-  ( ( j e. ZZ /\ A. k e. ( ZZ>= ` j ) ( k e. Z /\ ph ) ) -> A. k e. ( ZZ>= ` j ) ph )
26 22 25 jca 
 |-  ( ( j e. ZZ /\ A. k e. ( ZZ>= ` j ) ( k e. Z /\ ph ) ) -> ( j e. Z /\ A. k e. ( ZZ>= ` j ) ph ) )
27 16 26 impbii 
 |-  ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ph ) <-> ( j e. ZZ /\ A. k e. ( ZZ>= ` j ) ( k e. Z /\ ph ) ) )
28 27 rexbii2 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ph <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. Z /\ ph ) )
29 rexanuz 
 |-  ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. Z /\ ph ) <-> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) k e. Z /\ E. j e. ZZ A. k e. ( ZZ>= ` j ) ph ) )
30 28 29 bitr2i 
 |-  ( ( E. j e. ZZ A. k e. ( ZZ>= ` j ) k e. Z /\ E. j e. ZZ A. k e. ( ZZ>= ` j ) ph ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ph )
31 8 30 syl6rbb 
 |-  ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ph ) )