Metamath Proof Explorer

Theorem uzin2

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

		Ref	Expression
	Assertion	uzin2	$⊢ (A \in ran ℤ_{\geq} \land B \in ran ℤ_{\geq}) \to A \cap B \in ran ℤ_{\geq}$

Proof

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