This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem postr

Description: A poset ordering is transitive. (Contributed by NM, 11-Sep-2011)

Ref Expression
Hypotheses posi.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
posi.l ⊢ ≤ = ( le ‘ 𝐾 )
Assertion postr ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) )

Proof

Step Hyp Ref Expression
1 posi.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 posi.l ⊢ ≤ = ( le ‘ 𝐾 )
3 1 2 posi ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) → 𝑋 = 𝑌 ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) )
4 3 simp3d ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) )