Theorem latref 18511

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

Hypotheses

Ref	Expression
latref.b	⊢ 𝐵 = (Base‘𝐾)
latref.l	⊢ ≤ = (le‘𝐾)

Assertion

Ref	Expression
latref	⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋)

Proof of Theorem latref

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108   class class class wbr 5166  ‘cfv 6573  Basecbs 17258  lecple 17318  Posetcpo 18377  Latclat 18501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-dm 5710  df-iota 6525  df-fv 6581  df-proset 18365  df-poset 18383  df-lat 18502

This theorem is referenced by:  latleeqj1  18521  latjidm  18532  latleeqm1  18537  latmidm  18544  olj01  39181  olm01  39192  cmtidN  39213  ps-1  39434  3at  39447  llnneat  39471  2atnelpln  39501  lplnneat  39502  lplnnelln  39503  3atnelvolN  39543  lvolneatN  39545  lvolnelln  39546  lvolnelpln  39547  4at  39570  lplncvrlvol  39573  lncmp  39740  lhpocnle  39973  ltrnel  40096  ltrncnvel  40099  tendoidcl  40726  cdlemk39u  40925  dia1eldmN  40998  dia1N  41010  dihwN  41246  dihglblem5apreN  41248  dihmeetbclemN  41261