Theorem latref 18535

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   class class class wbr 5107  ‘cfv 6537  Basecbs 17307  lecple 17355  Posetcpo 18401  Latclat 18525

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 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-xp 5665  df-dm 5669  df-iota 6493  df-fv 6545  df-proset 18388  df-poset 18407  df-lat 18526

This theorem is used by:  latleeqj1  18545  latjidm  18556  latleeqm1  18561  latmidm  18568  olj01  40106  olm01  40117  cmtidN  40138  ps-1  40358  3at  40371  llnneat  40395  2atnelpln  40425  lplnneat  40426  lplnnelln  40427  3atnelvolN  40467  lvolneatN  40469  lvolnelln  40470  lvolnelpln  40471  4at  40494  lplncvrlvol  40497  lncmp  40664  lhpocnle  40897  ltrnel  41020  ltrncnvel  41023  tendoidcl  41650  cdlemk39u  41849  dia1eldmN  41922  dia1N  41934  dihwN  42170  dihglblem5apreN  42172  dihmeetbclemN  42185