Theorem uzin2

Description: The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013)

	Ref	Expression
Assertion	uzin2	$$⊢\left(A\in \mathrm{ran}{\mathbb{Z}}_{\ge }\wedge B\in \mathrm{ran}{\mathbb{Z}}_{\ge }\right)\to A\cap B\in \mathrm{ran}{\mathbb{Z}}_{\ge }$$

Proof

Step	Hyp	Ref	Expression
1		uzf	$$⊢{\mathbb{Z}}_{\ge }:\mathbb{Z}⟶𝒫\mathbb{Z}$$
2		ffn	$$⊢{\mathbb{Z}}_{\ge }:\mathbb{Z}⟶𝒫\mathbb{Z}\to {\mathbb{Z}}_{\ge }Fn\mathbb{Z}$$
3	1 2	ax-mp	$$⊢{\mathbb{Z}}_{\ge }Fn\mathbb{Z}$$
4		fvelrnb	$$⊢{\mathbb{Z}}_{\ge }Fn\mathbb{Z}\to \left(A\in \mathrm{ran}{\mathbb{Z}}_{\ge }\leftrightarrow \exists x\in \mathbb{Z}{\mathbb{Z}}_{\ge x}=A\right)$$
5	3 4	ax-mp	$$⊢A\in \mathrm{ran}{\mathbb{Z}}_{\ge }\leftrightarrow \exists x\in \mathbb{Z}{\mathbb{Z}}_{\ge x}=A$$
6		fvelrnb	$$⊢{\mathbb{Z}}_{\ge }Fn\mathbb{Z}\to \left(B\in \mathrm{ran}{\mathbb{Z}}_{\ge }\leftrightarrow \exists y\in \mathbb{Z}{\mathbb{Z}}_{\ge y}=B\right)$$
7	3 6	ax-mp	$$⊢B\in \mathrm{ran}{\mathbb{Z}}_{\ge }\leftrightarrow \exists y\in \mathbb{Z}{\mathbb{Z}}_{\ge y}=B$$
8		ineq1	$$⊢{\mathbb{Z}}_{\ge x}=A\to {\mathbb{Z}}_{\ge x}\cap {\mathbb{Z}}_{\ge y}=A\cap {\mathbb{Z}}_{\ge y}$$
9	8	eleq1d	$$⊢{\mathbb{Z}}_{\ge x}=A\to \left({\mathbb{Z}}_{\ge x}\cap {\mathbb{Z}}_{\ge y}\in \mathrm{ran}{\mathbb{Z}}_{\ge }\leftrightarrow A\cap {\mathbb{Z}}_{\ge y}\in \mathrm{ran}{\mathbb{Z}}_{\ge }\right)$$
10		ineq2	$$⊢{\mathbb{Z}}_{\ge y}=B\to A\cap {\mathbb{Z}}_{\ge y}=A\cap B$$
11	10	eleq1d	$$⊢{\mathbb{Z}}_{\ge y}=B\to \left(A\cap {\mathbb{Z}}_{\ge y}\in \mathrm{ran}{\mathbb{Z}}_{\ge }\leftrightarrow A\cap B\in \mathrm{ran}{\mathbb{Z}}_{\ge }\right)$$
12		uzin	$$⊢\left(x\in \mathbb{Z}\wedge y\in \mathbb{Z}\right)\to {\mathbb{Z}}_{\ge x}\cap {\mathbb{Z}}_{\ge y}={\mathbb{Z}}_{\ge if\left(x\le y,y,x\right)}$$
13		ifcl	$$⊢\left(y\in \mathbb{Z}\wedge x\in \mathbb{Z}\right)\to if\left(x\le y,y,x\right)\in \mathbb{Z}$$
14	13	ancoms	$$⊢\left(x\in \mathbb{Z}\wedge y\in \mathbb{Z}\right)\to if\left(x\le y,y,x\right)\in \mathbb{Z}$$
15		fnfvelrn	$$⊢\left({\mathbb{Z}}_{\ge }Fn\mathbb{Z}\wedge if\left(x\le y,y,x\right)\in \mathbb{Z}\right)\to {\mathbb{Z}}_{\ge if\left(x\le y,y,x\right)}\in \mathrm{ran}{\mathbb{Z}}_{\ge }$$
16	3 14 15	sylancr	$$⊢\left(x\in \mathbb{Z}\wedge y\in \mathbb{Z}\right)\to {\mathbb{Z}}_{\ge if\left(x\le y,y,x\right)}\in \mathrm{ran}{\mathbb{Z}}_{\ge }$$
17	12 16	eqeltrd	$$⊢\left(x\in \mathbb{Z}\wedge y\in \mathbb{Z}\right)\to {\mathbb{Z}}_{\ge x}\cap {\mathbb{Z}}_{\ge y}\in \mathrm{ran}{\mathbb{Z}}_{\ge }$$
18	5 7 9 11 17	2gencl	$$⊢\left(A\in \mathrm{ran}{\mathbb{Z}}_{\ge }\wedge B\in \mathrm{ran}{\mathbb{Z}}_{\ge }\right)\to A\cap B\in \mathrm{ran}{\mathbb{Z}}_{\ge }$$