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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴 ) ) )