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

Metamath Proof Explorer

Theorem axpre-lttri

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 . This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttri . (Contributed by NM, 19-May-1996) (Revised by Mario Carneiro, 16-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion axpre-lttri ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 elreal ⊢ ( 𝐴 ∈ ℝ ↔ ∃ 𝑥 ∈ R ⟨ 𝑥 , 0R ⟩ = 𝐴 )
2 elreal ⊢ ( 𝐵 ∈ ℝ ↔ ∃ 𝑦 ∈ R ⟨ 𝑦 , 0R ⟩ = 𝐵 )
3 breq1 ⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ↔ 𝐴 <ℝ ⟨ 𝑦 , 0R ⟩ ) )
4 eqeq1 ⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ⟨ 𝑥 , 0R ⟩ = ⟨ 𝑦 , 0R ⟩ ↔ 𝐴 = ⟨ 𝑦 , 0R ⟩ ) )
5 breq2 ⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑥 , 0R ⟩ ↔ ⟨ 𝑦 , 0R ⟩ <ℝ 𝐴 ) )
6 4 5 orbi12d ⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ( ⟨ 𝑥 , 0R ⟩ = ⟨ 𝑦 , 0R ⟩ ∨ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑥 , 0R ⟩ ) ↔ ( 𝐴 = ⟨ 𝑦 , 0R ⟩ ∨ ⟨ 𝑦 , 0R ⟩ <ℝ 𝐴 ) ) )
7 6 notbid ⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ¬ ( ⟨ 𝑥 , 0R ⟩ = ⟨ 𝑦 , 0R ⟩ ∨ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑥 , 0R ⟩ ) ↔ ¬ ( 𝐴 = ⟨ 𝑦 , 0R ⟩ ∨ ⟨ 𝑦 , 0R ⟩ <ℝ 𝐴 ) ) )
8 3 7 bibi12d ⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ↔ ¬ ( ⟨ 𝑥 , 0R ⟩ = ⟨ 𝑦 , 0R ⟩ ∨ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑥 , 0R ⟩ ) ) ↔ ( 𝐴 <ℝ ⟨ 𝑦 , 0R ⟩ ↔ ¬ ( 𝐴 = ⟨ 𝑦 , 0R ⟩ ∨ ⟨ 𝑦 , 0R ⟩ <ℝ 𝐴 ) ) ) )
9 breq2 ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( 𝐴 <ℝ ⟨ 𝑦 , 0R ⟩ ↔ 𝐴 <ℝ 𝐵 ) )
10 eqeq2 ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( 𝐴 = ⟨ 𝑦 , 0R ⟩ ↔ 𝐴 = 𝐵 ) )
11 breq1 ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( ⟨ 𝑦 , 0R ⟩ <ℝ 𝐴 ↔ 𝐵 <ℝ 𝐴 ) )
12 10 11 orbi12d ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( ( 𝐴 = ⟨ 𝑦 , 0R ⟩ ∨ ⟨ 𝑦 , 0R ⟩ <ℝ 𝐴 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴 ) ) )
13 12 notbid ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( ¬ ( 𝐴 = ⟨ 𝑦 , 0R ⟩ ∨ ⟨ 𝑦 , 0R ⟩ <ℝ 𝐴 ) ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴 ) ) )
14 9 13 bibi12d ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( ( 𝐴 <ℝ ⟨ 𝑦 , 0R ⟩ ↔ ¬ ( 𝐴 = ⟨ 𝑦 , 0R ⟩ ∨ ⟨ 𝑦 , 0R ⟩ <ℝ 𝐴 ) ) ↔ ( 𝐴 <ℝ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴 ) ) ) )
15 ltsosr ⊢ <R Or R
16 sotric ⊢ ( ( <R Or R ∧ ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ) → ( 𝑥 <R 𝑦 ↔ ¬ ( 𝑥 = 𝑦 ∨ 𝑦 <R 𝑥 ) ) )
17 15 16 mpan ⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) → ( 𝑥 <R 𝑦 ↔ ¬ ( 𝑥 = 𝑦 ∨ 𝑦 <R 𝑥 ) ) )
18 ltresr ⊢ ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ↔ 𝑥 <R 𝑦 )
19 vex ⊢ 𝑥 ∈ V
20 19 eqresr ⊢ ( ⟨ 𝑥 , 0R ⟩ = ⟨ 𝑦 , 0R ⟩ ↔ 𝑥 = 𝑦 )
21 ltresr ⊢ ( ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑥 , 0R ⟩ ↔ 𝑦 <R 𝑥 )
22 20 21 orbi12i ⊢ ( ( ⟨ 𝑥 , 0R ⟩ = ⟨ 𝑦 , 0R ⟩ ∨ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑥 , 0R ⟩ ) ↔ ( 𝑥 = 𝑦 ∨ 𝑦 <R 𝑥 ) )
23 22 notbii ⊢ ( ¬ ( ⟨ 𝑥 , 0R ⟩ = ⟨ 𝑦 , 0R ⟩ ∨ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑥 , 0R ⟩ ) ↔ ¬ ( 𝑥 = 𝑦 ∨ 𝑦 <R 𝑥 ) )
24 17 18 23 3bitr4g ⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) → ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ↔ ¬ ( ⟨ 𝑥 , 0R ⟩ = ⟨ 𝑦 , 0R ⟩ ∨ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑥 , 0R ⟩ ) ) )
25 1 2 8 14 24 2gencl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴 ) ) )