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	$⊢ (A \in ℝ \land B \in ℝ) \to (A <_{ℝ} B \leftrightarrow \neg (A = B \lor B <_{ℝ} A))$

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		breq1	$⊢ ⟨x, 0_{𝑹}⟩ = A \to (⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow A <_{ℝ} ⟨y, 0_{𝑹}⟩)$
4		eqeq1	$⊢ ⟨x, 0_{𝑹}⟩ = A \to (⟨x, 0_{𝑹}⟩ = ⟨y, 0_{𝑹}⟩ \leftrightarrow A = ⟨y, 0_{𝑹}⟩)$
5		breq2	$⊢ ⟨x, 0_{𝑹}⟩ = A \to (⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨x, 0_{𝑹}⟩ \leftrightarrow ⟨y, 0_{𝑹}⟩ <_{ℝ} A)$
6	4 5	orbi12d	$⊢ ⟨x, 0_{𝑹}⟩ = A \to ((⟨x, 0_{𝑹}⟩ = ⟨y, 0_{𝑹}⟩ \lor ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨x, 0_{𝑹}⟩) \leftrightarrow (A = ⟨y, 0_{𝑹}⟩ \lor ⟨y, 0_{𝑹}⟩ <_{ℝ} A))$
7	6	notbid	$⊢ ⟨x, 0_{𝑹}⟩ = A \to (\neg (⟨x, 0_{𝑹}⟩ = ⟨y, 0_{𝑹}⟩ \lor ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨x, 0_{𝑹}⟩) \leftrightarrow \neg (A = ⟨y, 0_{𝑹}⟩ \lor ⟨y, 0_{𝑹}⟩ <_{ℝ} A))$
8	3 7	bibi12d	$⊢ ⟨x, 0_{𝑹}⟩ = A \to ((⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow \neg (⟨x, 0_{𝑹}⟩ = ⟨y, 0_{𝑹}⟩ \lor ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨x, 0_{𝑹}⟩)) \leftrightarrow (A <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow \neg (A = ⟨y, 0_{𝑹}⟩ \lor ⟨y, 0_{𝑹}⟩ <_{ℝ} A)))$
9		breq2	$⊢ ⟨y, 0_{𝑹}⟩ = B \to (A <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow A <_{ℝ} B)$
10		eqeq2	$⊢ ⟨y, 0_{𝑹}⟩ = B \to (A = ⟨y, 0_{𝑹}⟩ \leftrightarrow A = B)$
11		breq1	$⊢ ⟨y, 0_{𝑹}⟩ = B \to (⟨y, 0_{𝑹}⟩ <_{ℝ} A \leftrightarrow B <_{ℝ} A)$
12	10 11	orbi12d	$⊢ ⟨y, 0_{𝑹}⟩ = B \to ((A = ⟨y, 0_{𝑹}⟩ \lor ⟨y, 0_{𝑹}⟩ <_{ℝ} A) \leftrightarrow (A = B \lor B <_{ℝ} A))$
13	12	notbid	$⊢ ⟨y, 0_{𝑹}⟩ = B \to (\neg (A = ⟨y, 0_{𝑹}⟩ \lor ⟨y, 0_{𝑹}⟩ <_{ℝ} A) \leftrightarrow \neg (A = B \lor B <_{ℝ} A))$
14	9 13	bibi12d	$⊢ ⟨y, 0_{𝑹}⟩ = B \to ((A <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow \neg (A = ⟨y, 0_{𝑹}⟩ \lor ⟨y, 0_{𝑹}⟩ <_{ℝ} A)) \leftrightarrow (A <_{ℝ} B \leftrightarrow \neg (A = B \lor B <_{ℝ} A)))$
15		ltsosr	$⊢ <_{𝑹} Or 𝑹$
16		sotric	$⊢ (<_{𝑹} Or 𝑹 \land (x \in 𝑹 \land y \in 𝑹)) \to (x <_{𝑹} y \leftrightarrow \neg (x = y \lor y <_{𝑹} x))$
17	15 16	mpan	$⊢ (x \in 𝑹 \land y \in 𝑹) \to (x <_{𝑹} y \leftrightarrow \neg (x = y \lor y <_{𝑹} x))$
18		ltresr	$⊢ ⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow x <_{𝑹} y$
19		vex	$⊢ x \in V$
20	19	eqresr	$⊢ ⟨x, 0_{𝑹}⟩ = ⟨y, 0_{𝑹}⟩ \leftrightarrow x = y$
21		ltresr	$⊢ ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨x, 0_{𝑹}⟩ \leftrightarrow y <_{𝑹} x$
22	20 21	orbi12i	$⊢ (⟨x, 0_{𝑹}⟩ = ⟨y, 0_{𝑹}⟩ \lor ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨x, 0_{𝑹}⟩) \leftrightarrow (x = y \lor y <_{𝑹} x)$
23	22	notbii	$⊢ \neg (⟨x, 0_{𝑹}⟩ = ⟨y, 0_{𝑹}⟩ \lor ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨x, 0_{𝑹}⟩) \leftrightarrow \neg (x = y \lor y <_{𝑹} x)$
24	17 18 23	3bitr4g	$⊢ (x \in 𝑹 \land y \in 𝑹) \to (⟨x, 0_{𝑹}⟩ <_{ℝ} ⟨y, 0_{𝑹}⟩ \leftrightarrow \neg (⟨x, 0_{𝑹}⟩ = ⟨y, 0_{𝑹}⟩ \lor ⟨y, 0_{𝑹}⟩ <_{ℝ} ⟨x, 0_{𝑹}⟩))$
25	1 2 8 14 24	2gencl	$⊢ (A \in ℝ \land B \in ℝ) \to (A <_{ℝ} B \leftrightarrow \neg (A = B \lor B <_{ℝ} A))$

Metamath Proof Explorer

Theorem axpre-lttri

Proof