uz11

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

		Ref	Expression
	Assertion	uz11	$⊢ M \in ℤ \to (ℤ_{\geq M} = ℤ_{\geq N} \leftrightarrow M = N)$

Proof

Step	Hyp	Ref	Expression
1		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
2		eleq2	$⊢ ℤ_{\geq M} = ℤ_{\geq N} \to (M \in ℤ_{\geq M} \leftrightarrow M \in ℤ_{\geq N})$
3		eluzel2	$⊢ M \in ℤ_{\geq N} \to N \in ℤ$
4	2 3	biimtrdi	$⊢ ℤ_{\geq M} = ℤ_{\geq N} \to (M \in ℤ_{\geq M} \to N \in ℤ)$
5	1 4	mpan9	$⊢ (M \in ℤ \land ℤ_{\geq M} = ℤ_{\geq N}) \to N \in ℤ$
6		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
7		eleq2	$⊢ ℤ_{\geq M} = ℤ_{\geq N} \to (N \in ℤ_{\geq M} \leftrightarrow N \in ℤ_{\geq N})$
8	6 7	imbitrrid	$⊢ ℤ_{\geq M} = ℤ_{\geq N} \to (N \in ℤ \to N \in ℤ_{\geq M})$
9		eluzle	$⊢ N \in ℤ_{\geq M} \to M \leq N$
10	8 9	syl6	$⊢ ℤ_{\geq M} = ℤ_{\geq N} \to (N \in ℤ \to M \leq N)$
11	1 2	imbitrid	$⊢ ℤ_{\geq M} = ℤ_{\geq N} \to (M \in ℤ \to M \in ℤ_{\geq N})$
12		eluzle	$⊢ M \in ℤ_{\geq N} \to N \leq M$
13	11 12	syl6	$⊢ ℤ_{\geq M} = ℤ_{\geq N} \to (M \in ℤ \to N \leq M)$
14	10 13	anim12d	$⊢ ℤ_{\geq M} = ℤ_{\geq N} \to ((N \in ℤ \land M \in ℤ) \to (M \leq N \land N \leq M))$
15	14	impl	$⊢ ((ℤ_{\geq M} = ℤ_{\geq N} \land N \in ℤ) \land M \in ℤ) \to (M \leq N \land N \leq M)$
16	15	ancoms	$⊢ (M \in ℤ \land (ℤ_{\geq M} = ℤ_{\geq N} \land N \in ℤ)) \to (M \leq N \land N \leq M)$
17	16	anassrs	$⊢ ((M \in ℤ \land ℤ_{\geq M} = ℤ_{\geq N}) \land N \in ℤ) \to (M \leq N \land N \leq M)$
18		zre	$⊢ M \in ℤ \to M \in ℝ$
19		zre	$⊢ N \in ℤ \to N \in ℝ$
20		letri3	$⊢ (M \in ℝ \land N \in ℝ) \to (M = N \leftrightarrow (M \leq N \land N \leq M))$
21	18 19 20	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to (M = N \leftrightarrow (M \leq N \land N \leq M))$
22	21	adantlr	$⊢ ((M \in ℤ \land ℤ_{\geq M} = ℤ_{\geq N}) \land N \in ℤ) \to (M = N \leftrightarrow (M \leq N \land N \leq M))$
23	17 22	mpbird	$⊢ ((M \in ℤ \land ℤ_{\geq M} = ℤ_{\geq N}) \land N \in ℤ) \to M = N$
24	5 23	mpdan	$⊢ (M \in ℤ \land ℤ_{\geq M} = ℤ_{\geq N}) \to M = N$
25	24	ex	$⊢ M \in ℤ \to (ℤ_{\geq M} = ℤ_{\geq N} \to M = N)$
26		fveq2	$⊢ M = N \to ℤ_{\geq M} = ℤ_{\geq N}$
27	25 26	impbid1	$⊢ M \in ℤ \to (ℤ_{\geq M} = ℤ_{\geq N} \leftrightarrow M = N)$

Metamath Proof Explorer

Theorem uz11

Proof