Theorem lhpbase 35284

Description: A co-atom is a member of the lattice base set (i.e. a lattice element). (Contributed by NM, 18-May-2012.)

Hypotheses

Ref	Expression
lhpbase.b	|- B = ( Base ` K )
lhpbase.h	|- H = ( LHyp ` K )

Assertion

Ref	Expression
lhpbase	|- ( W e. H -> W e. B )

Proof of Theorem lhpbase

Step	Hyp	Ref	Expression
1		n0i 3920	. . . 4 |- ( W e. H -> -. H = (/) )
2		lhpbase.h	. . . . 5 |- H = ( LHyp ` K )
3	2	eqeq1i 2627	. . . 4 |- ( H = (/) <-> ( LHyp ` K ) = (/) )
4	1, 3	sylnib 318	. . 3 |- ( W e. H -> -. ( LHyp ` K ) = (/) )
5		fvprc 6185	. . 3 |- ( -. K e. _V -> ( LHyp ` K ) = (/) )
6	4, 5	nsyl2 142	. 2 |- ( W e. H -> K e. _V )
7		lhpbase.b	. . . 4 |- B = ( Base ` K )
8		eqid 2622	. . . 4 |- ( 1. ` K ) = ( 1. ` K )
9		eqid 2622	. . . 4 |- ( <o ` K ) = ( <o ` K )
10	7, 8, 9, 2	islhp 35282	. . 3 |- ( K e. _V -> ( W e. H <-> ( W e. B /\ W ( <o ` K ) ( 1. ` K ) ) ) )
11	10	simprbda 653	. 2 |- ( ( K e. _V /\ W e. H ) -> W e. B )
12	6, 11	mpancom 703	1 |- ( W e. H -> W e. B )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   _Vcvv 3200   (/)c0 3915   class class class wbr 4653   ` cfv 5888   Basecbs 15857   1.cp1 17038   <o ccvr 34549   LHypclh 35270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-lhyp 35274

This theorem is referenced by:  lhplt  35286  lhp2lt  35287  lhpexlt  35288  lhp0lt  35289  lhpexle  35291  lhpexnle  35292  lhpexle1  35294  lhpexle2lem  35295  lhpexle3lem  35297  lhpocnle  35302  lhpocat  35303  lhpjat1  35306  lhpjat2  35307  lhpj1  35308  lhpmcvr  35309  lhpmcvr2  35310  lhpmcvr3  35311  lhpmcvr4N  35312  lhpmcvr5N  35313  lhpmcvr6N  35314  lhpm0atN  35315  lhpmat  35316  lhpmatb  35317  lhp2at0  35318  lhpelim  35323  lhpmod2i2  35324  lhpmod6i1  35325  cdlemb2  35327  lhpat  35329  lhpat3  35332  4atexlemwb  35345  ltrnatb  35423  ltrnel  35425  ltrncnvel  35428  ltrnmwOLD  35438  trlval2  35450  trlcl  35451  trljat1  35453  trljat2  35454  trlle  35471  trlval3  35474  cdlemc1  35478  cdlemc2  35479  cdlemc4  35481  cdlemc5  35482  cdlemc6  35483  cdlemd2  35486  cdleme0aa  35497  cdleme0b  35499  cdleme0c  35500  cdleme0cp  35501  cdleme0cq  35502  cdleme0e  35504  cdleme0fN  35505  cdlemeulpq  35507  cdleme01N  35508  cdleme0ex1N  35510  cdleme1b  35513  cdleme1  35514  cdleme2  35515  cdleme3b  35516  cdleme3c  35517  cdleme3g  35521  cdleme3h  35522  cdleme3  35524  cdleme4  35525  cdleme4a  35526  cdleme5  35527  cdleme7aa  35529  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme8  35537  cdleme9b  35539  cdleme9  35540  cdleme10  35541  cdleme11fN  35551  cdleme11g  35552  cdleme11k  35555  cdleme13  35559  cdleme15b  35562  cdleme15d  35564  cdleme15  35565  cdleme16e  35569  cdleme16f  35570  cdleme22gb  35581  cdlemedb  35584  cdlemednpq  35586  cdleme19b  35592  cdleme19c  35593  cdleme20aN  35597  cdleme20c  35599  cdleme20d  35600  cdleme20e  35601  cdleme20j  35606  cdleme21c  35615  cdleme21ct  35617  cdleme22aa  35627  cdleme22cN  35630  cdleme22d  35631  cdleme22e  35632  cdleme22eALTN  35633  cdleme22f  35634  cdleme22g  35636  cdleme23a  35637  cdleme23b  35638  cdleme23c  35639  cdleme28a  35658  cdleme28b  35659  cdleme29ex  35662  cdleme30a  35666  cdlemefr29exN  35690  cdleme32b  35730  cdleme32c  35731  cdleme32e  35733  cdleme35b  35738  cdleme35c  35739  cdleme35d  35740  cdleme35e  35741  cdleme35f  35742  cdleme42a  35759  cdleme42c  35760  cdleme42h  35770  cdleme42i  35771  cdleme48bw  35790  cdlemeg46frv  35813  cdlemeg46vrg  35815  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemf1  35849  cdlemf2  35850  trlord  35857  cdlemg2fv2  35888  cdlemg2m  35892  cdlemg7fvbwN  35895  cdlemg4  35905  cdlemg6c  35908  cdlemg10bALTN  35924  cdlemg10c  35927  cdlemg10  35929  cdlemg11b  35930  cdlemg12f  35936  cdlemg17a  35949  cdlemg17dALTN  35952  cdlemg19a  35971  cdlemg35  36001  trlcoabs2N  36010  trlcolem  36014  cdlemh2  36104  cdlemi1  36106  cdlemk3  36121  cdlemk4  36122  cdlemk9  36127  cdlemk9bN  36128  cdlemk10  36131  cdlemk39  36204  dia0eldmN  36329  dia1eldmN  36330  dia0  36341  dia1N  36342  diaglbN  36344  diaintclN  36347  dia2dimlem1  36353  dia2dimlem2  36354  dia2dimlem3  36355  dia2dimlem10  36362  dia2dimlem12  36364  cdlemm10N  36407  docaclN  36413  doca2N  36415  djajN  36426  dib0  36453  dibglbN  36455  dibintclN  36456  cdlemn2  36484  cdlemn10  36495  dihjustlem  36505  dihord1  36507  dihord2a  36508  dihord2b  36509  dihord2cN  36510  dihord11b  36511  dihord11c  36513  dihord2pre  36514  dihord2pre2  36515  dihlsscpre  36523  dib2dim  36532  dih2dimb  36533  dih2dimbALTN  36534  dihvalcq2  36536  dihopelvalcpre  36537  dihord6apre  36545  dihord5b  36548  dihord6b  36549  dihord5apre  36551  dih0  36569  dih1  36575  dihwN  36578  dihmeetlem1N  36579  dihglblem5apreN  36580  dihglblem5aN  36581  dihglblem2aN  36582  dihglblem2N  36583  dihglblem3N  36584  dihmeetlem2N  36588  dihglbcpreN  36589  dihmeetbclemN  36593  dihmeetlem3N  36594  dihmeetlem4preN  36595  dihmeetlem6  36598  dihjatc1  36600  dihmeetlem18N  36613  dih1dimatlem  36618  dihjatcclem1  36707  dihjatcclem2  36708  dihjatcclem4  36710