Theorem uzrest 21511

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	⊢ 𝑍 = (ℤ≥‘𝑀)

Assertion

Ref	Expression
uzrest	⊢ (𝑀 ∈ ℤ → (ran ℤ≥ ↾t 𝑍) = (ℤ≥ “ 𝑍))

Proof of Theorem uzrest

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zex 11263	. . . . . 6 ⊢ ℤ ∈ V
2	1	pwex 4774	. . . . 5 ⊢ 𝒫 ℤ ∈ V
3		uzf 11566	. . . . . 6 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
4		frn 5966	. . . . . 6 ⊢ (ℤ≥:ℤ⟶𝒫 ℤ → ran ℤ≥ ⊆ 𝒫 ℤ)
5	3, 4	ax-mp 5	. . . . 5 ⊢ ran ℤ≥ ⊆ 𝒫 ℤ
6	2, 5	ssexi 4731	. . . 4 ⊢ ran ℤ≥ ∈ V
7		uzfbas.1	. . . . 5 ⊢ 𝑍 = (ℤ≥‘𝑀)
8		fvex 6113	. . . . 5 ⊢ (ℤ≥‘𝑀) ∈ V
9	7, 8	eqeltri 2684	. . . 4 ⊢ 𝑍 ∈ V
10		restval 15910	. . . 4 ⊢ ((ran ℤ≥ ∈ V ∧ 𝑍 ∈ V) → (ran ℤ≥ ↾t 𝑍) = ran (𝑥 ∈ ran ℤ≥ ↦ (𝑥 ∩ 𝑍)))
11	6, 9, 10	mp2an 704	. . 3 ⊢ (ran ℤ≥ ↾t 𝑍) = ran (𝑥 ∈ ran ℤ≥ ↦ (𝑥 ∩ 𝑍))
12	7	ineq2i 3773	. . . . . . . . 9 ⊢ ((ℤ≥‘𝑦) ∩ 𝑍) = ((ℤ≥‘𝑦) ∩ (ℤ≥‘𝑀))
13		uzin 11596	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((ℤ≥‘𝑦) ∩ (ℤ≥‘𝑀)) = (ℤ≥‘if(𝑦 ≤ 𝑀, 𝑀, 𝑦)))
14	13	ancoms 468	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((ℤ≥‘𝑦) ∩ (ℤ≥‘𝑀)) = (ℤ≥‘if(𝑦 ≤ 𝑀, 𝑀, 𝑦)))
15	12, 14	syl5eq 2656	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((ℤ≥‘𝑦) ∩ 𝑍) = (ℤ≥‘if(𝑦 ≤ 𝑀, 𝑀, 𝑦)))
16		ffn 5958	. . . . . . . . . . 11 ⊢ (ℤ≥:ℤ⟶𝒫 ℤ → ℤ≥ Fn ℤ)
17	3, 16	ax-mp 5	. . . . . . . . . 10 ⊢ ℤ≥ Fn ℤ
18	17	a1i 11	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ℤ≥ Fn ℤ)
19		uzssz 11583	. . . . . . . . . . 11 ⊢ (ℤ≥‘𝑀) ⊆ ℤ
20	7, 19	eqsstri 3598	. . . . . . . . . 10 ⊢ 𝑍 ⊆ ℤ
21	20	a1i 11	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑍 ⊆ ℤ)
22		inss2 3796	. . . . . . . . . 10 ⊢ ((ℤ≥‘𝑦) ∩ 𝑍) ⊆ 𝑍
23		ifcl 4080	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ) → if(𝑦 ≤ 𝑀, 𝑀, 𝑦) ∈ ℤ)
24		uzid 11578	. . . . . . . . . . . 12 ⊢ (if(𝑦 ≤ 𝑀, 𝑀, 𝑦) ∈ ℤ → if(𝑦 ≤ 𝑀, 𝑀, 𝑦) ∈ (ℤ≥‘if(𝑦 ≤ 𝑀, 𝑀, 𝑦)))
25	23, 24	syl 17	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ) → if(𝑦 ≤ 𝑀, 𝑀, 𝑦) ∈ (ℤ≥‘if(𝑦 ≤ 𝑀, 𝑀, 𝑦)))
26	25, 15	eleqtrrd 2691	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ) → if(𝑦 ≤ 𝑀, 𝑀, 𝑦) ∈ ((ℤ≥‘𝑦) ∩ 𝑍))
27	22, 26	sseldi 3566	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ) → if(𝑦 ≤ 𝑀, 𝑀, 𝑦) ∈ 𝑍)
28		fnfvima 6400	. . . . . . . . 9 ⊢ ((ℤ≥ Fn ℤ ∧ 𝑍 ⊆ ℤ ∧ if(𝑦 ≤ 𝑀, 𝑀, 𝑦) ∈ 𝑍) → (ℤ≥‘if(𝑦 ≤ 𝑀, 𝑀, 𝑦)) ∈ (ℤ≥ “ 𝑍))
29	18, 21, 27, 28	syl3anc 1318	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (ℤ≥‘if(𝑦 ≤ 𝑀, 𝑀, 𝑦)) ∈ (ℤ≥ “ 𝑍))
30	15, 29	eqeltrd 2688	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((ℤ≥‘𝑦) ∩ 𝑍) ∈ (ℤ≥ “ 𝑍))
31	30	ralrimiva 2949	. . . . . 6 ⊢ (𝑀 ∈ ℤ → ∀𝑦 ∈ ℤ ((ℤ≥‘𝑦) ∩ 𝑍) ∈ (ℤ≥ “ 𝑍))
32		ineq1 3769	. . . . . . . . 9 ⊢ (𝑥 = (ℤ≥‘𝑦) → (𝑥 ∩ 𝑍) = ((ℤ≥‘𝑦) ∩ 𝑍))
33	32	eleq1d 2672	. . . . . . . 8 ⊢ (𝑥 = (ℤ≥‘𝑦) → ((𝑥 ∩ 𝑍) ∈ (ℤ≥ “ 𝑍) ↔ ((ℤ≥‘𝑦) ∩ 𝑍) ∈ (ℤ≥ “ 𝑍)))
34	33	ralrn 6270	. . . . . . 7 ⊢ (ℤ≥ Fn ℤ → (∀𝑥 ∈ ran ℤ≥(𝑥 ∩ 𝑍) ∈ (ℤ≥ “ 𝑍) ↔ ∀𝑦 ∈ ℤ ((ℤ≥‘𝑦) ∩ 𝑍) ∈ (ℤ≥ “ 𝑍)))
35	17, 34	ax-mp 5	. . . . . 6 ⊢ (∀𝑥 ∈ ran ℤ≥(𝑥 ∩ 𝑍) ∈ (ℤ≥ “ 𝑍) ↔ ∀𝑦 ∈ ℤ ((ℤ≥‘𝑦) ∩ 𝑍) ∈ (ℤ≥ “ 𝑍))
36	31, 35	sylibr 223	. . . . 5 ⊢ (𝑀 ∈ ℤ → ∀𝑥 ∈ ran ℤ≥(𝑥 ∩ 𝑍) ∈ (ℤ≥ “ 𝑍))
37		eqid 2610	. . . . . 6 ⊢ (𝑥 ∈ ran ℤ≥ ↦ (𝑥 ∩ 𝑍)) = (𝑥 ∈ ran ℤ≥ ↦ (𝑥 ∩ 𝑍))
38	37	fmpt 6289	. . . . 5 ⊢ (∀𝑥 ∈ ran ℤ≥(𝑥 ∩ 𝑍) ∈ (ℤ≥ “ 𝑍) ↔ (𝑥 ∈ ran ℤ≥ ↦ (𝑥 ∩ 𝑍)):ran ℤ≥⟶(ℤ≥ “ 𝑍))
39	36, 38	sylib 207	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝑥 ∈ ran ℤ≥ ↦ (𝑥 ∩ 𝑍)):ran ℤ≥⟶(ℤ≥ “ 𝑍))
40		frn 5966	. . . 4 ⊢ ((𝑥 ∈ ran ℤ≥ ↦ (𝑥 ∩ 𝑍)):ran ℤ≥⟶(ℤ≥ “ 𝑍) → ran (𝑥 ∈ ran ℤ≥ ↦ (𝑥 ∩ 𝑍)) ⊆ (ℤ≥ “ 𝑍))
41	39, 40	syl 17	. . 3 ⊢ (𝑀 ∈ ℤ → ran (𝑥 ∈ ran ℤ≥ ↦ (𝑥 ∩ 𝑍)) ⊆ (ℤ≥ “ 𝑍))
42	11, 41	syl5eqss 3612	. 2 ⊢ (𝑀 ∈ ℤ → (ran ℤ≥ ↾t 𝑍) ⊆ (ℤ≥ “ 𝑍))
43	7	uztrn2 11581	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑍 ∧ 𝑦 ∈ (ℤ≥‘𝑥)) → 𝑦 ∈ 𝑍)
44	43	ex 449	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑍 → (𝑦 ∈ (ℤ≥‘𝑥) → 𝑦 ∈ 𝑍))
45	44	ssrdv 3574	. . . . . . 7 ⊢ (𝑥 ∈ 𝑍 → (ℤ≥‘𝑥) ⊆ 𝑍)
46	45	adantl 481	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈ 𝑍) → (ℤ≥‘𝑥) ⊆ 𝑍)
47		df-ss 3554	. . . . . 6 ⊢ ((ℤ≥‘𝑥) ⊆ 𝑍 ↔ ((ℤ≥‘𝑥) ∩ 𝑍) = (ℤ≥‘𝑥))
48	46, 47	sylib 207	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈ 𝑍) → ((ℤ≥‘𝑥) ∩ 𝑍) = (ℤ≥‘𝑥))
49	6	a1i 11	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈ 𝑍) → ran ℤ≥ ∈ V)
50	9	a1i 11	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈ 𝑍) → 𝑍 ∈ V)
51	20	sseli 3564	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑍 → 𝑥 ∈ ℤ)
52	51	adantl 481	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈ 𝑍) → 𝑥 ∈ ℤ)
53		fnfvelrn 6264	. . . . . . 7 ⊢ ((ℤ≥ Fn ℤ ∧ 𝑥 ∈ ℤ) → (ℤ≥‘𝑥) ∈ ran ℤ≥)
54	17, 52, 53	sylancr 694	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈ 𝑍) → (ℤ≥‘𝑥) ∈ ran ℤ≥)
55		elrestr 15912	. . . . . 6 ⊢ ((ran ℤ≥ ∈ V ∧ 𝑍 ∈ V ∧ (ℤ≥‘𝑥) ∈ ran ℤ≥) → ((ℤ≥‘𝑥) ∩ 𝑍) ∈ (ran ℤ≥ ↾t 𝑍))
56	49, 50, 54, 55	syl3anc 1318	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈ 𝑍) → ((ℤ≥‘𝑥) ∩ 𝑍) ∈ (ran ℤ≥ ↾t 𝑍))
57	48, 56	eqeltrrd 2689	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈ 𝑍) → (ℤ≥‘𝑥) ∈ (ran ℤ≥ ↾t 𝑍))
58	57	ralrimiva 2949	. . 3 ⊢ (𝑀 ∈ ℤ → ∀𝑥 ∈ 𝑍 (ℤ≥‘𝑥) ∈ (ran ℤ≥ ↾t 𝑍))
59		ffun 5961	. . . . 5 ⊢ (ℤ≥:ℤ⟶𝒫 ℤ → Fun ℤ≥)
60	3, 59	ax-mp 5	. . . 4 ⊢ Fun ℤ≥
61	3	fdmi 5965	. . . . 5 ⊢ dom ℤ≥ = ℤ
62	20, 61	sseqtr4i 3601	. . . 4 ⊢ 𝑍 ⊆ dom ℤ≥
63		funimass4 6157	. . . 4 ⊢ ((Fun ℤ≥ ∧ 𝑍 ⊆ dom ℤ≥) → ((ℤ≥ “ 𝑍) ⊆ (ran ℤ≥ ↾t 𝑍) ↔ ∀𝑥 ∈ 𝑍 (ℤ≥‘𝑥) ∈ (ran ℤ≥ ↾t 𝑍)))
64	60, 62, 63	mp2an 704	. . 3 ⊢ ((ℤ≥ “ 𝑍) ⊆ (ran ℤ≥ ↾t 𝑍) ↔ ∀𝑥 ∈ 𝑍 (ℤ≥‘𝑥) ∈ (ran ℤ≥ ↾t 𝑍))
65	58, 64	sylibr 223	. 2 ⊢ (𝑀 ∈ ℤ → (ℤ≥ “ 𝑍) ⊆ (ran ℤ≥ ↾t 𝑍))
66	42, 65	eqssd 3585	1 ⊢ (𝑀 ∈ ℤ → (ran ℤ≥ ↾t 𝑍) = (ℤ≥ “ 𝑍))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540  ifcif 4036  𝒫 cpw 4108   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038  ran crn 5039   “ cima 5041  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ≤ cle 9954  ℤcz 11254  ℤ_≥cuz 11563   ↾_t crest 15904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-pre-lttri 9889  ax-pre-lttrn 9890

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-neg 10148  df-z 11255  df-uz 11564  df-rest 15906

This theorem is referenced by:  uzfbas  21512