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