axpre-lttrn

Description: Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axlttrn . This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttrn . (Contributed by NM, 19-May-1996) (Revised by Mario Carneiro, 16-Jun-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	axpre-lttrn	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A <_{ℝ} B \land B <_{ℝ} C) \to A <_{ℝ} C)$

Proof

Step	Hyp	Ref	Expression
1		elreal	$⊢ A \in ℝ \leftrightarrow \exists x \in 𝑹 ⟨x, 0_{𝑹}⟩ = A$
2		elreal	$⊢ B \in ℝ \leftrightarrow \exists y \in 𝑹 ⟨y, 0_{𝑹}⟩ = B$
3		elreal	$⊢ C \in ℝ \leftrightarrow \exists z \in 𝑹 ⟨z, 0_{𝑹}⟩ = C$
4		breq1	$⊢ ⟨x, 0_{𝑹}⟩ = A \to (⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow A <_{ℝ} ⟨y, 0_{𝑹}⟩)$
5	4	anbi1d	$⊢ ⟨x, 0_{𝑹}⟩ = A \to ((⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \land ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩) \leftrightarrow (A <_{ℝ} ⟨y, 0_{𝑹}⟩ \land ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩))$
6		breq1	$⊢ ⟨x, 0_{𝑹}⟩ = A \to (⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩ \leftrightarrow A <_{ℝ} ⟨z, 0_{𝑹}⟩)$
7	5 6	imbi12d	$⊢ ⟨x, 0_{𝑹}⟩ = A \to (((⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \land ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩) \to ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩) \leftrightarrow ((A <_{ℝ} ⟨y, 0_{𝑹}⟩ \land ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩) \to A <_{ℝ} ⟨z, 0_{𝑹}⟩))$
8		breq2	$⊢ ⟨y, 0_{𝑹}⟩ = B \to (A <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow A <_{ℝ} B)$
9		breq1	$⊢ ⟨y, 0_{𝑹}⟩ = B \to (⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩ \leftrightarrow B <_{ℝ} ⟨z, 0_{𝑹}⟩)$
10	8 9	anbi12d	$⊢ ⟨y, 0_{𝑹}⟩ = B \to ((A <_{ℝ} ⟨y, 0_{𝑹}⟩ \land ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩) \leftrightarrow (A <_{ℝ} B \land B <_{ℝ} ⟨z, 0_{𝑹}⟩))$
11	10	imbi1d	$⊢ ⟨y, 0_{𝑹}⟩ = B \to (((A <_{ℝ} ⟨y, 0_{𝑹}⟩ \land ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩) \to A <_{ℝ} ⟨z, 0_{𝑹}⟩) \leftrightarrow ((A <_{ℝ} B \land B <_{ℝ} ⟨z, 0_{𝑹}⟩) \to A <_{ℝ} ⟨z, 0_{𝑹}⟩))$
12		breq2	$⊢ ⟨z, 0_{𝑹}⟩ = C \to (B <_{ℝ} ⟨z, 0_{𝑹}⟩ \leftrightarrow B <_{ℝ} C)$
13	12	anbi2d	$⊢ ⟨z, 0_{𝑹}⟩ = C \to ((A <_{ℝ} B \land B <_{ℝ} ⟨z, 0_{𝑹}⟩) \leftrightarrow (A <_{ℝ} B \land B <_{ℝ} C))$
14		breq2	$⊢ ⟨z, 0_{𝑹}⟩ = C \to (A <_{ℝ} ⟨z, 0_{𝑹}⟩ \leftrightarrow A <_{ℝ} C)$
15	13 14	imbi12d	$⊢ ⟨z, 0_{𝑹}⟩ = C \to (((A <_{ℝ} B \land B <_{ℝ} ⟨z, 0_{𝑹}⟩) \to A <_{ℝ} ⟨z, 0_{𝑹}⟩) \leftrightarrow ((A <_{ℝ} B \land B <_{ℝ} C) \to A <_{ℝ} C))$
16		ltresr	$⊢ ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow x <_{𝑹} y$
17		ltresr	$⊢ ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩ \leftrightarrow y <_{𝑹} z$
18		ltsosr	$⊢ <_{𝑹} Or 𝑹$
19		ltrelsr	$⊢ <_{𝑹} \subseteq 𝑹 \times 𝑹$
20	18 19	sotri	$⊢ (x <_{𝑹} y \land y <_{𝑹} z) \to x <_{𝑹} z$
21	16 17 20	syl2anb	$⊢ (⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \land ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩) \to x <_{𝑹} z$
22		ltresr	$⊢ ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩ \leftrightarrow x <_{𝑹} z$
23	21 22	sylibr	$⊢ (⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \land ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩) \to ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩$
24	23	a1i	$⊢ (x \in 𝑹 \land y \in 𝑹 \land z \in 𝑹) \to ((⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \land ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩) \to ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨z, 0_{𝑹}⟩)$
25	1 2 3 7 11 15 24	3gencl	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A <_{ℝ} B \land B <_{ℝ} C) \to A <_{ℝ} C)$

Metamath Proof Explorer

Theorem axpre-lttrn

Proof