Theorem latref 16377

Description: A lattice ordering is reflexive. (ssid 3437 analog.) (Contributed by NM, 8-Oct-2011.)

Hypotheses

Ref	Expression
latref.b	|- B = ( Base ` K )
latref.l	|- .<_ = ( le ` K )

Assertion

Ref	Expression
latref	|- ( ( K e. Lat /\ X e. B ) -> X .<_ X )

Proof of Theorem latref

Step	Hyp	Ref	Expression
1		latpos 16374	. 2 |- ( K e. Lat -> K e. Poset )
2		latref.b	. . 3 |- B = ( Base ` K )
3		latref.l	. . 3 |- .<_ = ( le ` K )
4	2, 3	posref 16274	. 2 |- ( ( K e. Poset /\ X e. B ) -> X .<_ X )
5	1, 4	sylan 479	1 |- ( ( K e. Lat /\ X e. B ) -> X .<_ X )

Syntax hints:   -> wi 4   /\ wa 376   = wceq 1452   e. wcel 1904   class class class wbr 4395   ` cfv 5589   Basecbs 15199   lecple 15275   Posetcpo 16263   Latclat 16369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-nul 4527

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-xp 4845  df-dm 4849  df-iota 5553  df-fv 5597  df-preset 16251  df-poset 16269  df-lat 16370

This theorem is referenced by:  latleeqj1  16387  latjidm  16398  latleeqm1  16403  latmidm  16410  olj01  32862  olm01  32873  cmtidN  32894  ps-1  33113  3at  33126  llnneat  33150  2atnelpln  33180  lplnneat  33181  lplnnelln  33182  3atnelvolN  33222  lvolneatN  33224  lvolnelln  33225  lvolnelpln  33226  4at  33249  lplncvrlvol  33252  lncmp  33419  lhpocnle  33652  ltrnel  33775  ltrncnvel  33778  ltrnmwOLD  33788  tendoidcl  34407  cdlemk39u  34606  dia1eldmN  34680  dia1N  34692  dihwN  34928  dihglblem5apreN  34930  dihmeetbclemN  34943