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