Theorem uzrest 21701

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

Hypothesis

Ref	Expression
uzfbas.1	|- Z = ( ZZ>= ` M )

Assertion

Ref	Expression
uzrest	|- ( M e. ZZ -> ( ran ZZ>= ↾t Z ) = ( ZZ>= " Z ) )

Proof of Theorem uzrest

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zex 11386	. . . . . 6 |- ZZ e. _V
2	1	pwex 4848	. . . . 5 |- ~P ZZ e. _V
3		uzf 11690	. . . . . 6 |- ZZ>= : ZZ --> ~P ZZ
4		frn 6053	. . . . . 6 |- ( ZZ>= : ZZ --> ~P ZZ -> ran ZZ>= C_ ~P ZZ )
5	3, 4	ax-mp 5	. . . . 5 |- ran ZZ>= C_ ~P ZZ
6	2, 5	ssexi 4803	. . . 4 |- ran ZZ>= e. _V
7		uzfbas.1	. . . . 5 |- Z = ( ZZ>= ` M )
8		fvex 6201	. . . . 5 |- ( ZZ>= ` M ) e. _V
9	7, 8	eqeltri 2697	. . . 4 |- Z e. _V
10		restval 16087	. . . 4 |- ( ( ran ZZ>= e. _V /\ Z e. _V ) -> ( ran ZZ>= ↾t Z ) = ran ( x e. ran ZZ>= |-> ( x i^i Z ) ) )
11	6, 9, 10	mp2an 708	. . 3 |- ( ran ZZ>= ↾t Z ) = ran ( x e. ran ZZ>= |-> ( x i^i Z ) )
12	7	ineq2i 3811	. . . . . . . . 9 |- ( ( ZZ>= ` y ) i^i Z ) = ( ( ZZ>= ` y ) i^i ( ZZ>= ` M ) )
13		uzin 11720	. . . . . . . . . 10 |- ( ( y e. ZZ /\ M e. ZZ ) -> ( ( ZZ>= ` y ) i^i ( ZZ>= ` M ) ) = ( ZZ>= ` if ( y <_ M , M , y ) ) )
14	13	ancoms 469	. . . . . . . . 9 |- ( ( M e. ZZ /\ y e. ZZ ) -> ( ( ZZ>= ` y ) i^i ( ZZ>= ` M ) ) = ( ZZ>= ` if ( y <_ M , M , y ) ) )
15	12, 14	syl5eq 2668	. . . . . . . 8 |- ( ( M e. ZZ /\ y e. ZZ ) -> ( ( ZZ>= ` y ) i^i Z ) = ( ZZ>= ` if ( y <_ M , M , y ) ) )
16		ffn 6045	. . . . . . . . . . 11 |- ( ZZ>= : ZZ --> ~P ZZ -> ZZ>= Fn ZZ )
17	3, 16	ax-mp 5	. . . . . . . . . 10 |- ZZ>= Fn ZZ
18	17	a1i 11	. . . . . . . . 9 |- ( ( M e. ZZ /\ y e. ZZ ) -> ZZ>= Fn ZZ )
19		uzssz 11707	. . . . . . . . . . 11 |- ( ZZ>= ` M ) C_ ZZ
20	7, 19	eqsstri 3635	. . . . . . . . . 10 |- Z C_ ZZ
21	20	a1i 11	. . . . . . . . 9 |- ( ( M e. ZZ /\ y e. ZZ ) -> Z C_ ZZ )
22		inss2 3834	. . . . . . . . . 10 |- ( ( ZZ>= ` y ) i^i Z ) C_ Z
23		ifcl 4130	. . . . . . . . . . . 12 |- ( ( M e. ZZ /\ y e. ZZ ) -> if ( y <_ M , M , y ) e. ZZ )
24		uzid 11702	. . . . . . . . . . . 12 |- ( if ( y <_ M , M , y ) e. ZZ -> if ( y <_ M , M , y ) e. ( ZZ>= ` if ( y <_ M , M , y ) ) )
25	23, 24	syl 17	. . . . . . . . . . 11 |- ( ( M e. ZZ /\ y e. ZZ ) -> if ( y <_ M , M , y ) e. ( ZZ>= ` if ( y <_ M , M , y ) ) )
26	25, 15	eleqtrrd 2704	. . . . . . . . . 10 |- ( ( M e. ZZ /\ y e. ZZ ) -> if ( y <_ M , M , y ) e. ( ( ZZ>= ` y ) i^i Z ) )
27	22, 26	sseldi 3601	. . . . . . . . 9 |- ( ( M e. ZZ /\ y e. ZZ ) -> if ( y <_ M , M , y ) e. Z )
28		fnfvima 6496	. . . . . . . . 9 |- ( ( ZZ>= Fn ZZ /\ Z C_ ZZ /\ if ( y <_ M , M , y ) e. Z ) -> ( ZZ>= ` if ( y <_ M , M , y ) ) e. ( ZZ>= " Z ) )
29	18, 21, 27, 28	syl3anc 1326	. . . . . . . 8 |- ( ( M e. ZZ /\ y e. ZZ ) -> ( ZZ>= ` if ( y <_ M , M , y ) ) e. ( ZZ>= " Z ) )
30	15, 29	eqeltrd 2701	. . . . . . 7 |- ( ( M e. ZZ /\ y e. ZZ ) -> ( ( ZZ>= ` y ) i^i Z ) e. ( ZZ>= " Z ) )
31	30	ralrimiva 2966	. . . . . 6 |- ( M e. ZZ -> A. y e. ZZ ( ( ZZ>= ` y ) i^i Z ) e. ( ZZ>= " Z ) )
32		ineq1 3807	. . . . . . . . 9 |- ( x = ( ZZ>= ` y ) -> ( x i^i Z ) = ( ( ZZ>= ` y ) i^i Z ) )
33	32	eleq1d 2686	. . . . . . . 8 |- ( x = ( ZZ>= ` y ) -> ( ( x i^i Z ) e. ( ZZ>= " Z ) <-> ( ( ZZ>= ` y ) i^i Z ) e. ( ZZ>= " Z ) ) )
34	33	ralrn 6362	. . . . . . 7 |- ( 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 ) ) )
35	17, 34	ax-mp 5	. . . . . 6 |- ( A. x e. ran ZZ>= ( x i^i Z ) e. ( ZZ>= " Z ) <-> A. y e. ZZ ( ( ZZ>= ` y ) i^i Z ) e. ( ZZ>= " Z ) )
36	31, 35	sylibr 224	. . . . 5 |- ( M e. ZZ -> A. x e. ran ZZ>= ( x i^i Z ) e. ( ZZ>= " Z ) )
37		eqid 2622	. . . . . 6 |- ( x e. ran ZZ>= |-> ( x i^i Z ) ) = ( x e. ran ZZ>= |-> ( x i^i Z ) )
38	37	fmpt 6381	. . . . 5 |- ( A. x e. ran ZZ>= ( x i^i Z ) e. ( ZZ>= " Z ) <-> ( x e. ran ZZ>= |-> ( x i^i Z ) ) : ran ZZ>= --> ( ZZ>= " Z ) )
39	36, 38	sylib 208	. . . 4 |- ( M e. ZZ -> ( x e. ran ZZ>= |-> ( x i^i Z ) ) : ran ZZ>= --> ( ZZ>= " Z ) )
40		frn 6053	. . . 4 |- ( ( x e. ran ZZ>= |-> ( x i^i Z ) ) : ran ZZ>= --> ( ZZ>= " Z ) -> ran ( x e. ran ZZ>= |-> ( x i^i Z ) ) C_ ( ZZ>= " Z ) )
41	39, 40	syl 17	. . 3 |- ( M e. ZZ -> ran ( x e. ran ZZ>= |-> ( x i^i Z ) ) C_ ( ZZ>= " Z ) )
42	11, 41	syl5eqss 3649	. 2 |- ( M e. ZZ -> ( ran ZZ>= ↾t Z ) C_ ( ZZ>= " Z ) )
43	7	uztrn2 11705	. . . . . . . . 9 |- ( ( x e. Z /\ y e. ( ZZ>= ` x ) ) -> y e. Z )
44	43	ex 450	. . . . . . . 8 |- ( x e. Z -> ( y e. ( ZZ>= ` x ) -> y e. Z ) )
45	44	ssrdv 3609	. . . . . . 7 |- ( x e. Z -> ( ZZ>= ` x ) C_ Z )
46	45	adantl 482	. . . . . 6 |- ( ( M e. ZZ /\ x e. Z ) -> ( ZZ>= ` x ) C_ Z )
47		df-ss 3588	. . . . . 6 |- ( ( ZZ>= ` x ) C_ Z <-> ( ( ZZ>= ` x ) i^i Z ) = ( ZZ>= ` x ) )
48	46, 47	sylib 208	. . . . 5 |- ( ( M e. ZZ /\ x e. Z ) -> ( ( ZZ>= ` x ) i^i Z ) = ( ZZ>= ` x ) )
49	6	a1i 11	. . . . . 6 |- ( ( M e. ZZ /\ x e. Z ) -> ran ZZ>= e. _V )
50	9	a1i 11	. . . . . 6 |- ( ( M e. ZZ /\ x e. Z ) -> Z e. _V )
51	20	sseli 3599	. . . . . . . 8 |- ( x e. Z -> x e. ZZ )
52	51	adantl 482	. . . . . . 7 |- ( ( M e. ZZ /\ x e. Z ) -> x e. ZZ )
53		fnfvelrn 6356	. . . . . . 7 |- ( ( ZZ>= Fn ZZ /\ x e. ZZ ) -> ( ZZ>= ` x ) e. ran ZZ>= )
54	17, 52, 53	sylancr 695	. . . . . 6 |- ( ( M e. ZZ /\ x e. Z ) -> ( ZZ>= ` x ) e. ran ZZ>= )
55		elrestr 16089	. . . . . 6 |- ( ( ran ZZ>= e. _V /\ Z e. _V /\ ( ZZ>= ` x ) e. ran ZZ>= ) -> ( ( ZZ>= ` x ) i^i Z ) e. ( ran ZZ>= ↾t Z ) )
56	49, 50, 54, 55	syl3anc 1326	. . . . 5 |- ( ( M e. ZZ /\ x e. Z ) -> ( ( ZZ>= ` x ) i^i Z ) e. ( ran ZZ>= ↾t Z ) )
57	48, 56	eqeltrrd 2702	. . . 4 |- ( ( M e. ZZ /\ x e. Z ) -> ( ZZ>= ` x ) e. ( ran ZZ>= ↾t Z ) )
58	57	ralrimiva 2966	. . 3 |- ( M e. ZZ -> A. x e. Z ( ZZ>= ` x ) e. ( ran ZZ>= ↾t Z ) )
59		ffun 6048	. . . . 5 |- ( ZZ>= : ZZ --> ~P ZZ -> Fun ZZ>= )
60	3, 59	ax-mp 5	. . . 4 |- Fun ZZ>=
61	3	fdmi 6052	. . . . 5 |- dom ZZ>= = ZZ
62	20, 61	sseqtr4i 3638	. . . 4 |- Z C_ dom ZZ>=
63		funimass4 6247	. . . 4 |- ( ( Fun ZZ>= /\ Z C_ dom ZZ>= ) -> ( ( ZZ>= " Z ) C_ ( ran ZZ>= ↾t Z ) <-> A. x e. Z ( ZZ>= ` x ) e. ( ran ZZ>= ↾t Z ) ) )
64	60, 62, 63	mp2an 708	. . 3 |- ( ( ZZ>= " Z ) C_ ( ran ZZ>= ↾t Z ) <-> A. x e. Z ( ZZ>= ` x ) e. ( ran ZZ>= ↾t Z ) )
65	58, 64	sylibr 224	. 2 |- ( M e. ZZ -> ( ZZ>= " Z ) C_ ( ran ZZ>= ↾t Z ) )
66	42, 65	eqssd 3620	1 |- ( M e. ZZ -> ( ran ZZ>= ↾t Z ) = ( ZZ>= " Z ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   i^i cin 3573   C_ wss 3574   ifcif 4086   ~Pcpw 4158   class class class wbr 4653   |-> cmpt 4729   dom cdm 5114   ran crn 5115   "cima 5117   Fun wfun 5882   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   <_ cle 10075   ZZcz 11377   ZZ>=cuz 11687   ↾_t crest 16081

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-pre-lttri 10010  ax-pre-lttrn 10011

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-neg 10269  df-z 11378  df-uz 11688  df-rest 16083

This theorem is referenced by:  uzfbas  21702