This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⁡ ℤ ≥