Metamath Proof Explorer

Theorem 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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶 ) → 𝐴 <ℝ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 elreal ⊢ ( 𝐴 ∈ ℝ ↔ ∃ 𝑥 ∈ R ⟨ 𝑥 , 0R ⟩ = 𝐴 )
2 elreal ⊢ ( 𝐵 ∈ ℝ ↔ ∃ 𝑦 ∈ R ⟨ 𝑦 , 0R ⟩ = 𝐵 )
3 elreal ⊢ ( 𝐶 ∈ ℝ ↔ ∃ 𝑧 ∈ R ⟨ 𝑧 , 0R ⟩ = 𝐶 )
4 breq1 ⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ↔ 𝐴 <ℝ ⟨ 𝑦 , 0R ⟩ ) )
5 4 anbi1d ⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ∧ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ) ↔ ( 𝐴 <ℝ ⟨ 𝑦 , 0R ⟩ ∧ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ) ) )
6 breq1 ⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ↔ 𝐴 <ℝ ⟨ 𝑧 , 0R ⟩ ) )
7 5 6 imbi12d ⊢ ( ⟨ 𝑥 , 0R ⟩ = 𝐴 → ( ( ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ∧ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ) → ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ) ↔ ( ( 𝐴 <ℝ ⟨ 𝑦 , 0R ⟩ ∧ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ) → 𝐴 <ℝ ⟨ 𝑧 , 0R ⟩ ) ) )
8 breq2 ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( 𝐴 <ℝ ⟨ 𝑦 , 0R ⟩ ↔ 𝐴 <ℝ 𝐵 ) )
9 breq1 ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ↔ 𝐵 <ℝ ⟨ 𝑧 , 0R ⟩ ) )
10 8 9 anbi12d ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( ( 𝐴 <ℝ ⟨ 𝑦 , 0R ⟩ ∧ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ) ↔ ( 𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ ⟨ 𝑧 , 0R ⟩ ) ) )
11 10 imbi1d ⊢ ( ⟨ 𝑦 , 0R ⟩ = 𝐵 → ( ( ( 𝐴 <ℝ ⟨ 𝑦 , 0R ⟩ ∧ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ) → 𝐴 <ℝ ⟨ 𝑧 , 0R ⟩ ) ↔ ( ( 𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ ⟨ 𝑧 , 0R ⟩ ) → 𝐴 <ℝ ⟨ 𝑧 , 0R ⟩ ) ) )
12 breq2 ⊢ ( ⟨ 𝑧 , 0R ⟩ = 𝐶 → ( 𝐵 <ℝ ⟨ 𝑧 , 0R ⟩ ↔ 𝐵 <ℝ 𝐶 ) )
13 12 anbi2d ⊢ ( ⟨ 𝑧 , 0R ⟩ = 𝐶 → ( ( 𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ ⟨ 𝑧 , 0R ⟩ ) ↔ ( 𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶 ) ) )
14 breq2 ⊢ ( ⟨ 𝑧 , 0R ⟩ = 𝐶 → ( 𝐴 <ℝ ⟨ 𝑧 , 0R ⟩ ↔ 𝐴 <ℝ 𝐶 ) )
15 13 14 imbi12d ⊢ ( ⟨ 𝑧 , 0R ⟩ = 𝐶 → ( ( ( 𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ ⟨ 𝑧 , 0R ⟩ ) → 𝐴 <ℝ ⟨ 𝑧 , 0R ⟩ ) ↔ ( ( 𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶 ) → 𝐴 <ℝ 𝐶 ) ) )
16 ltresr ⊢ ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ↔ 𝑥 <R 𝑦 )
17 ltresr ⊢ ( ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ↔ 𝑦 <R 𝑧 )
18 ltsosr ⊢ <R Or R
19 ltrelsr ⊢ <R ⊆ ( R × R )
20 18 19 sotri ⊢ ( ( 𝑥 <R 𝑦 ∧ 𝑦 <R 𝑧 ) → 𝑥 <R 𝑧 )
21 16 17 20 syl2anb ⊢ ( ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ∧ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ) → 𝑥 <R 𝑧 )
22 ltresr ⊢ ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ↔ 𝑥 <R 𝑧 )
23 21 22 sylibr ⊢ ( ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ∧ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ) → ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ )
24 23 a1i ⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ∧ 𝑧 ∈ R ) → ( ( ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑦 , 0R ⟩ ∧ ⟨ 𝑦 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ) → ⟨ 𝑥 , 0R ⟩ <ℝ ⟨ 𝑧 , 0R ⟩ ) )
25 1 2 3 7 11 15 24 3gencl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶 ) → 𝐴 <ℝ 𝐶 ) )