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

Metamath Proof Explorer

Theorem latref

Description: A lattice ordering is reflexive. ( ssid analog.) (Contributed by NM, 8-Oct-2011)

Ref Expression
Hypotheses latref.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
latref.l ⊢ ≤ = ( le ‘ 𝐾 )
Assertion latref ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )

Proof

Step Hyp Ref Expression
1 latref.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 latref.l ⊢ ≤ = ( le ‘ 𝐾 )
3 latpos ⊢ ( 𝐾 ∈ Lat → 𝐾 ∈ Poset )
4 1 2 posref ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )
5 3 4 sylan ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )