Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axpre-lttri Structured version   Visualization version   GIF version

Theorem axpre-lttri 9930
 Description: Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axlttri 10053. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttri 9954. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
Assertion
Ref Expression
axpre-lttri ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵𝐵 < 𝐴)))

Proof of Theorem axpre-lttri
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elreal 9896 . 2 (𝐴 ∈ ℝ ↔ ∃𝑥R𝑥, 0R⟩ = 𝐴)
2 elreal 9896 . 2 (𝐵 ∈ ℝ ↔ ∃𝑦R𝑦, 0R⟩ = 𝐵)
3 breq1 4616 . . 3 (⟨𝑥, 0R⟩ = 𝐴 → (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ 𝐴 <𝑦, 0R⟩))
4 eqeq1 2625 . . . . 5 (⟨𝑥, 0R⟩ = 𝐴 → (⟨𝑥, 0R⟩ = ⟨𝑦, 0R⟩ ↔ 𝐴 = ⟨𝑦, 0R⟩))
5 breq2 4617 . . . . 5 (⟨𝑥, 0R⟩ = 𝐴 → (⟨𝑦, 0R⟩ <𝑥, 0R⟩ ↔ ⟨𝑦, 0R⟩ < 𝐴))
64, 5orbi12d 745 . . . 4 (⟨𝑥, 0R⟩ = 𝐴 → ((⟨𝑥, 0R⟩ = ⟨𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ <𝑥, 0R⟩) ↔ (𝐴 = ⟨𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ < 𝐴)))
76notbid 308 . . 3 (⟨𝑥, 0R⟩ = 𝐴 → (¬ (⟨𝑥, 0R⟩ = ⟨𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ <𝑥, 0R⟩) ↔ ¬ (𝐴 = ⟨𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ < 𝐴)))
83, 7bibi12d 335 . 2 (⟨𝑥, 0R⟩ = 𝐴 → ((⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ ¬ (⟨𝑥, 0R⟩ = ⟨𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ <𝑥, 0R⟩)) ↔ (𝐴 <𝑦, 0R⟩ ↔ ¬ (𝐴 = ⟨𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ < 𝐴))))
9 breq2 4617 . . 3 (⟨𝑦, 0R⟩ = 𝐵 → (𝐴 <𝑦, 0R⟩ ↔ 𝐴 < 𝐵))
10 eqeq2 2632 . . . . 5 (⟨𝑦, 0R⟩ = 𝐵 → (𝐴 = ⟨𝑦, 0R⟩ ↔ 𝐴 = 𝐵))
11 breq1 4616 . . . . 5 (⟨𝑦, 0R⟩ = 𝐵 → (⟨𝑦, 0R⟩ < 𝐴𝐵 < 𝐴))
1210, 11orbi12d 745 . . . 4 (⟨𝑦, 0R⟩ = 𝐵 → ((𝐴 = ⟨𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ < 𝐴) ↔ (𝐴 = 𝐵𝐵 < 𝐴)))
1312notbid 308 . . 3 (⟨𝑦, 0R⟩ = 𝐵 → (¬ (𝐴 = ⟨𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ < 𝐴) ↔ ¬ (𝐴 = 𝐵𝐵 < 𝐴)))
149, 13bibi12d 335 . 2 (⟨𝑦, 0R⟩ = 𝐵 → ((𝐴 <𝑦, 0R⟩ ↔ ¬ (𝐴 = ⟨𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ < 𝐴)) ↔ (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵𝐵 < 𝐴))))
15 ltsosr 9859 . . . 4 <R Or R
16 sotric 5021 . . . 4 (( <R Or R ∧ (𝑥R𝑦R)) → (𝑥 <R 𝑦 ↔ ¬ (𝑥 = 𝑦𝑦 <R 𝑥)))
1715, 16mpan 705 . . 3 ((𝑥R𝑦R) → (𝑥 <R 𝑦 ↔ ¬ (𝑥 = 𝑦𝑦 <R 𝑥)))
18 ltresr 9905 . . 3 (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ 𝑥 <R 𝑦)
19 vex 3189 . . . . . 6 𝑥 ∈ V
2019eqresr 9902 . . . . 5 (⟨𝑥, 0R⟩ = ⟨𝑦, 0R⟩ ↔ 𝑥 = 𝑦)
21 ltresr 9905 . . . . 5 (⟨𝑦, 0R⟩ <𝑥, 0R⟩ ↔ 𝑦 <R 𝑥)
2220, 21orbi12i 543 . . . 4 ((⟨𝑥, 0R⟩ = ⟨𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ <𝑥, 0R⟩) ↔ (𝑥 = 𝑦𝑦 <R 𝑥))
2322notbii 310 . . 3 (¬ (⟨𝑥, 0R⟩ = ⟨𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ <𝑥, 0R⟩) ↔ ¬ (𝑥 = 𝑦𝑦 <R 𝑥))
2417, 18, 233bitr4g 303 . 2 ((𝑥R𝑦R) → (⟨𝑥, 0R⟩ <𝑦, 0R⟩ ↔ ¬ (⟨𝑥, 0R⟩ = ⟨𝑦, 0R⟩ ∨ ⟨𝑦, 0R⟩ <𝑥, 0R⟩)))
251, 2, 8, 14, 242gencl 3222 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵𝐵 < 𝐴)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ⟨cop 4154   class class class wbr 4613   Or wor 4994  Rcnr 9631  0Rc0r 9632
 Copyright terms: Public domain W3C validator