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 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) )