Metamath Proof Explorer

Axiom ax-pre-lttrn

Description: Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, justified by theorem axpre-lttrn . Note: The more general version for extended reals is axlttrn . Normally new proofs would use lttr . (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion ax-pre-lttrn ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < ℝ B ∧ B < ℝ C → A < ℝ C

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cr class ℝ
2 0 1 wcel wff A ∈ ℝ
3 cB class B
4 3 1 wcel wff B ∈ ℝ
5 cC class C
6 5 1 wcel wff C ∈ ℝ
7 2 4 6 w3a wff A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ
8 cltrr class < ℝ
9 0 3 8 wbr wff A < ℝ B
10 3 5 8 wbr wff B < ℝ C
11 9 10 wa wff A < ℝ B ∧ B < ℝ C
12 0 5 8 wbr wff A < ℝ C
13 11 12 wi wff A < ℝ B ∧ B < ℝ C → A < ℝ C
14 7 13 wi wff A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < ℝ B ∧ B < ℝ C → A < ℝ C