Theorem latref 18322

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106   class class class wbr 5103  ‘cfv 6493  Basecbs 17075  lecple 17132  Posetcpo 18188  Latclat 18312

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 2707  ax-nul 5261

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 2714  df-cleq 2728  df-clel 2814  df-ne 2942  df-ral 3063  df-rab 3406  df-v 3445  df-sbc 3738  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-xp 5637  df-dm 5641  df-iota 6445  df-fv 6501  df-proset 18176  df-poset 18194  df-lat 18313

This theorem is referenced by:  latleeqj1  18332  latjidm  18343  latleeqm1  18348  latmidm  18355  olj01  37654  olm01  37665  cmtidN  37686  ps-1  37907  3at  37920  llnneat  37944  2atnelpln  37974  lplnneat  37975  lplnnelln  37976  3atnelvolN  38016  lvolneatN  38018  lvolnelln  38019  lvolnelpln  38020  4at  38043  lplncvrlvol  38046  lncmp  38213  lhpocnle  38446  ltrnel  38569  ltrncnvel  38572  tendoidcl  39199  cdlemk39u  39398  dia1eldmN  39471  dia1N  39483  dihwN  39719  dihglblem5apreN  39721  dihmeetbclemN  39734