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 = ℤ_{\geq M}$
	Assertion	uzrest	$⊢ M \in ℤ \to ran ℤ_{\geq} ↾_{𝑡} Z = ℤ_{\geq} [Z]$

Proof

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

Metamath Proof Explorer

Theorem uzrest

Proof