Theorem zextle

Description: An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005)

	Ref	Expression
Assertion	zextle	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) ) → 𝑀 = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
2	1	leidd	⊢ ( 𝑀 ∈ ℤ → 𝑀 ≤ 𝑀 )
3	2	adantr	⊢ ( ( 𝑀 ∈ ℤ ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) ) → 𝑀 ≤ 𝑀 )
4		breq1	⊢ ( 𝑘 = 𝑀 → ( 𝑘 ≤ 𝑀 ↔ 𝑀 ≤ 𝑀 ) )
5		breq1	⊢ ( 𝑘 = 𝑀 → ( 𝑘 ≤ 𝑁 ↔ 𝑀 ≤ 𝑁 ) )
6	4 5	bibi12d	⊢ ( 𝑘 = 𝑀 → ( ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) ↔ ( 𝑀 ≤ 𝑀 ↔ 𝑀 ≤ 𝑁 ) ) )
7	6	rspcva	⊢ ( ( 𝑀 ∈ ℤ ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) ) → ( 𝑀 ≤ 𝑀 ↔ 𝑀 ≤ 𝑁 ) )
8	3 7	mpbid	⊢ ( ( 𝑀 ∈ ℤ ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) ) → 𝑀 ≤ 𝑁 )
9	8	adantlr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) ) → 𝑀 ≤ 𝑁 )
10		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
11	10	leidd	⊢ ( 𝑁 ∈ ℤ → 𝑁 ≤ 𝑁 )
12	11	adantr	⊢ ( ( 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) ) → 𝑁 ≤ 𝑁 )
13		breq1	⊢ ( 𝑘 = 𝑁 → ( 𝑘 ≤ 𝑀 ↔ 𝑁 ≤ 𝑀 ) )
14		breq1	⊢ ( 𝑘 = 𝑁 → ( 𝑘 ≤ 𝑁 ↔ 𝑁 ≤ 𝑁 ) )
15	13 14	bibi12d	⊢ ( 𝑘 = 𝑁 → ( ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) ↔ ( 𝑁 ≤ 𝑀 ↔ 𝑁 ≤ 𝑁 ) ) )
16	15	rspcva	⊢ ( ( 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) ) → ( 𝑁 ≤ 𝑀 ↔ 𝑁 ≤ 𝑁 ) )
17	12 16	mpbird	⊢ ( ( 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) ) → 𝑁 ≤ 𝑀 )
18	17	adantll	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) ) → 𝑁 ≤ 𝑀 )
19	9 18	jca	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) ) → ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) )
20	19	ex	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) → ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) )
21		letri3	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 = 𝑁 ↔ ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) )
22	1 10 21	syl2an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 = 𝑁 ↔ ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) )
23	20 22	sylibrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) → 𝑀 = 𝑁 ) )
24	23	3impia	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) ) → 𝑀 = 𝑁 )