This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion uzrest ( 𝑀 ∈ ℤ → ( ran ℤ≥ ↾t 𝑍 ) = ( ℤ≥ “ 𝑍 ) )

Proof

Step Hyp Ref Expression
1 uzfbas.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
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 ⊢ 𝑍 ∈ V
9 restval ⊢ ( ( ran ℤ≥ ∈ V ∧ 𝑍 ∈ V ) → ( ran ℤ≥ ↾t 𝑍 ) = ran ( 𝑥 ∈ ran ℤ≥ ↦ ( 𝑥 ∩ 𝑍 ) ) )
10 7 8 9 mp2an ⊢ ( ran ℤ≥ ↾t 𝑍 ) = ran ( 𝑥 ∈ ran ℤ≥ ↦ ( 𝑥 ∩ 𝑍 ) )
11 1 ineq2i ⊢ ( ( ℤ≥ ‘ 𝑦 ) ∩ 𝑍 ) = ( ( ℤ≥ ‘ 𝑦 ) ∩ ( ℤ≥ ‘ 𝑀 ) )
12 uzin ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ℤ≥ ‘ 𝑦 ) ∩ ( ℤ≥ ‘ 𝑀 ) ) = ( ℤ≥ ‘ if ( 𝑦 ≤ 𝑀 , 𝑀 , 𝑦 ) ) )
13 12 ancoms ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ℤ≥ ‘ 𝑦 ) ∩ ( ℤ≥ ‘ 𝑀 ) ) = ( ℤ≥ ‘ if ( 𝑦 ≤ 𝑀 , 𝑀 , 𝑦 ) ) )
14 11 13 eqtrid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ℤ≥ ‘ 𝑦 ) ∩ 𝑍 ) = ( ℤ≥ ‘ if ( 𝑦 ≤ 𝑀 , 𝑀 , 𝑦 ) ) )
15 ffn ⊢ ( ℤ≥ : ℤ ⟶ 𝒫 ℤ → ℤ≥ Fn ℤ )
16 4 15 ax-mp ⊢ ℤ≥ Fn ℤ
17 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
18 1 17 eqsstri ⊢ 𝑍 ⊆ ℤ
19 ifcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → if ( 𝑦 ≤ 𝑀 , 𝑀 , 𝑦 ) ∈ ℤ )
20 uzid ⊢ ( if ( 𝑦 ≤ 𝑀 , 𝑀 , 𝑦 ) ∈ ℤ → if ( 𝑦 ≤ 𝑀 , 𝑀 , 𝑦 ) ∈ ( ℤ≥ ‘ if ( 𝑦 ≤ 𝑀 , 𝑀 , 𝑦 ) ) )
21 19 20 syl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → if ( 𝑦 ≤ 𝑀 , 𝑀 , 𝑦 ) ∈ ( ℤ≥ ‘ if ( 𝑦 ≤ 𝑀 , 𝑀 , 𝑦 ) ) )
22 21 14 eleqtrrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → if ( 𝑦 ≤ 𝑀 , 𝑀 , 𝑦 ) ∈ ( ( ℤ≥ ‘ 𝑦 ) ∩ 𝑍 ) )
23 22 elin2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → if ( 𝑦 ≤ 𝑀 , 𝑀 , 𝑦 ) ∈ 𝑍 )
24 fnfvima ⊢ ( ( ℤ≥ Fn ℤ ∧ 𝑍 ⊆ ℤ ∧ if ( 𝑦 ≤ 𝑀 , 𝑀 , 𝑦 ) ∈ 𝑍 ) → ( ℤ≥ ‘ if ( 𝑦 ≤ 𝑀 , 𝑀 , 𝑦 ) ) ∈ ( ℤ≥ “ 𝑍 ) )
25 16 18 23 24 mp3an12i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ℤ≥ ‘ if ( 𝑦 ≤ 𝑀 , 𝑀 , 𝑦 ) ) ∈ ( ℤ≥ “ 𝑍 ) )
26 14 25 eqeltrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ℤ≥ ‘ 𝑦 ) ∩ 𝑍 ) ∈ ( ℤ≥ “ 𝑍 ) )
27 26 ralrimiva ⊢ ( 𝑀 ∈ ℤ → ∀ 𝑦 ∈ ℤ ( ( ℤ≥ ‘ 𝑦 ) ∩ 𝑍 ) ∈ ( ℤ≥ “ 𝑍 ) )
28 ineq1 ⊢ ( 𝑥 = ( ℤ≥ ‘ 𝑦 ) → ( 𝑥 ∩ 𝑍 ) = ( ( ℤ≥ ‘ 𝑦 ) ∩ 𝑍 ) )
29 28 eleq1d ⊢ ( 𝑥 = ( ℤ≥ ‘ 𝑦 ) → ( ( 𝑥 ∩ 𝑍 ) ∈ ( ℤ≥ “ 𝑍 ) ↔ ( ( ℤ≥ ‘ 𝑦 ) ∩ 𝑍 ) ∈ ( ℤ≥ “ 𝑍 ) ) )
30 29 ralrn ⊢ ( ℤ≥ Fn ℤ → ( ∀ 𝑥 ∈ ran ℤ≥ ( 𝑥 ∩ 𝑍 ) ∈ ( ℤ≥ “ 𝑍 ) ↔ ∀ 𝑦 ∈ ℤ ( ( ℤ≥ ‘ 𝑦 ) ∩ 𝑍 ) ∈ ( ℤ≥ “ 𝑍 ) ) )
31 16 30 ax-mp ⊢ ( ∀ 𝑥 ∈ ran ℤ≥ ( 𝑥 ∩ 𝑍 ) ∈ ( ℤ≥ “ 𝑍 ) ↔ ∀ 𝑦 ∈ ℤ ( ( ℤ≥ ‘ 𝑦 ) ∩ 𝑍 ) ∈ ( ℤ≥ “ 𝑍 ) )
32 27 31 sylibr ⊢ ( 𝑀 ∈ ℤ → ∀ 𝑥 ∈ ran ℤ≥ ( 𝑥 ∩ 𝑍 ) ∈ ( ℤ≥ “ 𝑍 ) )
33 eqid ⊢ ( 𝑥 ∈ ran ℤ≥ ↦ ( 𝑥 ∩ 𝑍 ) ) = ( 𝑥 ∈ ran ℤ≥ ↦ ( 𝑥 ∩ 𝑍 ) )
34 33 fmpt ⊢ ( ∀ 𝑥 ∈ ran ℤ≥ ( 𝑥 ∩ 𝑍 ) ∈ ( ℤ≥ “ 𝑍 ) ↔ ( 𝑥 ∈ ran ℤ≥ ↦ ( 𝑥 ∩ 𝑍 ) ) : ran ℤ≥ ⟶ ( ℤ≥ “ 𝑍 ) )
35 32 34 sylib ⊢ ( 𝑀 ∈ ℤ → ( 𝑥 ∈ ran ℤ≥ ↦ ( 𝑥 ∩ 𝑍 ) ) : ran ℤ≥ ⟶ ( ℤ≥ “ 𝑍 ) )
36 35 frnd ⊢ ( 𝑀 ∈ ℤ → ran ( 𝑥 ∈ ran ℤ≥ ↦ ( 𝑥 ∩ 𝑍 ) ) ⊆ ( ℤ≥ “ 𝑍 ) )
37 10 36 eqsstrid ⊢ ( 𝑀 ∈ ℤ → ( ran ℤ≥ ↾t 𝑍 ) ⊆ ( ℤ≥ “ 𝑍 ) )
38 1 uztrn2 ⊢ ( ( 𝑥 ∈ 𝑍 ∧ 𝑦 ∈ ( ℤ≥ ‘ 𝑥 ) ) → 𝑦 ∈ 𝑍 )
39 38 ex ⊢ ( 𝑥 ∈ 𝑍 → ( 𝑦 ∈ ( ℤ≥ ‘ 𝑥 ) → 𝑦 ∈ 𝑍 ) )
40 39 ssrdv ⊢ ( 𝑥 ∈ 𝑍 → ( ℤ≥ ‘ 𝑥 ) ⊆ 𝑍 )
41 40 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑥 ) ⊆ 𝑍 )
42 dfss2 ⊢ ( ( ℤ≥ ‘ 𝑥 ) ⊆ 𝑍 ↔ ( ( ℤ≥ ‘ 𝑥 ) ∩ 𝑍 ) = ( ℤ≥ ‘ 𝑥 ) )
43 41 42 sylib ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ 𝑍 ) → ( ( ℤ≥ ‘ 𝑥 ) ∩ 𝑍 ) = ( ℤ≥ ‘ 𝑥 ) )
44 18 sseli ⊢ ( 𝑥 ∈ 𝑍 → 𝑥 ∈ ℤ )
45 44 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ 𝑍 ) → 𝑥 ∈ ℤ )
46 fnfvelrn ⊢ ( ( ℤ≥ Fn ℤ ∧ 𝑥 ∈ ℤ ) → ( ℤ≥ ‘ 𝑥 ) ∈ ran ℤ≥ )
47 16 45 46 sylancr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑥 ) ∈ ran ℤ≥ )
48 elrestr ⊢ ( ( ran ℤ≥ ∈ V ∧ 𝑍 ∈ V ∧ ( ℤ≥ ‘ 𝑥 ) ∈ ran ℤ≥ ) → ( ( ℤ≥ ‘ 𝑥 ) ∩ 𝑍 ) ∈ ( ran ℤ≥ ↾t 𝑍 ) )
49 7 8 47 48 mp3an12i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ 𝑍 ) → ( ( ℤ≥ ‘ 𝑥 ) ∩ 𝑍 ) ∈ ( ran ℤ≥ ↾t 𝑍 ) )
50 43 49 eqeltrrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑥 ) ∈ ( ran ℤ≥ ↾t 𝑍 ) )
51 50 ralrimiva ⊢ ( 𝑀 ∈ ℤ → ∀ 𝑥 ∈ 𝑍 ( ℤ≥ ‘ 𝑥 ) ∈ ( ran ℤ≥ ↾t 𝑍 ) )
52 ffun ⊢ ( ℤ≥ : ℤ ⟶ 𝒫 ℤ → Fun ℤ≥ )
53 4 52 ax-mp ⊢ Fun ℤ≥
54 4 fdmi ⊢ dom ℤ≥ = ℤ
55 18 54 sseqtrri ⊢ 𝑍 ⊆ dom ℤ≥
56 funimass4 ⊢ ( ( Fun ℤ≥ ∧ 𝑍 ⊆ dom ℤ≥ ) → ( ( ℤ≥ “ 𝑍 ) ⊆ ( ran ℤ≥ ↾t 𝑍 ) ↔ ∀ 𝑥 ∈ 𝑍 ( ℤ≥ ‘ 𝑥 ) ∈ ( ran ℤ≥ ↾t 𝑍 ) ) )
57 53 55 56 mp2an ⊢ ( ( ℤ≥ “ 𝑍 ) ⊆ ( ran ℤ≥ ↾t 𝑍 ) ↔ ∀ 𝑥 ∈ 𝑍 ( ℤ≥ ‘ 𝑥 ) ∈ ( ran ℤ≥ ↾t 𝑍 ) )
58 51 57 sylibr ⊢ ( 𝑀 ∈ ℤ → ( ℤ≥ “ 𝑍 ) ⊆ ( ran ℤ≥ ↾t 𝑍 ) )
59 37 58 eqssd ⊢ ( 𝑀 ∈ ℤ → ( ran ℤ≥ ↾t 𝑍 ) = ( ℤ≥ “ 𝑍 ) )