Theorem uz11

Description: The upper integers function is one-to-one. (Contributed by NM, 12-Dec-2005)

	Ref	Expression
Assertion	uz11	⊢ ( 𝑀 ∈ ℤ → ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) ↔ 𝑀 = 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		uzid	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		eleq2	⊢ ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) → ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
3		eluzel2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ∈ ℤ )
4	2 3	biimtrdi	⊢ ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) → ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ ) )
5	1 4	mpan9	⊢ ( ( 𝑀 ∈ ℤ ∧ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℤ )
6		uzid	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
7		eleq2	⊢ ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
8	6 7	imbitrrid	⊢ ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) → ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
9		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑁 )
10	8 9	syl6	⊢ ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) → ( 𝑁 ∈ ℤ → 𝑀 ≤ 𝑁 ) )
11	1 2	imbitrid	⊢ ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) → ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
12		eluzle	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝑀 )
13	11 12	syl6	⊢ ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) → ( 𝑀 ∈ ℤ → 𝑁 ≤ 𝑀 ) )
14	10 13	anim12d	⊢ ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) → ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) )
15	14	impl	⊢ ( ( ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) )
16	15	ancoms	⊢ ( ( 𝑀 ∈ ℤ ∧ ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) )
17	16	anassrs	⊢ ( ( ( 𝑀 ∈ ℤ ∧ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) )
18		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
19		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
20		letri3	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 = 𝑁 ↔ ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) )
21	18 19 20	syl2an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 = 𝑁 ↔ ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) )
22	21	adantlr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 = 𝑁 ↔ ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) )
23	17 22	mpbird	⊢ ( ( ( 𝑀 ∈ ℤ ∧ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑁 ∈ ℤ ) → 𝑀 = 𝑁 )
24	5 23	mpdan	⊢ ( ( 𝑀 ∈ ℤ ∧ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 = 𝑁 )
25	24	ex	⊢ ( 𝑀 ∈ ℤ → ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) → 𝑀 = 𝑁 ) )
26		fveq2	⊢ ( 𝑀 = 𝑁 → ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) )
27	25 26	impbid1	⊢ ( 𝑀 ∈ ℤ → ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑁 ) ↔ 𝑀 = 𝑁 ) )