Theorem latref 15533

Description: A lattice ordering is reflexive. (ssid 3523 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 15530	. 2 |- ( K e. Lat -> K e. Poset )
2		latref.b	. . 3 |- B = ( Base ` K )
3		latref.l	. . 3 |- .<_ = ( le ` K )
4	2, 3	posref 15431	. 2 |- ( ( K e. Poset /\ X e. B ) -> X .<_ X )
5	1, 4	sylan 471	1 |- ( ( K e. Lat /\ X e. B ) -> X .<_ X )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   e. wcel 1767   class class class wbr 4447   ` cfv 5586   Basecbs 14483   lecple 14555   Posetcpo 15420   Latclat 15525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4576

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-xp 5005  df-dm 5009  df-iota 5549  df-fv 5594  df-poset 15426  df-lat 15526

This theorem is referenced by:  latleeqj1  15543  latjidm  15554  latleeqm1  15559  latmidm  15566  olj01  34022  olm01  34033  cmtidN  34054  ps-1  34273  3at  34286  llnneat  34310  2atnelpln  34340  lplnneat  34341  lplnnelln  34342  3atnelvolN  34382  lvolneatN  34384  lvolnelln  34385  lvolnelpln  34386  4at  34409  lplncvrlvol  34412  lncmp  34579  lhpocnle  34812  ltrnel  34935  ltrncnvel  34938  ltrnmw  34947  tendoidcl  35565  cdlemk39u  35764  dia1eldmN  35838  dia1N  35850  dihwN  36086  dihglblem5apreN  36088  dihmeetbclemN  36101