Metamath Proof Explorer

Theorem uzrest

Description: The restriction of the set of upper sets of integers to an upper set of integers is the set of upper sets of integers based at a point above the cutoff. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypothesis uzfbas.1 
|- Z = ( ZZ>= ` M )
Assertion uzrest 
|- ( M e. ZZ -> ( ran ZZ>= |`t Z ) = ( ZZ>= " Z ) )

Proof

Step Hyp Ref Expression
1 uzfbas.1 
 |-  Z = ( ZZ>= ` M )
2 zex 
 |-  ZZ e. _V
3 2 pwex 
 |-  ~P ZZ e. _V
4 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
5 frn 
 |-  ( ZZ>= : ZZ --> ~P ZZ -> ran ZZ>= C_ ~P ZZ )
6 4 5 ax-mp 
 |-  ran ZZ>= C_ ~P ZZ
7 3 6 ssexi 
 |-  ran ZZ>= e. _V
8 1 fvexi 
 |-  Z e. _V
9 restval 
 |-  ( ( ran ZZ>= e. _V /\ Z e. _V ) -> ( ran ZZ>= |`t Z ) = ran ( x e. ran ZZ>= |-> ( x i^i Z ) ) )
10 7 8 9 mp2an 
 |-  ( ran ZZ>= |`t Z ) = ran ( x e. ran ZZ>= |-> ( x i^i Z ) )
11 1 ineq2i 
 |-  ( ( ZZ>= ` y ) i^i Z ) = ( ( ZZ>= ` y ) i^i ( ZZ>= ` M ) )
12 uzin 
 |-  ( ( y e. ZZ /\ M e. ZZ ) -> ( ( ZZ>= ` y ) i^i ( ZZ>= ` M ) ) = ( ZZ>= ` if ( y <_ M , M , y ) ) )
13 12 ancoms 
 |-  ( ( M e. ZZ /\ y e. ZZ ) -> ( ( ZZ>= ` y ) i^i ( ZZ>= ` M ) ) = ( ZZ>= ` if ( y <_ M , M , y ) ) )
14 11 13 syl5eq 
 |-  ( ( M e. ZZ /\ y e. ZZ ) -> ( ( ZZ>= ` y ) i^i Z ) = ( ZZ>= ` if ( y <_ M , M , y ) ) )
15 ffn 
 |-  ( ZZ>= : ZZ --> ~P ZZ -> ZZ>= Fn ZZ )
16 4 15 ax-mp 
 |-  ZZ>= Fn ZZ
17 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
18 1 17 eqsstri 
 |-  Z C_ ZZ
19 ifcl 
 |-  ( ( M e. ZZ /\ y e. ZZ ) -> if ( y <_ M , M , y ) e. ZZ )
20 uzid 
 |-  ( if ( y <_ M , M , y ) e. ZZ -> if ( y <_ M , M , y ) e. ( ZZ>= ` if ( y <_ M , M , y ) ) )
21 19 20 syl 
 |-  ( ( M e. ZZ /\ y e. ZZ ) -> if ( y <_ M , M , y ) e. ( ZZ>= ` if ( y <_ M , M , y ) ) )
22 21 14 eleqtrrd 
 |-  ( ( M e. ZZ /\ y e. ZZ ) -> if ( y <_ M , M , y ) e. ( ( ZZ>= ` y ) i^i Z ) )
23 22 elin2d 
 |-  ( ( M e. ZZ /\ y e. ZZ ) -> if ( y <_ M , M , y ) e. Z )
24 fnfvima 
 |-  ( ( ZZ>= Fn ZZ /\ Z C_ ZZ /\ if ( y <_ M , M , y ) e. Z ) -> ( ZZ>= ` if ( y <_ M , M , y ) ) e. ( ZZ>= " Z ) )
25 16 18 23 24 mp3an12i 
 |-  ( ( M e. ZZ /\ y e. ZZ ) -> ( ZZ>= ` if ( y <_ M , M , y ) ) e. ( ZZ>= " Z ) )
26 14 25 eqeltrd 
 |-  ( ( M e. ZZ /\ y e. ZZ ) -> ( ( ZZ>= ` y ) i^i Z ) e. ( ZZ>= " Z ) )
27 26 ralrimiva 
 |-  ( M e. ZZ -> A. y e. ZZ ( ( ZZ>= ` y ) i^i Z ) e. ( ZZ>= " Z ) )
28 ineq1 
 |-  ( x = ( ZZ>= ` y ) -> ( x i^i Z ) = ( ( ZZ>= ` y ) i^i Z ) )
29 28 eleq1d 
 |-  ( x = ( ZZ>= ` y ) -> ( ( x i^i Z ) e. ( ZZ>= " Z ) <-> ( ( ZZ>= ` y ) i^i Z ) e. ( ZZ>= " Z ) ) )
30 29 ralrn 
 |-  ( ZZ>= Fn ZZ -> ( A. x e. ran ZZ>= ( x i^i Z ) e. ( ZZ>= " Z ) <-> A. y e. ZZ ( ( ZZ>= ` y ) i^i Z ) e. ( ZZ>= " Z ) ) )
31 16 30 ax-mp 
 |-  ( A. x e. ran ZZ>= ( x i^i Z ) e. ( ZZ>= " Z ) <-> A. y e. ZZ ( ( ZZ>= ` y ) i^i Z ) e. ( ZZ>= " Z ) )
32 27 31 sylibr 
 |-  ( M e. ZZ -> A. x e. ran ZZ>= ( x i^i Z ) e. ( ZZ>= " Z ) )
33 eqid 
 |-  ( x e. ran ZZ>= |-> ( x i^i Z ) ) = ( x e. ran ZZ>= |-> ( x i^i Z ) )
34 33 fmpt 
 |-  ( A. x e. ran ZZ>= ( x i^i Z ) e. ( ZZ>= " Z ) <-> ( x e. ran ZZ>= |-> ( x i^i Z ) ) : ran ZZ>= --> ( ZZ>= " Z ) )
35 32 34 sylib 
 |-  ( M e. ZZ -> ( x e. ran ZZ>= |-> ( x i^i Z ) ) : ran ZZ>= --> ( ZZ>= " Z ) )
36 35 frnd 
 |-  ( M e. ZZ -> ran ( x e. ran ZZ>= |-> ( x i^i Z ) ) C_ ( ZZ>= " Z ) )
37 10 36 eqsstrid 
 |-  ( M e. ZZ -> ( ran ZZ>= |`t Z ) C_ ( ZZ>= " Z ) )
38 1 uztrn2 
 |-  ( ( x e. Z /\ y e. ( ZZ>= ` x ) ) -> y e. Z )
39 38 ex 
 |-  ( x e. Z -> ( y e. ( ZZ>= ` x ) -> y e. Z ) )
40 39 ssrdv 
 |-  ( x e. Z -> ( ZZ>= ` x ) C_ Z )
41 40 adantl 
 |-  ( ( M e. ZZ /\ x e. Z ) -> ( ZZ>= ` x ) C_ Z )
42 df-ss 
 |-  ( ( ZZ>= ` x ) C_ Z <-> ( ( ZZ>= ` x ) i^i Z ) = ( ZZ>= ` x ) )
43 41 42 sylib 
 |-  ( ( M e. ZZ /\ x e. Z ) -> ( ( ZZ>= ` x ) i^i Z ) = ( ZZ>= ` x ) )
44 18 sseli 
 |-  ( x e. Z -> x e. ZZ )
45 44 adantl 
 |-  ( ( M e. ZZ /\ x e. Z ) -> x e. ZZ )
46 fnfvelrn 
 |-  ( ( ZZ>= Fn ZZ /\ x e. ZZ ) -> ( ZZ>= ` x ) e. ran ZZ>= )
47 16 45 46 sylancr 
 |-  ( ( M e. ZZ /\ x e. Z ) -> ( ZZ>= ` x ) e. ran ZZ>= )
48 elrestr 
 |-  ( ( ran ZZ>= e. _V /\ Z e. _V /\ ( ZZ>= ` x ) e. ran ZZ>= ) -> ( ( ZZ>= ` x ) i^i Z ) e. ( ran ZZ>= |`t Z ) )
49 7 8 47 48 mp3an12i 
 |-  ( ( M e. ZZ /\ x e. Z ) -> ( ( ZZ>= ` x ) i^i Z ) e. ( ran ZZ>= |`t Z ) )
50 43 49 eqeltrrd 
 |-  ( ( M e. ZZ /\ x e. Z ) -> ( ZZ>= ` x ) e. ( ran ZZ>= |`t Z ) )
51 50 ralrimiva 
 |-  ( M e. ZZ -> A. x e. Z ( ZZ>= ` x ) e. ( ran ZZ>= |`t Z ) )
52 ffun 
 |-  ( ZZ>= : ZZ --> ~P ZZ -> Fun ZZ>= )
53 4 52 ax-mp 
 |-  Fun ZZ>=
54 4 fdmi 
 |-  dom ZZ>= = ZZ
55 18 54 sseqtrri 
 |-  Z C_ dom ZZ>=
56 funimass4 
 |-  ( ( Fun ZZ>= /\ Z C_ dom ZZ>= ) -> ( ( ZZ>= " Z ) C_ ( ran ZZ>= |`t Z ) <-> A. x e. Z ( ZZ>= ` x ) e. ( ran ZZ>= |`t Z ) ) )
57 53 55 56 mp2an 
 |-  ( ( ZZ>= " Z ) C_ ( ran ZZ>= |`t Z ) <-> A. x e. Z ( ZZ>= ` x ) e. ( ran ZZ>= |`t Z ) )
58 51 57 sylibr 
 |-  ( M e. ZZ -> ( ZZ>= " Z ) C_ ( ran ZZ>= |`t Z ) )
59 37 58 eqssd 
 |-  ( M e. ZZ -> ( ran ZZ>= |`t Z ) = ( ZZ>= " Z ) )