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

Theorem lhpbase 37287
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 𝐵 = (Base‘𝐾)
lhpbase.h 𝐻 = (LHyp‘𝐾)
Assertion
Ref Expression
lhpbase (𝑊𝐻𝑊𝐵)

Proof of Theorem lhpbase
StepHypRef Expression
1 n0i 4252 . . . 4 (𝑊𝐻 → ¬ 𝐻 = ∅)
2 lhpbase.h . . . . 5 𝐻 = (LHyp‘𝐾)
32eqeq1i 2806 . . . 4 (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
41, 3sylnib 331 . . 3 (𝑊𝐻 → ¬ (LHyp‘𝐾) = ∅)
5 fvprc 6642 . . 3 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
64, 5nsyl2 143 . 2 (𝑊𝐻𝐾 ∈ V)
7 lhpbase.b . . . 4 𝐵 = (Base‘𝐾)
8 eqid 2801 . . . 4 (1.‘𝐾) = (1.‘𝐾)
9 eqid 2801 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
107, 8, 9, 2islhp 37285 . . 3 (𝐾 ∈ V → (𝑊𝐻 ↔ (𝑊𝐵𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
1110simprbda 502 . 2 ((𝐾 ∈ V ∧ 𝑊𝐻) → 𝑊𝐵)
126, 11mpancom 687 1 (𝑊𝐻𝑊𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2112  Vcvv 3444  c0 4246   class class class wbr 5033  cfv 6328  Basecbs 16478  1.cp1 17643  ccvr 36551  LHypclh 37273
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-iota 6287  df-fun 6330  df-fv 6336  df-lhyp 37277
This theorem is referenced by:  lhplt  37289  lhp2lt  37290  lhpexlt  37291  lhp0lt  37292  lhpexle  37294  lhpexnle  37295  lhpexle1  37297  lhpexle2lem  37298  lhpexle3lem  37300  lhpocnle  37305  lhpocat  37306  lhpjat1  37309  lhpjat2  37310  lhpj1  37311  lhpmcvr  37312  lhpmcvr2  37313  lhpmcvr3  37314  lhpmcvr4N  37315  lhpmcvr5N  37316  lhpmcvr6N  37317  lhpm0atN  37318  lhpmat  37319  lhpmatb  37320  lhp2at0  37321  lhpelim  37326  lhpmod2i2  37327  lhpmod6i1  37328  cdlemb2  37330  lhpat  37332  lhpat3  37335  4atexlemwb  37348  ltrnatb  37426  ltrnel  37428  ltrncnvel  37431  trlval2  37452  trlcl  37453  trljat1  37455  trljat2  37456  trlle  37473  trlval3  37476  cdlemc1  37480  cdlemc2  37481  cdlemc4  37483  cdlemc5  37484  cdlemc6  37485  cdlemd2  37488  cdleme0aa  37499  cdleme0b  37501  cdleme0c  37502  cdleme0cp  37503  cdleme0cq  37504  cdleme0e  37506  cdleme0fN  37507  cdlemeulpq  37509  cdleme01N  37510  cdleme0ex1N  37512  cdleme1b  37515  cdleme1  37516  cdleme2  37517  cdleme3b  37518  cdleme3c  37519  cdleme3g  37523  cdleme3h  37524  cdleme3  37526  cdleme4  37527  cdleme4a  37528  cdleme5  37529  cdleme7aa  37531  cdleme7c  37534  cdleme7d  37535  cdleme7e  37536  cdleme7ga  37537  cdleme7  37538  cdleme8  37539  cdleme9b  37541  cdleme9  37542  cdleme10  37543  cdleme11fN  37553  cdleme11g  37554  cdleme11k  37557  cdleme13  37561  cdleme15b  37564  cdleme15d  37566  cdleme15  37567  cdleme16e  37571  cdleme16f  37572  cdleme22gb  37583  cdlemedb  37586  cdlemednpq  37588  cdleme19b  37593  cdleme19c  37594  cdleme20aN  37598  cdleme20c  37600  cdleme20d  37601  cdleme20e  37602  cdleme20j  37607  cdleme21c  37616  cdleme21ct  37618  cdleme22aa  37628  cdleme22cN  37631  cdleme22d  37632  cdleme22e  37633  cdleme22eALTN  37634  cdleme22f  37635  cdleme22g  37637  cdleme23a  37638  cdleme23b  37639  cdleme23c  37640  cdleme28a  37659  cdleme28b  37660  cdleme29ex  37663  cdleme30a  37667  cdlemefr29exN  37691  cdleme32b  37731  cdleme32c  37732  cdleme32e  37734  cdleme35b  37739  cdleme35c  37740  cdleme35d  37741  cdleme35e  37742  cdleme35f  37743  cdleme42a  37760  cdleme42c  37761  cdleme42h  37771  cdleme42i  37772  cdleme48bw  37791  cdlemeg46frv  37814  cdlemeg46vrg  37816  cdlemeg46rgv  37817  cdlemeg46req  37818  cdlemf1  37850  cdlemf2  37851  trlord  37858  cdlemg2fv2  37889  cdlemg2m  37893  cdlemg7fvbwN  37896  cdlemg4  37906  cdlemg6c  37909  cdlemg10bALTN  37925  cdlemg10c  37928  cdlemg10  37930  cdlemg11b  37931  cdlemg12f  37937  cdlemg17a  37950  cdlemg17dALTN  37953  cdlemg19a  37972  cdlemg35  38002  trlcoabs2N  38011  trlcolem  38015  cdlemh2  38105  cdlemi1  38107  cdlemk3  38122  cdlemk4  38123  cdlemk9  38128  cdlemk9bN  38129  cdlemk10  38132  cdlemk39  38205  dia0eldmN  38329  dia1eldmN  38330  dia0  38341  dia1N  38342  diaglbN  38344  diaintclN  38347  dia2dimlem1  38353  dia2dimlem2  38354  dia2dimlem3  38355  dia2dimlem10  38362  dia2dimlem12  38364  cdlemm10N  38407  docaclN  38413  doca2N  38415  djajN  38426  dib0  38453  dibglbN  38455  dibintclN  38456  cdlemn2  38484  cdlemn10  38495  dihjustlem  38505  dihord1  38507  dihord2a  38508  dihord2b  38509  dihord2cN  38510  dihord11b  38511  dihord11c  38513  dihord2pre  38514  dihord2pre2  38515  dihlsscpre  38523  dib2dim  38532  dih2dimb  38533  dih2dimbALTN  38534  dihvalcq2  38536  dihopelvalcpre  38537  dihord6apre  38545  dihord5b  38548  dihord6b  38549  dihord5apre  38551  dih0  38569  dih1  38575  dihwN  38578  dihmeetlem1N  38579  dihglblem5apreN  38580  dihglblem5aN  38581  dihglblem2aN  38582  dihglblem2N  38583  dihglblem3N  38584  dihmeetlem2N  38588  dihglbcpreN  38589  dihmeetbclemN  38593  dihmeetlem3N  38594  dihmeetlem4preN  38595  dihmeetlem6  38598  dihjatc1  38600  dihmeetlem18N  38613  dih1dimatlem  38618  dihjatcclem1  38707  dihjatcclem2  38708  dihjatcclem4  38710
  Copyright terms: Public domain W3C validator