Theorem latref 18398

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   class class class wbr 5086  ‘cfv 6492  Basecbs 17170  lecple 17218  Posetcpo 18264  Latclat 18388

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5630  df-dm 5634  df-iota 6448  df-fv 6500  df-proset 18251  df-poset 18270  df-lat 18389

This theorem is referenced by:  latleeqj1  18408  latjidm  18419  latleeqm1  18424  latmidm  18431  olj01  39685  olm01  39696  cmtidN  39717  ps-1  39937  3at  39950  llnneat  39974  2atnelpln  40004  lplnneat  40005  lplnnelln  40006  3atnelvolN  40046  lvolneatN  40048  lvolnelln  40049  lvolnelpln  40050  4at  40073  lplncvrlvol  40076  lncmp  40243  lhpocnle  40476  ltrnel  40599  ltrncnvel  40602  tendoidcl  41229  cdlemk39u  41428  dia1eldmN  41501  dia1N  41513  dihwN  41749  dihglblem5apreN  41751  dihmeetbclemN  41764