Theorem latref 17655

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1531   ∈ wcel 2108   class class class wbr 5057  ‘cfv 6348  Basecbs 16475  lecple 16564  Posetcpo 17542  Latclat 17647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-nul 5201

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-xp 5554  df-dm 5558  df-iota 6307  df-fv 6356  df-proset 17530  df-poset 17548  df-lat 17648

This theorem is referenced by:  latleeqj1  17665  latjidm  17676  latleeqm1  17681  latmidm  17688  olj01  36353  olm01  36364  cmtidN  36385  ps-1  36605  3at  36618  llnneat  36642  2atnelpln  36672  lplnneat  36673  lplnnelln  36674  3atnelvolN  36714  lvolneatN  36716  lvolnelln  36717  lvolnelpln  36718  4at  36741  lplncvrlvol  36744  lncmp  36911  lhpocnle  37144  ltrnel  37267  ltrncnvel  37270  tendoidcl  37897  cdlemk39u  38096  dia1eldmN  38169  dia1N  38181  dihwN  38417  dihglblem5apreN  38419  dihmeetbclemN  38432