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

Theorem lhpbase 30732
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 3625 . . . 4  |-  ( W  e.  H  ->  -.  H  =  (/) )
2 lhpbase.h . . . . 5  |-  H  =  ( LHyp `  K
)
32eqeq1i 2442 . . . 4  |-  ( H  =  (/)  <->  ( LHyp `  K
)  =  (/) )
41, 3sylnib 296 . . 3  |-  ( W  e.  H  ->  -.  ( LHyp `  K )  =  (/) )
5 fvprc 5714 . . 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 2435 . . . 4  |-  ( 1.
`  K )  =  ( 1. `  K
)
9 eqid 2435 . . . 4  |-  (  <o  `  K )  =  ( 
<o  `  K )
107, 8, 9, 2islhp 30730 . . 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 2948   (/)c0 3620   class class class wbr 4204   ` cfv 5446   Basecbs 13461   1.cp1 14459    <o ccvr 29997   LHypclh 30718
This theorem is referenced by:  lhplt  30734  lhp2lt  30735  lhpexlt  30736  lhp0lt  30737  lhpexle  30739  lhpexnle  30740  lhpexle1  30742  lhpexle2lem  30743  lhpexle3lem  30745  lhpocnle  30750  lhpocat  30751  lhpjat1  30754  lhpjat2  30755  lhpj1  30756  lhpmcvr  30757  lhpmcvr2  30758  lhpmcvr3  30759  lhpmcvr4N  30760  lhpmcvr5N  30761  lhpmcvr6N  30762  lhpm0atN  30763  lhpmat  30764  lhpmatb  30765  lhp2at0  30766  lhpelim  30771  lhpmod2i2  30772  lhpmod6i1  30773  cdlemb2  30775  lhpat  30777  lhpat3  30780  4atexlemwb  30793  ltrnatb  30871  ltrnel  30873  ltrncnvel  30876  ltrnmw  30885  trlval2  30897  trlcl  30898  trljat1  30900  trljat2  30901  trlle  30918  trlval3  30921  cdlemc1  30925  cdlemc2  30926  cdlemc4  30928  cdlemc5  30929  cdlemc6  30930  cdlemd2  30933  cdleme0aa  30944  cdleme0b  30946  cdleme0c  30947  cdleme0cp  30948  cdleme0cq  30949  cdleme0e  30951  cdleme0fN  30952  cdlemeulpq  30954  cdleme01N  30955  cdleme0ex1N  30957  cdleme1b  30960  cdleme1  30961  cdleme2  30962  cdleme3b  30963  cdleme3c  30964  cdleme3g  30968  cdleme3h  30969  cdleme3  30971  cdleme4  30972  cdleme4a  30973  cdleme5  30974  cdleme7aa  30976  cdleme7c  30979  cdleme7d  30980  cdleme7e  30981  cdleme7ga  30982  cdleme7  30983  cdleme8  30984  cdleme9b  30986  cdleme9  30987  cdleme10  30988  cdleme11fN  30998  cdleme11g  30999  cdleme11k  31002  cdleme13  31006  cdleme15b  31009  cdleme15d  31011  cdleme15  31012  cdleme16e  31016  cdleme16f  31017  cdleme22gb  31028  cdlemedb  31031  cdlemednpq  31033  cdleme19b  31038  cdleme19c  31039  cdleme20aN  31043  cdleme20c  31045  cdleme20d  31046  cdleme20e  31047  cdleme20j  31052  cdleme21c  31061  cdleme21ct  31063  cdleme22aa  31073  cdleme22cN  31076  cdleme22d  31077  cdleme22e  31078  cdleme22eALTN  31079  cdleme22f  31080  cdleme22g  31082  cdleme23a  31083  cdleme23b  31084  cdleme23c  31085  cdleme28a  31104  cdleme28b  31105  cdleme29ex  31108  cdleme30a  31112  cdlemefr29exN  31136  cdleme32b  31176  cdleme32c  31177  cdleme32e  31179  cdleme35b  31184  cdleme35c  31185  cdleme35d  31186  cdleme35e  31187  cdleme35f  31188  cdleme42a  31205  cdleme42c  31206  cdleme42h  31216  cdleme42i  31217  cdleme48bw  31236  cdlemeg46frv  31259  cdlemeg46vrg  31261  cdlemeg46rgv  31262  cdlemeg46req  31263  cdlemf1  31295  cdlemf2  31296  trlord  31303  cdlemg2fv2  31334  cdlemg2m  31338  cdlemg7fvbwN  31341  cdlemg4  31351  cdlemg6c  31354  cdlemg10bALTN  31370  cdlemg10c  31373  cdlemg10  31375  cdlemg11b  31376  cdlemg12f  31382  cdlemg17a  31395  cdlemg17dALTN  31398  cdlemg19a  31417  cdlemg35  31447  trlcoabs2N  31456  trlcolem  31460  cdlemh2  31550  cdlemi1  31552  cdlemk3  31567  cdlemk4  31568  cdlemk9  31573  cdlemk9bN  31574  cdlemk10  31577  cdlemk39  31650  dia0eldmN  31775  dia1eldmN  31776  dia0  31787  dia1N  31788  diaglbN  31790  diaintclN  31793  dia2dimlem1  31799  dia2dimlem2  31800  dia2dimlem3  31801  dia2dimlem10  31808  dia2dimlem12  31810  cdlemm10N  31853  docaclN  31859  doca2N  31861  djajN  31872  dib0  31899  dibglbN  31901  dibintclN  31902  cdlemn2  31930  cdlemn10  31941  dihjustlem  31951  dihord1  31953  dihord2a  31954  dihord2b  31955  dihord2cN  31956  dihord11b  31957  dihord11c  31959  dihord2pre  31960  dihord2pre2  31961  dihlsscpre  31969  dib2dim  31978  dih2dimb  31979  dih2dimbALTN  31980  dihvalcq2  31982  dihopelvalcpre  31983  dihord6apre  31991  dihord5b  31994  dihord6b  31995  dihord5apre  31997  dih0  32015  dih1  32021  dihwN  32024  dihmeetlem1N  32025  dihglblem5apreN  32026  dihglblem5aN  32027  dihglblem2aN  32028  dihglblem2N  32029  dihglblem3N  32030  dihmeetlem2N  32034  dihglbcpreN  32035  dihmeetbclemN  32039  dihmeetlem3N  32040  dihmeetlem4preN  32041  dihmeetlem6  32044  dihjatc1  32046  dihmeetlem18N  32059  dih1dimatlem  32064  dihjatcclem1  32153  dihjatcclem2  32154  dihjatcclem4  32156
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 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395
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 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-iota 5410  df-fun 5448  df-fv 5454  df-lhyp 30722
  Copyright terms: Public domain W3C validator