# 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 = ℤ ≥ M$
Assertion uzrest $⊢ M ∈ ℤ → ran ⁡ ℤ ≥ ↾ 𝑡 Z = ℤ ≥ Z$

### Proof

Step Hyp Ref Expression
1 uzfbas.1 $⊢ Z = ℤ ≥ M$
2 zex $⊢ ℤ ∈ V$
3 2 pwex $⊢ 𝒫 ℤ ∈ V$
4 uzf $⊢ ℤ ≥ : ℤ ⟶ 𝒫 ℤ$
5 frn $⊢ ℤ ≥ : ℤ ⟶ 𝒫 ℤ → ran ⁡ ℤ ≥ ⊆ 𝒫 ℤ$
6 4 5 ax-mp $⊢ ran ⁡ ℤ ≥ ⊆ 𝒫 ℤ$
7 3 6 ssexi $⊢ ran ⁡ ℤ ≥ ∈ V$
8 1 fvexi $⊢ Z ∈ V$
9 restval $⊢ ran ⁡ ℤ ≥ ∈ V ∧ Z ∈ V → ran ⁡ ℤ ≥ ↾ 𝑡 Z = ran ⁡ x ∈ ran ⁡ ℤ ≥ ⟼ x ∩ Z$
10 7 8 9 mp2an $⊢ ran ⁡ ℤ ≥ ↾ 𝑡 Z = ran ⁡ x ∈ ran ⁡ ℤ ≥ ⟼ x ∩ Z$
11 1 ineq2i $⊢ ℤ ≥ y ∩ Z = ℤ ≥ y ∩ ℤ ≥ M$
12 uzin $⊢ y ∈ ℤ ∧ M ∈ ℤ → ℤ ≥ y ∩ ℤ ≥ M = ℤ ≥ if y ≤ M M y$
13 12 ancoms $⊢ M ∈ ℤ ∧ y ∈ ℤ → ℤ ≥ y ∩ ℤ ≥ M = ℤ ≥ if y ≤ M M y$
14 11 13 syl5eq $⊢ M ∈ ℤ ∧ y ∈ ℤ → ℤ ≥ y ∩ Z = ℤ ≥ if y ≤ M M y$
15 ffn $⊢ ℤ ≥ : ℤ ⟶ 𝒫 ℤ → ℤ ≥ Fn ℤ$
16 4 15 ax-mp $⊢ ℤ ≥ Fn ℤ$
17 uzssz $⊢ ℤ ≥ M ⊆ ℤ$
18 1 17 eqsstri $⊢ Z ⊆ ℤ$
19 ifcl $⊢ M ∈ ℤ ∧ y ∈ ℤ → if y ≤ M M y ∈ ℤ$
20 uzid $⊢ if y ≤ M M y ∈ ℤ → if y ≤ M M y ∈ ℤ ≥ if y ≤ M M y$
21 19 20 syl $⊢ M ∈ ℤ ∧ y ∈ ℤ → if y ≤ M M y ∈ ℤ ≥ if y ≤ M M y$
22 21 14 eleqtrrd $⊢ M ∈ ℤ ∧ y ∈ ℤ → if y ≤ M M y ∈ ℤ ≥ y ∩ Z$
23 22 elin2d $⊢ M ∈ ℤ ∧ y ∈ ℤ → if y ≤ M M y ∈ Z$
24 fnfvima $⊢ ℤ ≥ Fn ℤ ∧ Z ⊆ ℤ ∧ if y ≤ M M y ∈ Z → ℤ ≥ if y ≤ M M y ∈ ℤ ≥ Z$
25 16 18 23 24 mp3an12i $⊢ M ∈ ℤ ∧ y ∈ ℤ → ℤ ≥ if y ≤ M M y ∈ ℤ ≥ Z$
26 14 25 eqeltrd $⊢ M ∈ ℤ ∧ y ∈ ℤ → ℤ ≥ y ∩ Z ∈ ℤ ≥ Z$
27 26 ralrimiva $⊢ M ∈ ℤ → ∀ y ∈ ℤ ℤ ≥ y ∩ Z ∈ ℤ ≥ Z$
28 ineq1 $⊢ x = ℤ ≥ y → x ∩ Z = ℤ ≥ y ∩ Z$
29 28 eleq1d $⊢ x = ℤ ≥ y → x ∩ Z ∈ ℤ ≥ Z ↔ ℤ ≥ y ∩ Z ∈ ℤ ≥ Z$
30 29 ralrn $⊢ ℤ ≥ Fn ℤ → ∀ x ∈ ran ⁡ ℤ ≥ x ∩ Z ∈ ℤ ≥ Z ↔ ∀ y ∈ ℤ ℤ ≥ y ∩ Z ∈ ℤ ≥ Z$
31 16 30 ax-mp $⊢ ∀ x ∈ ran ⁡ ℤ ≥ x ∩ Z ∈ ℤ ≥ Z ↔ ∀ y ∈ ℤ ℤ ≥ y ∩ Z ∈ ℤ ≥ Z$
32 27 31 sylibr $⊢ M ∈ ℤ → ∀ x ∈ ran ⁡ ℤ ≥ x ∩ Z ∈ ℤ ≥ Z$
33 eqid $⊢ x ∈ ran ⁡ ℤ ≥ ⟼ x ∩ Z = x ∈ ran ⁡ ℤ ≥ ⟼ x ∩ Z$
34 33 fmpt $⊢ ∀ x ∈ ran ⁡ ℤ ≥ x ∩ Z ∈ ℤ ≥ Z ↔ x ∈ ran ⁡ ℤ ≥ ⟼ x ∩ Z : ran ⁡ ℤ ≥ ⟶ ℤ ≥ Z$
35 32 34 sylib $⊢ M ∈ ℤ → x ∈ ran ⁡ ℤ ≥ ⟼ x ∩ Z : ran ⁡ ℤ ≥ ⟶ ℤ ≥ Z$
36 35 frnd $⊢ M ∈ ℤ → ran ⁡ x ∈ ran ⁡ ℤ ≥ ⟼ x ∩ Z ⊆ ℤ ≥ Z$
37 10 36 eqsstrid $⊢ M ∈ ℤ → ran ⁡ ℤ ≥ ↾ 𝑡 Z ⊆ ℤ ≥ Z$
38 1 uztrn2 $⊢ x ∈ Z ∧ y ∈ ℤ ≥ x → y ∈ Z$
39 38 ex $⊢ x ∈ Z → y ∈ ℤ ≥ x → y ∈ Z$
40 39 ssrdv $⊢ x ∈ Z → ℤ ≥ x ⊆ Z$
41 40 adantl $⊢ M ∈ ℤ ∧ x ∈ Z → ℤ ≥ x ⊆ Z$
42 df-ss $⊢ ℤ ≥ x ⊆ Z ↔ ℤ ≥ x ∩ Z = ℤ ≥ x$
43 41 42 sylib $⊢ M ∈ ℤ ∧ x ∈ Z → ℤ ≥ x ∩ Z = ℤ ≥ x$
44 18 sseli $⊢ x ∈ Z → x ∈ ℤ$
45 44 adantl $⊢ M ∈ ℤ ∧ x ∈ Z → x ∈ ℤ$
46 fnfvelrn $⊢ ℤ ≥ Fn ℤ ∧ x ∈ ℤ → ℤ ≥ x ∈ ran ⁡ ℤ ≥$
47 16 45 46 sylancr $⊢ M ∈ ℤ ∧ x ∈ Z → ℤ ≥ x ∈ ran ⁡ ℤ ≥$
48 elrestr $⊢ ran ⁡ ℤ ≥ ∈ V ∧ Z ∈ V ∧ ℤ ≥ x ∈ ran ⁡ ℤ ≥ → ℤ ≥ x ∩ Z ∈ ran ⁡ ℤ ≥ ↾ 𝑡 Z$
49 7 8 47 48 mp3an12i $⊢ M ∈ ℤ ∧ x ∈ Z → ℤ ≥ x ∩ Z ∈ ran ⁡ ℤ ≥ ↾ 𝑡 Z$
50 43 49 eqeltrrd $⊢ M ∈ ℤ ∧ x ∈ Z → ℤ ≥ x ∈ ran ⁡ ℤ ≥ ↾ 𝑡 Z$
51 50 ralrimiva $⊢ M ∈ ℤ → ∀ x ∈ Z ℤ ≥ x ∈ ran ⁡ ℤ ≥ ↾ 𝑡 Z$
52 ffun $⊢ ℤ ≥ : ℤ ⟶ 𝒫 ℤ → Fun ⁡ ℤ ≥$
53 4 52 ax-mp $⊢ Fun ⁡ ℤ ≥$
54 4 fdmi $⊢ dom ⁡ ℤ ≥ = ℤ$
55 18 54 sseqtrri $⊢ Z ⊆ dom ⁡ ℤ ≥$
56 funimass4 $⊢ Fun ⁡ ℤ ≥ ∧ Z ⊆ dom ⁡ ℤ ≥ → ℤ ≥ Z ⊆ ran ⁡ ℤ ≥ ↾ 𝑡 Z ↔ ∀ x ∈ Z ℤ ≥ x ∈ ran ⁡ ℤ ≥ ↾ 𝑡 Z$
57 53 55 56 mp2an $⊢ ℤ ≥ Z ⊆ ran ⁡ ℤ ≥ ↾ 𝑡 Z ↔ ∀ x ∈ Z ℤ ≥ x ∈ ran ⁡ ℤ ≥ ↾ 𝑡 Z$
58 51 57 sylibr $⊢ M ∈ ℤ → ℤ ≥ Z ⊆ ran ⁡ ℤ ≥ ↾ 𝑡 Z$
59 37 58 eqssd $⊢ M ∈ ℤ → ran ⁡ ℤ ≥ ↾ 𝑡 Z = ℤ ≥ Z$