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 bitr2di
 |-  ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ph ) )