This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ∀ 𝑘 ∈ ℤ ( 𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁 ) ) → 𝑀 = 𝑁 )