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 ( ( 𝐴 ∈ ran ℤ≥ ∧ 𝐵 ∈ ran ℤ≥ ) → ( 𝐴 ∩ 𝐵 ) ∈ ran ℤ≥ )

Proof

Step Hyp Ref Expression
1 uzf ⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ
2 ffn ⊢ ( ℤ≥ : ℤ ⟶ 𝒫 ℤ → ℤ≥ Fn ℤ )
3 1 2 ax-mp ⊢ ℤ≥ Fn ℤ
4 fvelrnb ⊢ ( ℤ≥ Fn ℤ → ( 𝐴 ∈ ran ℤ≥ ↔ ∃ 𝑥 ∈ ℤ ( ℤ≥ ‘ 𝑥 ) = 𝐴 ) )
5 3 4 ax-mp ⊢ ( 𝐴 ∈ ran ℤ≥ ↔ ∃ 𝑥 ∈ ℤ ( ℤ≥ ‘ 𝑥 ) = 𝐴 )
6 fvelrnb ⊢ ( ℤ≥ Fn ℤ → ( 𝐵 ∈ ran ℤ≥ ↔ ∃ 𝑦 ∈ ℤ ( ℤ≥ ‘ 𝑦 ) = 𝐵 ) )
7 3 6 ax-mp ⊢ ( 𝐵 ∈ ran ℤ≥ ↔ ∃ 𝑦 ∈ ℤ ( ℤ≥ ‘ 𝑦 ) = 𝐵 )
8 ineq1 ⊢ ( ( ℤ≥ ‘ 𝑥 ) = 𝐴 → ( ( ℤ≥ ‘ 𝑥 ) ∩ ( ℤ≥ ‘ 𝑦 ) ) = ( 𝐴 ∩ ( ℤ≥ ‘ 𝑦 ) ) )
9 8 eleq1d ⊢ ( ( ℤ≥ ‘ 𝑥 ) = 𝐴 → ( ( ( ℤ≥ ‘ 𝑥 ) ∩ ( ℤ≥ ‘ 𝑦 ) ) ∈ ran ℤ≥ ↔ ( 𝐴 ∩ ( ℤ≥ ‘ 𝑦 ) ) ∈ ran ℤ≥ ) )
10 ineq2 ⊢ ( ( ℤ≥ ‘ 𝑦 ) = 𝐵 → ( 𝐴 ∩ ( ℤ≥ ‘ 𝑦 ) ) = ( 𝐴 ∩ 𝐵 ) )
11 10 eleq1d ⊢ ( ( ℤ≥ ‘ 𝑦 ) = 𝐵 → ( ( 𝐴 ∩ ( ℤ≥ ‘ 𝑦 ) ) ∈ ran ℤ≥ ↔ ( 𝐴 ∩ 𝐵 ) ∈ ran ℤ≥ ) )
12 uzin ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ℤ≥ ‘ 𝑥 ) ∩ ( ℤ≥ ‘ 𝑦 ) ) = ( ℤ≥ ‘ if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ) )
13 ifcl ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ∈ ℤ )
14 13 ancoms ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ∈ ℤ )
15 fnfvelrn ⊢ ( ( ℤ≥ Fn ℤ ∧ if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ∈ ℤ ) → ( ℤ≥ ‘ if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ) ∈ ran ℤ≥ )
16 3 14 15 sylancr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ℤ≥ ‘ if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ) ∈ ran ℤ≥ )
17 12 16 eqeltrd ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ℤ≥ ‘ 𝑥 ) ∩ ( ℤ≥ ‘ 𝑦 ) ) ∈ ran ℤ≥ )
18 5 7 9 11 17 2gencl ⊢ ( ( 𝐴 ∈ ran ℤ≥ ∧ 𝐵 ∈ ran ℤ≥ ) → ( 𝐴 ∩ 𝐵 ) ∈ ran ℤ≥ )