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

Theorem lhpbase 30809
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 3473 . . . 4  |-  ( W  e.  H  ->  -.  H  =  (/) )
2 lhpbase.h . . . . 5  |-  H  =  ( LHyp `  K
)
32eqeq1i 2303 . . . 4  |-  ( H  =  (/)  <->  ( LHyp `  K
)  =  (/) )
41, 3sylnib 295 . . 3  |-  ( W  e.  H  ->  -.  ( LHyp `  K )  =  (/) )
5 fvprc 5535 . . 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 2296 . . . 4  |-  ( 1.
`  K )  =  ( 1. `  K
)
9 eqid 2296 . . . 4  |-  (  <o  `  K )  =  ( 
<o  `  K )
107, 8, 9, 2islhp 30807 . . 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 1632    e. wcel 1696   _Vcvv 2801   (/)c0 3468   class class class wbr 4039   ` cfv 5271   Basecbs 13164   1.cp1 14160    <o ccvr 30074   LHypclh 30795
This theorem is referenced by:  lhplt  30811  lhp2lt  30812  lhpexlt  30813  lhp0lt  30814  lhpexle  30816  lhpexnle  30817  lhpexle1  30819  lhpexle2lem  30820  lhpexle3lem  30822  lhpocnle  30827  lhpocat  30828  lhpjat1  30831  lhpjat2  30832  lhpj1  30833  lhpmcvr  30834  lhpmcvr2  30835  lhpmcvr3  30836  lhpmcvr4N  30837  lhpmcvr5N  30838  lhpmcvr6N  30839  lhpm0atN  30840  lhpmat  30841  lhpmatb  30842  lhp2at0  30843  lhpelim  30848  lhpmod2i2  30849  lhpmod6i1  30850  cdlemb2  30852  lhpat  30854  lhpat3  30857  4atexlemwb  30870  ltrnatb  30948  ltrnel  30950  ltrncnvel  30953  ltrnmw  30962  trlval2  30974  trlcl  30975  trljat1  30977  trljat2  30978  trlle  30995  trlval3  30998  cdlemc1  31002  cdlemc2  31003  cdlemc4  31005  cdlemc5  31006  cdlemc6  31007  cdlemd2  31010  cdleme0aa  31021  cdleme0b  31023  cdleme0c  31024  cdleme0cp  31025  cdleme0cq  31026  cdleme0e  31028  cdleme0fN  31029  cdlemeulpq  31031  cdleme01N  31032  cdleme0ex1N  31034  cdleme1b  31037  cdleme1  31038  cdleme2  31039  cdleme3b  31040  cdleme3c  31041  cdleme3g  31045  cdleme3h  31046  cdleme3  31048  cdleme4  31049  cdleme4a  31050  cdleme5  31051  cdleme7aa  31053  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme7  31060  cdleme8  31061  cdleme9b  31063  cdleme9  31064  cdleme10  31065  cdleme11fN  31075  cdleme11g  31076  cdleme11k  31079  cdleme13  31083  cdleme15b  31086  cdleme15d  31088  cdleme15  31089  cdleme16e  31093  cdleme16f  31094  cdleme22gb  31105  cdlemedb  31108  cdlemednpq  31110  cdleme19b  31115  cdleme19c  31116  cdleme20aN  31120  cdleme20c  31122  cdleme20d  31123  cdleme20e  31124  cdleme20j  31129  cdleme21c  31138  cdleme21ct  31140  cdleme22aa  31150  cdleme22cN  31153  cdleme22d  31154  cdleme22e  31155  cdleme22eALTN  31156  cdleme22f  31157  cdleme22g  31159  cdleme23a  31160  cdleme23b  31161  cdleme23c  31162  cdleme28a  31181  cdleme28b  31182  cdleme29ex  31185  cdleme30a  31189  cdlemefr29exN  31213  cdleme32b  31253  cdleme32c  31254  cdleme32e  31256  cdleme35b  31261  cdleme35c  31262  cdleme35d  31263  cdleme35e  31264  cdleme35f  31265  cdleme42a  31282  cdleme42c  31283  cdleme42h  31293  cdleme42i  31294  cdleme48bw  31313  cdlemeg46frv  31336  cdlemeg46vrg  31338  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemf1  31372  cdlemf2  31373  trlord  31380  cdlemg2fv2  31411  cdlemg2m  31415  cdlemg7fvbwN  31418  cdlemg4  31428  cdlemg6c  31431  cdlemg10bALTN  31447  cdlemg10c  31450  cdlemg10  31452  cdlemg11b  31453  cdlemg12f  31459  cdlemg17a  31472  cdlemg17dALTN  31475  cdlemg19a  31494  cdlemg35  31524  trlcoabs2N  31533  trlcolem  31537  cdlemh2  31627  cdlemi1  31629  cdlemk3  31644  cdlemk4  31645  cdlemk9  31650  cdlemk9bN  31651  cdlemk10  31654  cdlemk39  31727  dia0eldmN  31852  dia1eldmN  31853  dia0  31864  dia1N  31865  diaglbN  31867  diaintclN  31870  dia2dimlem1  31876  dia2dimlem2  31877  dia2dimlem3  31878  dia2dimlem10  31885  dia2dimlem12  31887  cdlemm10N  31930  docaclN  31936  doca2N  31938  djajN  31949  dib0  31976  dibglbN  31978  dibintclN  31979  cdlemn2  32007  cdlemn10  32018  dihjustlem  32028  dihord1  32030  dihord2a  32031  dihord2b  32032  dihord2cN  32033  dihord11b  32034  dihord11c  32036  dihord2pre  32037  dihord2pre2  32038  dihlsscpre  32046  dib2dim  32055  dih2dimb  32056  dih2dimbALTN  32057  dihvalcq2  32059  dihopelvalcpre  32060  dihord6apre  32068  dihord5b  32071  dihord6b  32072  dihord5apre  32074  dih0  32092  dih1  32098  dihwN  32101  dihmeetlem1N  32102  dihglblem5apreN  32103  dihglblem5aN  32104  dihglblem2aN  32105  dihglblem2N  32106  dihglblem3N  32107  dihmeetlem2N  32111  dihglbcpreN  32112  dihmeetbclemN  32116  dihmeetlem3N  32117  dihmeetlem4preN  32118  dihmeetlem6  32121  dihjatc1  32123  dihmeetlem18N  32136  dih1dimatlem  32141  dihjatcclem1  32230  dihjatcclem2  32231  dihjatcclem4  32233
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-iota 5235  df-fun 5273  df-fv 5279  df-lhyp 30799
  Copyright terms: Public domain W3C validator