# 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 ∈ ran ⁡ ℤ ≥ ∧ B ∈ ran ⁡ ℤ ≥ → A ∩ B ∈ ran ⁡ ℤ ≥$

### Proof

Step Hyp Ref Expression
1 uzf $⊢ ℤ ≥ : ℤ ⟶ 𝒫 ℤ$
2 ffn $⊢ ℤ ≥ : ℤ ⟶ 𝒫 ℤ → ℤ ≥ Fn ℤ$
3 1 2 ax-mp $⊢ ℤ ≥ Fn ℤ$
4 fvelrnb $⊢ ℤ ≥ Fn ℤ → A ∈ ran ⁡ ℤ ≥ ↔ ∃ x ∈ ℤ ℤ ≥ x = A$
5 3 4 ax-mp $⊢ A ∈ ran ⁡ ℤ ≥ ↔ ∃ x ∈ ℤ ℤ ≥ x = A$
6 fvelrnb $⊢ ℤ ≥ Fn ℤ → B ∈ ran ⁡ ℤ ≥ ↔ ∃ y ∈ ℤ ℤ ≥ y = B$
7 3 6 ax-mp $⊢ B ∈ ran ⁡ ℤ ≥ ↔ ∃ y ∈ ℤ ℤ ≥ y = B$
8 ineq1 $⊢ ℤ ≥ x = A → ℤ ≥ x ∩ ℤ ≥ y = A ∩ ℤ ≥ y$
9 8 eleq1d $⊢ ℤ ≥ x = A → ℤ ≥ x ∩ ℤ ≥ y ∈ ran ⁡ ℤ ≥ ↔ A ∩ ℤ ≥ y ∈ ran ⁡ ℤ ≥$
10 ineq2 $⊢ ℤ ≥ y = B → A ∩ ℤ ≥ y = A ∩ B$
11 10 eleq1d $⊢ ℤ ≥ y = B → A ∩ ℤ ≥ y ∈ ran ⁡ ℤ ≥ ↔ A ∩ B ∈ ran ⁡ ℤ ≥$
12 uzin $⊢ x ∈ ℤ ∧ y ∈ ℤ → ℤ ≥ x ∩ ℤ ≥ y = ℤ ≥ if x ≤ y y x$
13 ifcl $⊢ y ∈ ℤ ∧ x ∈ ℤ → if x ≤ y y x ∈ ℤ$
14 13 ancoms $⊢ x ∈ ℤ ∧ y ∈ ℤ → if x ≤ y y x ∈ ℤ$
15 fnfvelrn $⊢ ℤ ≥ Fn ℤ ∧ if x ≤ y y x ∈ ℤ → ℤ ≥ if x ≤ y y x ∈ ran ⁡ ℤ ≥$
16 3 14 15 sylancr $⊢ x ∈ ℤ ∧ y ∈ ℤ → ℤ ≥ if x ≤ y y x ∈ ran ⁡ ℤ ≥$
17 12 16 eqeltrd $⊢ x ∈ ℤ ∧ y ∈ ℤ → ℤ ≥ x ∩ ℤ ≥ y ∈ ran ⁡ ℤ ≥$
18 5 7 9 11 17 2gencl $⊢ A ∈ ran ⁡ ℤ ≥ ∧ B ∈ ran ⁡ ℤ ≥ → A ∩ B ∈ ran ⁡ ℤ ≥$