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

Theorem lhpbase 30733
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 3626 . . . 4  |-  ( W  e.  H  ->  -.  H  =  (/) )
2 lhpbase.h . . . . 5  |-  H  =  ( LHyp `  K
)
32eqeq1i 2443 . . . 4  |-  ( H  =  (/)  <->  ( LHyp `  K
)  =  (/) )
41, 3sylnib 296 . . 3  |-  ( W  e.  H  ->  -.  ( LHyp `  K )  =  (/) )
5 fvprc 5715 . . 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 2436 . . . 4  |-  ( 1.
`  K )  =  ( 1. `  K
)
9 eqid 2436 . . . 4  |-  (  <o  `  K )  =  ( 
<o  `  K )
107, 8, 9, 2islhp 30731 . . 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 1652    e. wcel 1725   _Vcvv 2949   (/)c0 3621   class class class wbr 4205   ` cfv 5447   Basecbs 13462   1.cp1 14460    <o ccvr 29998   LHypclh 30719
This theorem is referenced by:  lhplt  30735  lhp2lt  30736  lhpexlt  30737  lhp0lt  30738  lhpexle  30740  lhpexnle  30741  lhpexle1  30743  lhpexle2lem  30744  lhpexle3lem  30746  lhpocnle  30751  lhpocat  30752  lhpjat1  30755  lhpjat2  30756  lhpj1  30757  lhpmcvr  30758  lhpmcvr2  30759  lhpmcvr3  30760  lhpmcvr4N  30761  lhpmcvr5N  30762  lhpmcvr6N  30763  lhpm0atN  30764  lhpmat  30765  lhpmatb  30766  lhp2at0  30767  lhpelim  30772  lhpmod2i2  30773  lhpmod6i1  30774  cdlemb2  30776  lhpat  30778  lhpat3  30781  4atexlemwb  30794  ltrnatb  30872  ltrnel  30874  ltrncnvel  30877  ltrnmw  30886  trlval2  30898  trlcl  30899  trljat1  30901  trljat2  30902  trlle  30919  trlval3  30922  cdlemc1  30926  cdlemc2  30927  cdlemc4  30929  cdlemc5  30930  cdlemc6  30931  cdlemd2  30934  cdleme0aa  30945  cdleme0b  30947  cdleme0c  30948  cdleme0cp  30949  cdleme0cq  30950  cdleme0e  30952  cdleme0fN  30953  cdlemeulpq  30955  cdleme01N  30956  cdleme0ex1N  30958  cdleme1b  30961  cdleme1  30962  cdleme2  30963  cdleme3b  30964  cdleme3c  30965  cdleme3g  30969  cdleme3h  30970  cdleme3  30972  cdleme4  30973  cdleme4a  30974  cdleme5  30975  cdleme7aa  30977  cdleme7c  30980  cdleme7d  30981  cdleme7e  30982  cdleme7ga  30983  cdleme7  30984  cdleme8  30985  cdleme9b  30987  cdleme9  30988  cdleme10  30989  cdleme11fN  30999  cdleme11g  31000  cdleme11k  31003  cdleme13  31007  cdleme15b  31010  cdleme15d  31012  cdleme15  31013  cdleme16e  31017  cdleme16f  31018  cdleme22gb  31029  cdlemedb  31032  cdlemednpq  31034  cdleme19b  31039  cdleme19c  31040  cdleme20aN  31044  cdleme20c  31046  cdleme20d  31047  cdleme20e  31048  cdleme20j  31053  cdleme21c  31062  cdleme21ct  31064  cdleme22aa  31074  cdleme22cN  31077  cdleme22d  31078  cdleme22e  31079  cdleme22eALTN  31080  cdleme22f  31081  cdleme22g  31083  cdleme23a  31084  cdleme23b  31085  cdleme23c  31086  cdleme28a  31105  cdleme28b  31106  cdleme29ex  31109  cdleme30a  31113  cdlemefr29exN  31137  cdleme32b  31177  cdleme32c  31178  cdleme32e  31180  cdleme35b  31185  cdleme35c  31186  cdleme35d  31187  cdleme35e  31188  cdleme35f  31189  cdleme42a  31206  cdleme42c  31207  cdleme42h  31217  cdleme42i  31218  cdleme48bw  31237  cdlemeg46frv  31260  cdlemeg46vrg  31262  cdlemeg46rgv  31263  cdlemeg46req  31264  cdlemf1  31296  cdlemf2  31297  trlord  31304  cdlemg2fv2  31335  cdlemg2m  31339  cdlemg7fvbwN  31342  cdlemg4  31352  cdlemg6c  31355  cdlemg10bALTN  31371  cdlemg10c  31374  cdlemg10  31376  cdlemg11b  31377  cdlemg12f  31383  cdlemg17a  31396  cdlemg17dALTN  31399  cdlemg19a  31418  cdlemg35  31448  trlcoabs2N  31457  trlcolem  31461  cdlemh2  31551  cdlemi1  31553  cdlemk3  31568  cdlemk4  31569  cdlemk9  31574  cdlemk9bN  31575  cdlemk10  31578  cdlemk39  31651  dia0eldmN  31776  dia1eldmN  31777  dia0  31788  dia1N  31789  diaglbN  31791  diaintclN  31794  dia2dimlem1  31800  dia2dimlem2  31801  dia2dimlem3  31802  dia2dimlem10  31809  dia2dimlem12  31811  cdlemm10N  31854  docaclN  31860  doca2N  31862  djajN  31873  dib0  31900  dibglbN  31902  dibintclN  31903  cdlemn2  31931  cdlemn10  31942  dihjustlem  31952  dihord1  31954  dihord2a  31955  dihord2b  31956  dihord2cN  31957  dihord11b  31958  dihord11c  31960  dihord2pre  31961  dihord2pre2  31962  dihlsscpre  31970  dib2dim  31979  dih2dimb  31980  dih2dimbALTN  31981  dihvalcq2  31983  dihopelvalcpre  31984  dihord6apre  31992  dihord5b  31995  dihord6b  31996  dihord5apre  31998  dih0  32016  dih1  32022  dihwN  32025  dihmeetlem1N  32026  dihglblem5apreN  32027  dihglblem5aN  32028  dihglblem2aN  32029  dihglblem2N  32030  dihglblem3N  32031  dihmeetlem2N  32035  dihglbcpreN  32036  dihmeetbclemN  32040  dihmeetlem3N  32041  dihmeetlem4preN  32042  dihmeetlem6  32045  dihjatc1  32047  dihmeetlem18N  32060  dih1dimatlem  32065  dihjatcclem1  32154  dihjatcclem2  32155  dihjatcclem4  32157
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4323  ax-nul 4331  ax-pow 4370  ax-pr 4396
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2703  df-rex 2704  df-rab 2707  df-v 2951  df-sbc 3155  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-nul 3622  df-if 3733  df-sn 3813  df-pr 3814  df-op 3816  df-uni 4009  df-br 4206  df-opab 4260  df-mpt 4261  df-id 4491  df-xp 4877  df-rel 4878  df-cnv 4879  df-co 4880  df-dm 4881  df-iota 5411  df-fun 5449  df-fv 5455  df-lhyp 30723
  Copyright terms: Public domain W3C validator