Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lhpbase Unicode version

Theorem lhpbase 30480
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
StepHypRef Expression
1 n0i 3593 . . . 4  |-  ( W  e.  H  ->  -.  H  =  (/) )
2 lhpbase.h . . . . 5  |-  H  =  ( LHyp `  K
)
32eqeq1i 2411 . . . 4  |-  ( H  =  (/)  <->  ( LHyp `  K
)  =  (/) )
41, 3sylnib 296 . . 3  |-  ( W  e.  H  ->  -.  ( LHyp `  K )  =  (/) )
5 fvprc 5681 . . 3  |-  ( -.  K  e.  _V  ->  (
LHyp `  K )  =  (/) )
64, 5nsyl2 121 . 2  |-  ( W  e.  H  ->  K  e.  _V )
7 lhpbase.b . . . 4  |-  B  =  ( Base `  K
)
8 eqid 2404 . . . 4  |-  ( 1.
`  K )  =  ( 1. `  K
)
9 eqid 2404 . . . 4  |-  (  <o  `  K )  =  ( 
<o  `  K )
107, 8, 9, 2islhp 30478 . . 3  |-  ( K  e.  _V  ->  ( W  e.  H  <->  ( W  e.  B  /\  W ( 
<o  `  K ) ( 1. `  K ) ) ) )
1110simprbda 607 . 2  |-  ( ( K  e.  _V  /\  W  e.  H )  ->  W  e.  B )
126, 11mpancom 651 1  |-  ( W  e.  H  ->  W  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721   _Vcvv 2916   (/)c0 3588   class class class wbr 4172   ` cfv 5413   Basecbs 13424   1.cp1 14422    <o ccvr 29745   LHypclh 30466
This theorem is referenced by:  lhplt  30482  lhp2lt  30483  lhpexlt  30484  lhp0lt  30485  lhpexle  30487  lhpexnle  30488  lhpexle1  30490  lhpexle2lem  30491  lhpexle3lem  30493  lhpocnle  30498  lhpocat  30499  lhpjat1  30502  lhpjat2  30503  lhpj1  30504  lhpmcvr  30505  lhpmcvr2  30506  lhpmcvr3  30507  lhpmcvr4N  30508  lhpmcvr5N  30509  lhpmcvr6N  30510  lhpm0atN  30511  lhpmat  30512  lhpmatb  30513  lhp2at0  30514  lhpelim  30519  lhpmod2i2  30520  lhpmod6i1  30521  cdlemb2  30523  lhpat  30525  lhpat3  30528  4atexlemwb  30541  ltrnatb  30619  ltrnel  30621  ltrncnvel  30624  ltrnmw  30633  trlval2  30645  trlcl  30646  trljat1  30648  trljat2  30649  trlle  30666  trlval3  30669  cdlemc1  30673  cdlemc2  30674  cdlemc4  30676  cdlemc5  30677  cdlemc6  30678  cdlemd2  30681  cdleme0aa  30692  cdleme0b  30694  cdleme0c  30695  cdleme0cp  30696  cdleme0cq  30697  cdleme0e  30699  cdleme0fN  30700  cdlemeulpq  30702  cdleme01N  30703  cdleme0ex1N  30705  cdleme1b  30708  cdleme1  30709  cdleme2  30710  cdleme3b  30711  cdleme3c  30712  cdleme3g  30716  cdleme3h  30717  cdleme3  30719  cdleme4  30720  cdleme4a  30721  cdleme5  30722  cdleme7aa  30724  cdleme7c  30727  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme8  30732  cdleme9b  30734  cdleme9  30735  cdleme10  30736  cdleme11fN  30746  cdleme11g  30747  cdleme11k  30750  cdleme13  30754  cdleme15b  30757  cdleme15d  30759  cdleme15  30760  cdleme16e  30764  cdleme16f  30765  cdleme22gb  30776  cdlemedb  30779  cdlemednpq  30781  cdleme19b  30786  cdleme19c  30787  cdleme20aN  30791  cdleme20c  30793  cdleme20d  30794  cdleme20e  30795  cdleme20j  30800  cdleme21c  30809  cdleme21ct  30811  cdleme22aa  30821  cdleme22cN  30824  cdleme22d  30825  cdleme22e  30826  cdleme22eALTN  30827  cdleme22f  30828  cdleme22g  30830  cdleme23a  30831  cdleme23b  30832  cdleme23c  30833  cdleme28a  30852  cdleme28b  30853  cdleme29ex  30856  cdleme30a  30860  cdlemefr29exN  30884  cdleme32b  30924  cdleme32c  30925  cdleme32e  30927  cdleme35b  30932  cdleme35c  30933  cdleme35d  30934  cdleme35e  30935  cdleme35f  30936  cdleme42a  30953  cdleme42c  30954  cdleme42h  30964  cdleme42i  30965  cdleme48bw  30984  cdlemeg46frv  31007  cdlemeg46vrg  31009  cdlemeg46rgv  31010  cdlemeg46req  31011  cdlemf1  31043  cdlemf2  31044  trlord  31051  cdlemg2fv2  31082  cdlemg2m  31086  cdlemg7fvbwN  31089  cdlemg4  31099  cdlemg6c  31102  cdlemg10bALTN  31118  cdlemg10c  31121  cdlemg10  31123  cdlemg11b  31124  cdlemg12f  31130  cdlemg17a  31143  cdlemg17dALTN  31146  cdlemg19a  31165  cdlemg35  31195  trlcoabs2N  31204  trlcolem  31208  cdlemh2  31298  cdlemi1  31300  cdlemk3  31315  cdlemk4  31316  cdlemk9  31321  cdlemk9bN  31322  cdlemk10  31325  cdlemk39  31398  dia0eldmN  31523  dia1eldmN  31524  dia0  31535  dia1N  31536  diaglbN  31538  diaintclN  31541  dia2dimlem1  31547  dia2dimlem2  31548  dia2dimlem3  31549  dia2dimlem10  31556  dia2dimlem12  31558  cdlemm10N  31601  docaclN  31607  doca2N  31609  djajN  31620  dib0  31647  dibglbN  31649  dibintclN  31650  cdlemn2  31678  cdlemn10  31689  dihjustlem  31699  dihord1  31701  dihord2a  31702  dihord2b  31703  dihord2cN  31704  dihord11b  31705  dihord11c  31707  dihord2pre  31708  dihord2pre2  31709  dihlsscpre  31717  dib2dim  31726  dih2dimb  31727  dih2dimbALTN  31728  dihvalcq2  31730  dihopelvalcpre  31731  dihord6apre  31739  dihord5b  31742  dihord6b  31743  dihord5apre  31745  dih0  31763  dih1  31769  dihwN  31772  dihmeetlem1N  31773  dihglblem5apreN  31774  dihglblem5aN  31775  dihglblem2aN  31776  dihglblem2N  31777  dihglblem3N  31778  dihmeetlem2N  31782  dihglbcpreN  31783  dihmeetbclemN  31787  dihmeetlem3N  31788  dihmeetlem4preN  31789  dihmeetlem6  31792  dihjatc1  31794  dihmeetlem18N  31807  dih1dimatlem  31812  dihjatcclem1  31901  dihjatcclem2  31902  dihjatcclem4  31904
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-iota 5377  df-fun 5415  df-fv 5421  df-lhyp 30470
  Copyright terms: Public domain W3C validator