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

Theorem lhpbase 30260
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 3462 . . . 4  |-  ( W  e.  H  ->  -.  H  =  (/) )
2 lhpbase.h . . . . 5  |-  H  =  ( LHyp `  K
)
32eqeq1i 2292 . . . 4  |-  ( H  =  (/)  <->  ( LHyp `  K
)  =  (/) )
41, 3sylnib 295 . . 3  |-  ( W  e.  H  ->  -.  ( LHyp `  K )  =  (/) )
5 fvprc 5521 . . 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 2285 . . . 4  |-  ( 1.
`  K )  =  ( 1. `  K
)
9 eqid 2285 . . . 4  |-  (  <o  `  K )  =  ( 
<o  `  K )
107, 8, 9, 2islhp 30258 . . 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 1625    e. wcel 1686   _Vcvv 2790   (/)c0 3457   class class class wbr 4025   ` cfv 5257   Basecbs 13150   1.cp1 14146    <o ccvr 29525   LHypclh 30246
This theorem is referenced by:  lhplt  30262  lhp2lt  30263  lhpexlt  30264  lhp0lt  30265  lhpexle  30267  lhpexnle  30268  lhpexle1  30270  lhpexle2lem  30271  lhpexle3lem  30273  lhpocnle  30278  lhpocat  30279  lhpjat1  30282  lhpjat2  30283  lhpj1  30284  lhpmcvr  30285  lhpmcvr2  30286  lhpmcvr3  30287  lhpmcvr4N  30288  lhpmcvr5N  30289  lhpmcvr6N  30290  lhpm0atN  30291  lhpmat  30292  lhpmatb  30293  lhp2at0  30294  lhpelim  30299  lhpmod2i2  30300  lhpmod6i1  30301  cdlemb2  30303  lhpat  30305  lhpat3  30308  4atexlemwb  30321  ltrnatb  30399  ltrnel  30401  ltrncnvel  30404  ltrnmw  30413  trlval2  30425  trlcl  30426  trljat1  30428  trljat2  30429  trlle  30446  trlval3  30449  cdlemc1  30453  cdlemc2  30454  cdlemc4  30456  cdlemc5  30457  cdlemc6  30458  cdlemd2  30461  cdleme0aa  30472  cdleme0b  30474  cdleme0c  30475  cdleme0cp  30476  cdleme0cq  30477  cdleme0e  30479  cdleme0fN  30480  cdlemeulpq  30482  cdleme01N  30483  cdleme0ex1N  30485  cdleme1b  30488  cdleme1  30489  cdleme2  30490  cdleme3b  30491  cdleme3c  30492  cdleme3g  30496  cdleme3h  30497  cdleme3  30499  cdleme4  30500  cdleme4a  30501  cdleme5  30502  cdleme7aa  30504  cdleme7c  30507  cdleme7d  30508  cdleme7e  30509  cdleme7ga  30510  cdleme7  30511  cdleme8  30512  cdleme9b  30514  cdleme9  30515  cdleme10  30516  cdleme11fN  30526  cdleme11g  30527  cdleme11k  30530  cdleme13  30534  cdleme15b  30537  cdleme15d  30539  cdleme15  30540  cdleme16e  30544  cdleme16f  30545  cdleme22gb  30556  cdlemedb  30559  cdlemednpq  30561  cdleme19b  30566  cdleme19c  30567  cdleme20aN  30571  cdleme20c  30573  cdleme20d  30574  cdleme20e  30575  cdleme20j  30580  cdleme21c  30589  cdleme21ct  30591  cdleme22aa  30601  cdleme22cN  30604  cdleme22d  30605  cdleme22e  30606  cdleme22eALTN  30607  cdleme22f  30608  cdleme22g  30610  cdleme23a  30611  cdleme23b  30612  cdleme23c  30613  cdleme28a  30632  cdleme28b  30633  cdleme29ex  30636  cdleme30a  30640  cdlemefr29exN  30664  cdleme32b  30704  cdleme32c  30705  cdleme32e  30707  cdleme35b  30712  cdleme35c  30713  cdleme35d  30714  cdleme35e  30715  cdleme35f  30716  cdleme42a  30733  cdleme42c  30734  cdleme42h  30744  cdleme42i  30745  cdleme48bw  30764  cdlemeg46frv  30787  cdlemeg46vrg  30789  cdlemeg46rgv  30790  cdlemeg46req  30791  cdlemf1  30823  cdlemf2  30824  trlord  30831  cdlemg2fv2  30862  cdlemg2m  30866  cdlemg7fvbwN  30869  cdlemg4  30879  cdlemg6c  30882  cdlemg10bALTN  30898  cdlemg10c  30901  cdlemg10  30903  cdlemg11b  30904  cdlemg12f  30910  cdlemg17a  30923  cdlemg17dALTN  30926  cdlemg19a  30945  cdlemg35  30975  trlcoabs2N  30984  trlcolem  30988  cdlemh2  31078  cdlemi1  31080  cdlemk3  31095  cdlemk4  31096  cdlemk9  31101  cdlemk9bN  31102  cdlemk10  31105  cdlemk39  31178  dia0eldmN  31303  dia1eldmN  31304  dia0  31315  dia1N  31316  diaglbN  31318  diaintclN  31321  dia2dimlem1  31327  dia2dimlem2  31328  dia2dimlem3  31329  dia2dimlem10  31336  dia2dimlem12  31338  cdlemm10N  31381  docaclN  31387  doca2N  31389  djajN  31400  dib0  31427  dibglbN  31429  dibintclN  31430  cdlemn2  31458  cdlemn10  31469  dihjustlem  31479  dihord1  31481  dihord2a  31482  dihord2b  31483  dihord2cN  31484  dihord11b  31485  dihord11c  31487  dihord2pre  31488  dihord2pre2  31489  dihlsscpre  31497  dib2dim  31506  dih2dimb  31507  dih2dimbALTN  31508  dihvalcq2  31510  dihopelvalcpre  31511  dihord6apre  31519  dihord5b  31522  dihord6b  31523  dihord5apre  31525  dih0  31543  dih1  31549  dihwN  31552  dihmeetlem1N  31553  dihglblem5apreN  31554  dihglblem5aN  31555  dihglblem2aN  31556  dihglblem2N  31557  dihglblem3N  31558  dihmeetlem2N  31562  dihglbcpreN  31563  dihmeetbclemN  31567  dihmeetlem3N  31568  dihmeetlem4preN  31569  dihmeetlem6  31572  dihjatc1  31574  dihmeetlem18N  31587  dih1dimatlem  31592  dihjatcclem1  31681  dihjatcclem2  31682  dihjatcclem4  31684
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-iota 5221  df-fun 5259  df-fv 5265  df-lhyp 30250
  Copyright terms: Public domain W3C validator