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

Theorem lhpbase 30869
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 3635 . . . 4  |-  ( W  e.  H  ->  -.  H  =  (/) )
2 lhpbase.h . . . . 5  |-  H  =  ( LHyp `  K
)
32eqeq1i 2445 . . . 4  |-  ( H  =  (/)  <->  ( LHyp `  K
)  =  (/) )
41, 3sylnib 297 . . 3  |-  ( W  e.  H  ->  -.  ( LHyp `  K )  =  (/) )
5 fvprc 5725 . . 3  |-  ( -.  K  e.  _V  ->  (
LHyp `  K )  =  (/) )
64, 5nsyl2 122 . 2  |-  ( W  e.  H  ->  K  e.  _V )
7 lhpbase.b . . . 4  |-  B  =  ( Base `  K
)
8 eqid 2438 . . . 4  |-  ( 1.
`  K )  =  ( 1. `  K
)
9 eqid 2438 . . . 4  |-  (  <o  `  K )  =  ( 
<o  `  K )
107, 8, 9, 2islhp 30867 . . 3  |-  ( K  e.  _V  ->  ( W  e.  H  <->  ( W  e.  B  /\  W ( 
<o  `  K ) ( 1. `  K ) ) ) )
1110simprbda 608 . 2  |-  ( ( K  e.  _V  /\  W  e.  H )  ->  W  e.  B )
126, 11mpancom 652 1  |-  ( W  e.  H  ->  W  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726   _Vcvv 2958   (/)c0 3630   class class class wbr 4215   ` cfv 5457   Basecbs 13474   1.cp1 14472    <o ccvr 30134   LHypclh 30855
This theorem is referenced by:  lhplt  30871  lhp2lt  30872  lhpexlt  30873  lhp0lt  30874  lhpexle  30876  lhpexnle  30877  lhpexle1  30879  lhpexle2lem  30880  lhpexle3lem  30882  lhpocnle  30887  lhpocat  30888  lhpjat1  30891  lhpjat2  30892  lhpj1  30893  lhpmcvr  30894  lhpmcvr2  30895  lhpmcvr3  30896  lhpmcvr4N  30897  lhpmcvr5N  30898  lhpmcvr6N  30899  lhpm0atN  30900  lhpmat  30901  lhpmatb  30902  lhp2at0  30903  lhpelim  30908  lhpmod2i2  30909  lhpmod6i1  30910  cdlemb2  30912  lhpat  30914  lhpat3  30917  4atexlemwb  30930  ltrnatb  31008  ltrnel  31010  ltrncnvel  31013  ltrnmw  31022  trlval2  31034  trlcl  31035  trljat1  31037  trljat2  31038  trlle  31055  trlval3  31058  cdlemc1  31062  cdlemc2  31063  cdlemc4  31065  cdlemc5  31066  cdlemc6  31067  cdlemd2  31070  cdleme0aa  31081  cdleme0b  31083  cdleme0c  31084  cdleme0cp  31085  cdleme0cq  31086  cdleme0e  31088  cdleme0fN  31089  cdlemeulpq  31091  cdleme01N  31092  cdleme0ex1N  31094  cdleme1b  31097  cdleme1  31098  cdleme2  31099  cdleme3b  31100  cdleme3c  31101  cdleme3g  31105  cdleme3h  31106  cdleme3  31108  cdleme4  31109  cdleme4a  31110  cdleme5  31111  cdleme7aa  31113  cdleme7c  31116  cdleme7d  31117  cdleme7e  31118  cdleme7ga  31119  cdleme7  31120  cdleme8  31121  cdleme9b  31123  cdleme9  31124  cdleme10  31125  cdleme11fN  31135  cdleme11g  31136  cdleme11k  31139  cdleme13  31143  cdleme15b  31146  cdleme15d  31148  cdleme15  31149  cdleme16e  31153  cdleme16f  31154  cdleme22gb  31165  cdlemedb  31168  cdlemednpq  31170  cdleme19b  31175  cdleme19c  31176  cdleme20aN  31180  cdleme20c  31182  cdleme20d  31183  cdleme20e  31184  cdleme20j  31189  cdleme21c  31198  cdleme21ct  31200  cdleme22aa  31210  cdleme22cN  31213  cdleme22d  31214  cdleme22e  31215  cdleme22eALTN  31216  cdleme22f  31217  cdleme22g  31219  cdleme23a  31220  cdleme23b  31221  cdleme23c  31222  cdleme28a  31241  cdleme28b  31242  cdleme29ex  31245  cdleme30a  31249  cdlemefr29exN  31273  cdleme32b  31313  cdleme32c  31314  cdleme32e  31316  cdleme35b  31321  cdleme35c  31322  cdleme35d  31323  cdleme35e  31324  cdleme35f  31325  cdleme42a  31342  cdleme42c  31343  cdleme42h  31353  cdleme42i  31354  cdleme48bw  31373  cdlemeg46frv  31396  cdlemeg46vrg  31398  cdlemeg46rgv  31399  cdlemeg46req  31400  cdlemf1  31432  cdlemf2  31433  trlord  31440  cdlemg2fv2  31471  cdlemg2m  31475  cdlemg7fvbwN  31478  cdlemg4  31488  cdlemg6c  31491  cdlemg10bALTN  31507  cdlemg10c  31510  cdlemg10  31512  cdlemg11b  31513  cdlemg12f  31519  cdlemg17a  31532  cdlemg17dALTN  31535  cdlemg19a  31554  cdlemg35  31584  trlcoabs2N  31593  trlcolem  31597  cdlemh2  31687  cdlemi1  31689  cdlemk3  31704  cdlemk4  31705  cdlemk9  31710  cdlemk9bN  31711  cdlemk10  31714  cdlemk39  31787  dia0eldmN  31912  dia1eldmN  31913  dia0  31924  dia1N  31925  diaglbN  31927  diaintclN  31930  dia2dimlem1  31936  dia2dimlem2  31937  dia2dimlem3  31938  dia2dimlem10  31945  dia2dimlem12  31947  cdlemm10N  31990  docaclN  31996  doca2N  31998  djajN  32009  dib0  32036  dibglbN  32038  dibintclN  32039  cdlemn2  32067  cdlemn10  32078  dihjustlem  32088  dihord1  32090  dihord2a  32091  dihord2b  32092  dihord2cN  32093  dihord11b  32094  dihord11c  32096  dihord2pre  32097  dihord2pre2  32098  dihlsscpre  32106  dib2dim  32115  dih2dimb  32116  dih2dimbALTN  32117  dihvalcq2  32119  dihopelvalcpre  32120  dihord6apre  32128  dihord5b  32131  dihord6b  32132  dihord5apre  32134  dih0  32152  dih1  32158  dihwN  32161  dihmeetlem1N  32162  dihglblem5apreN  32163  dihglblem5aN  32164  dihglblem2aN  32165  dihglblem2N  32166  dihglblem3N  32167  dihmeetlem2N  32171  dihglbcpreN  32172  dihmeetbclemN  32176  dihmeetlem3N  32177  dihmeetlem4preN  32178  dihmeetlem6  32181  dihjatc1  32183  dihmeetlem18N  32196  dih1dimatlem  32201  dihjatcclem1  32290  dihjatcclem2  32291  dihjatcclem4  32293
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-iota 5421  df-fun 5459  df-fv 5465  df-lhyp 30859
  Copyright terms: Public domain W3C validator