Theorem latref 18344

Description: A lattice ordering is reflexive. (ssid 3969 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 18341	. 2 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
2		latref.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
3		latref.l	. . 3 ⊢ ≤ = (le‘𝐾)
4	2, 3	posref 18221	. 2 ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋)
5	1, 4	sylan 580	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106   class class class wbr 5110  ‘cfv 6501  Basecbs 17094  lecple 17154  Posetcpo 18210  Latclat 18334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-nul 5268

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rab 3406  df-v 3448  df-sbc 3743  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-xp 5644  df-dm 5648  df-iota 6453  df-fv 6509  df-proset 18198  df-poset 18216  df-lat 18335

This theorem is referenced by:  latleeqj1  18354  latjidm  18365  latleeqm1  18370  latmidm  18377  olj01  37760  olm01  37771  cmtidN  37792  ps-1  38013  3at  38026  llnneat  38050  2atnelpln  38080  lplnneat  38081  lplnnelln  38082  3atnelvolN  38122  lvolneatN  38124  lvolnelln  38125  lvolnelpln  38126  4at  38149  lplncvrlvol  38152  lncmp  38319  lhpocnle  38552  ltrnel  38675  ltrncnvel  38678  tendoidcl  39305  cdlemk39u  39504  dia1eldmN  39577  dia1N  39589  dihwN  39825  dihglblem5apreN  39827  dihmeetbclemN  39840