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	syl5eq	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ℤ≥ ‘ 𝑦 ) ∩ 𝑍 ) = ( ℤ≥ ‘ 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		df-ss	⊢ ( ( ℤ≥ ‘ 𝑥 ) ⊆ 𝑍 ↔ ( ( ℤ≥ ‘ 𝑥 ) ∩ 𝑍 ) = ( ℤ≥ ‘ 𝑥 ) )
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 𝑍 ) = ( ℤ≥ “ 𝑍 ) )