Theorem latref 18522

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146   class class class wbr 5114  ‘cfv 6543  Basecbs 17294  lecple 17342  Posetcpo 18388  Latclat 18512

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-xp 5672  df-dm 5676  df-iota 6499  df-fv 6551  df-proset 18375  df-poset 18394  df-lat 18513

This theorem is used by:  latleeqj1  18532  latjidm  18543  latleeqm1  18548  latmidm  18555  olj01  40040  olm01  40051  cmtidN  40072  ps-1  40292  3at  40305  llnneat  40329  2atnelpln  40359  lplnneat  40360  lplnnelln  40361  3atnelvolN  40401  lvolneatN  40403  lvolnelln  40404  lvolnelpln  40405  4at  40428  lplncvrlvol  40431  lncmp  40598  lhpocnle  40831  ltrnel  40954  ltrncnvel  40957  tendoidcl  41584  cdlemk39u  41783  dia1eldmN  41856  dia1N  41868  dihwN  42104  dihglblem5apreN  42106  dihmeetbclemN  42119