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

Theorem lhpbase 29466
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 3461 . . . 4  |-  ( W  e.  H  ->  -.  H  =  (/) )
2 lhpbase.h . . . . 5  |-  H  =  ( LHyp `  K
)
32eqeq1i 2291 . . . 4  |-  ( H  =  (/)  <->  ( LHyp `  K
)  =  (/) )
41, 3sylnib 295 . . 3  |-  ( W  e.  H  ->  -.  ( LHyp `  K )  =  (/) )
5 fvprc 5483 . . 3  |-  ( -.  K  e.  _V  ->  (
LHyp `  K )  =  (/) )
64, 5nsyl2 119 . 2  |-  ( W  e.  H  ->  K  e.  _V )
7 lhpbase.b . . . 4  |-  B  =  ( Base `  K
)
8 eqid 2284 . . . 4  |-  ( 1.
`  K )  =  ( 1. `  K
)
9 eqid 2284 . . . 4  |-  (  <o  `  K )  =  ( 
<o  `  K )
107, 8, 9, 2islhp 29464 . . 3  |-  ( K  e.  _V  ->  ( W  e.  H  <->  ( W  e.  B  /\  W ( 
<o  `  K ) ( 1. `  K ) ) ) )
1110simprbda 606 . 2  |-  ( ( K  e.  _V  /\  W  e.  H )  ->  W  e.  B )
126, 11mpancom 650 1  |-  ( W  e.  H  ->  W  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1685   _Vcvv 2789   (/)c0 3456   class class class wbr 4024   ` cfv 5221   Basecbs 13144   1.cp1 14140    <o ccvr 28731   LHypclh 29452
This theorem is referenced by:  lhplt  29468  lhp2lt  29469  lhpexlt  29470  lhp0lt  29471  lhpexle  29473  lhpexnle  29474  lhpexle1  29476  lhpexle2lem  29477  lhpexle3lem  29479  lhpocnle  29484  lhpocat  29485  lhpjat1  29488  lhpjat2  29489  lhpj1  29490  lhpmcvr  29491  lhpmcvr2  29492  lhpmcvr3  29493  lhpmcvr4N  29494  lhpmcvr5N  29495  lhpmcvr6N  29496  lhpm0atN  29497  lhpmat  29498  lhpmatb  29499  lhp2at0  29500  lhpelim  29505  lhpmod2i2  29506  lhpmod6i1  29507  cdlemb2  29509  lhpat  29511  lhpat3  29514  4atexlemwb  29527  ltrnatb  29605  ltrnel  29607  ltrncnvel  29610  ltrnmw  29619  trlval2  29631  trlcl  29632  trljat1  29634  trljat2  29635  trlle  29652  trlval3  29655  cdlemc1  29659  cdlemc2  29660  cdlemc4  29662  cdlemc5  29663  cdlemc6  29664  cdlemd2  29667  cdleme0aa  29678  cdleme0b  29680  cdleme0c  29681  cdleme0cp  29682  cdleme0cq  29683  cdleme0e  29685  cdleme0fN  29686  cdlemeulpq  29688  cdleme01N  29689  cdleme0ex1N  29691  cdleme1b  29694  cdleme1  29695  cdleme2  29696  cdleme3b  29697  cdleme3c  29698  cdleme3g  29702  cdleme3h  29703  cdleme3  29705  cdleme4  29706  cdleme4a  29707  cdleme5  29708  cdleme7aa  29710  cdleme7c  29713  cdleme7d  29714  cdleme7e  29715  cdleme7ga  29716  cdleme7  29717  cdleme8  29718  cdleme9b  29720  cdleme9  29721  cdleme10  29722  cdleme11fN  29732  cdleme11g  29733  cdleme11k  29736  cdleme13  29740  cdleme15b  29743  cdleme15d  29745  cdleme15  29746  cdleme16e  29750  cdleme16f  29751  cdleme22gb  29762  cdlemedb  29765  cdlemednpq  29767  cdleme19b  29772  cdleme19c  29773  cdleme20aN  29777  cdleme20c  29779  cdleme20d  29780  cdleme20e  29781  cdleme20j  29786  cdleme21c  29795  cdleme21ct  29797  cdleme22aa  29807  cdleme22cN  29810  cdleme22d  29811  cdleme22e  29812  cdleme22eALTN  29813  cdleme22f  29814  cdleme22g  29816  cdleme23a  29817  cdleme23b  29818  cdleme23c  29819  cdleme28a  29838  cdleme28b  29839  cdleme29ex  29842  cdleme30a  29846  cdlemefr29exN  29870  cdleme32b  29910  cdleme32c  29911  cdleme32e  29913  cdleme35b  29918  cdleme35c  29919  cdleme35d  29920  cdleme35e  29921  cdleme35f  29922  cdleme42a  29939  cdleme42c  29940  cdleme42h  29950  cdleme42i  29951  cdleme48bw  29970  cdlemeg46frv  29993  cdlemeg46vrg  29995  cdlemeg46rgv  29996  cdlemeg46req  29997  cdlemf1  30029  cdlemf2  30030  trlord  30037  cdlemg2fv2  30068  cdlemg2m  30072  cdlemg7fvbwN  30075  cdlemg4  30085  cdlemg6c  30088  cdlemg10bALTN  30104  cdlemg10c  30107  cdlemg10  30109  cdlemg11b  30110  cdlemg12f  30116  cdlemg17a  30129  cdlemg17dALTN  30132  cdlemg19a  30151  cdlemg35  30181  trlcoabs2N  30190  trlcolem  30194  cdlemh2  30284  cdlemi1  30286  cdlemk3  30301  cdlemk4  30302  cdlemk9  30307  cdlemk9bN  30308  cdlemk10  30311  cdlemk39  30384  dia0eldmN  30509  dia1eldmN  30510  dia0  30521  dia1N  30522  diaglbN  30524  diaintclN  30527  dia2dimlem1  30533  dia2dimlem2  30534  dia2dimlem3  30535  dia2dimlem10  30542  dia2dimlem12  30544  cdlemm10N  30587  docaclN  30593  doca2N  30595  djajN  30606  dib0  30633  dibglbN  30635  dibintclN  30636  cdlemn2  30664  cdlemn10  30675  dihjustlem  30685  dihord1  30687  dihord2a  30688  dihord2b  30689  dihord2cN  30690  dihord11b  30691  dihord11c  30693  dihord2pre  30694  dihord2pre2  30695  dihlsscpre  30703  dib2dim  30712  dih2dimb  30713  dih2dimbALTN  30714  dihvalcq2  30716  dihopelvalcpre  30717  dihord6apre  30725  dihord5b  30728  dihord6b  30729  dihord5apre  30731  dih0  30749  dih1  30755  dihwN  30758  dihmeetlem1N  30759  dihglblem5apreN  30760  dihglblem5aN  30761  dihglblem2aN  30762  dihglblem2N  30763  dihglblem3N  30764  dihmeetlem2N  30768  dihglbcpreN  30769  dihmeetbclemN  30773  dihmeetlem3N  30774  dihmeetlem4preN  30775  dihmeetlem6  30778  dihjatc1  30780  dihmeetlem18N  30793  dih1dimatlem  30798  dihjatcclem1  30887  dihjatcclem2  30888  dihjatcclem4  30890
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-mpt 4080  df-id 4308  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fv 5229  df-lhyp 29456
  Copyright terms: Public domain W3C validator