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 35602
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 3953 . . . 4 (𝑊𝐻 → ¬ 𝐻 = ∅)
2 lhpbase.h . . . . 5 𝐻 = (LHyp‘𝐾)
32eqeq1i 2656 . . . 4 (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
41, 3sylnib 317 . . 3 (𝑊𝐻 → ¬ (LHyp‘𝐾) = ∅)
5 fvprc 6223 . . 3 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
64, 5nsyl2 142 . 2 (𝑊𝐻𝐾 ∈ V)
7 lhpbase.b . . . 4 𝐵 = (Base‘𝐾)
8 eqid 2651 . . . 4 (1.‘𝐾) = (1.‘𝐾)
9 eqid 2651 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
107, 8, 9, 2islhp 35600 . . 3 (𝐾 ∈ V → (𝑊𝐻 ↔ (𝑊𝐵𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
1110simprbda 652 . 2 ((𝐾 ∈ V ∧ 𝑊𝐻) → 𝑊𝐵)
126, 11mpancom 704 1 (𝑊𝐻𝑊𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  Vcvv 3231  c0 3948   class class class wbr 4685  cfv 5926  Basecbs 15904  1.cp1 17085  ccvr 34867  LHypclh 35588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-iota 5889  df-fun 5928  df-fv 5934  df-lhyp 35592
This theorem is referenced by:  lhplt  35604  lhp2lt  35605  lhpexlt  35606  lhp0lt  35607  lhpexle  35609  lhpexnle  35610  lhpexle1  35612  lhpexle2lem  35613  lhpexle3lem  35615  lhpocnle  35620  lhpocat  35621  lhpjat1  35624  lhpjat2  35625  lhpj1  35626  lhpmcvr  35627  lhpmcvr2  35628  lhpmcvr3  35629  lhpmcvr4N  35630  lhpmcvr5N  35631  lhpmcvr6N  35632  lhpm0atN  35633  lhpmat  35634  lhpmatb  35635  lhp2at0  35636  lhpelim  35641  lhpmod2i2  35642  lhpmod6i1  35643  cdlemb2  35645  lhpat  35647  lhpat3  35650  4atexlemwb  35663  ltrnatb  35741  ltrnel  35743  ltrncnvel  35746  ltrnmwOLD  35756  trlval2  35768  trlcl  35769  trljat1  35771  trljat2  35772  trlle  35789  trlval3  35792  cdlemc1  35796  cdlemc2  35797  cdlemc4  35799  cdlemc5  35800  cdlemc6  35801  cdlemd2  35804  cdleme0aa  35815  cdleme0b  35817  cdleme0c  35818  cdleme0cp  35819  cdleme0cq  35820  cdleme0e  35822  cdleme0fN  35823  cdlemeulpq  35825  cdleme01N  35826  cdleme0ex1N  35828  cdleme1b  35831  cdleme1  35832  cdleme2  35833  cdleme3b  35834  cdleme3c  35835  cdleme3g  35839  cdleme3h  35840  cdleme3  35842  cdleme4  35843  cdleme4a  35844  cdleme5  35845  cdleme7aa  35847  cdleme7c  35850  cdleme7d  35851  cdleme7e  35852  cdleme7ga  35853  cdleme7  35854  cdleme8  35855  cdleme9b  35857  cdleme9  35858  cdleme10  35859  cdleme11fN  35869  cdleme11g  35870  cdleme11k  35873  cdleme13  35877  cdleme15b  35880  cdleme15d  35882  cdleme15  35883  cdleme16e  35887  cdleme16f  35888  cdleme22gb  35899  cdlemedb  35902  cdlemednpq  35904  cdleme19b  35909  cdleme19c  35910  cdleme20aN  35914  cdleme20c  35916  cdleme20d  35917  cdleme20e  35918  cdleme20j  35923  cdleme21c  35932  cdleme21ct  35934  cdleme22aa  35944  cdleme22cN  35947  cdleme22d  35948  cdleme22e  35949  cdleme22eALTN  35950  cdleme22f  35951  cdleme22g  35953  cdleme23a  35954  cdleme23b  35955  cdleme23c  35956  cdleme28a  35975  cdleme28b  35976  cdleme29ex  35979  cdleme30a  35983  cdlemefr29exN  36007  cdleme32b  36047  cdleme32c  36048  cdleme32e  36050  cdleme35b  36055  cdleme35c  36056  cdleme35d  36057  cdleme35e  36058  cdleme35f  36059  cdleme42a  36076  cdleme42c  36077  cdleme42h  36087  cdleme42i  36088  cdleme48bw  36107  cdlemeg46frv  36130  cdlemeg46vrg  36132  cdlemeg46rgv  36133  cdlemeg46req  36134  cdlemf1  36166  cdlemf2  36167  trlord  36174  cdlemg2fv2  36205  cdlemg2m  36209  cdlemg7fvbwN  36212  cdlemg4  36222  cdlemg6c  36225  cdlemg10bALTN  36241  cdlemg10c  36244  cdlemg10  36246  cdlemg11b  36247  cdlemg12f  36253  cdlemg17a  36266  cdlemg17dALTN  36269  cdlemg19a  36288  cdlemg35  36318  trlcoabs2N  36327  trlcolem  36331  cdlemh2  36421  cdlemi1  36423  cdlemk3  36438  cdlemk4  36439  cdlemk9  36444  cdlemk9bN  36445  cdlemk10  36448  cdlemk39  36521  dia0eldmN  36646  dia1eldmN  36647  dia0  36658  dia1N  36659  diaglbN  36661  diaintclN  36664  dia2dimlem1  36670  dia2dimlem2  36671  dia2dimlem3  36672  dia2dimlem10  36679  dia2dimlem12  36681  cdlemm10N  36724  docaclN  36730  doca2N  36732  djajN  36743  dib0  36770  dibglbN  36772  dibintclN  36773  cdlemn2  36801  cdlemn10  36812  dihjustlem  36822  dihord1  36824  dihord2a  36825  dihord2b  36826  dihord2cN  36827  dihord11b  36828  dihord11c  36830  dihord2pre  36831  dihord2pre2  36832  dihlsscpre  36840  dib2dim  36849  dih2dimb  36850  dih2dimbALTN  36851  dihvalcq2  36853  dihopelvalcpre  36854  dihord6apre  36862  dihord5b  36865  dihord6b  36866  dihord5apre  36868  dih0  36886  dih1  36892  dihwN  36895  dihmeetlem1N  36896  dihglblem5apreN  36897  dihglblem5aN  36898  dihglblem2aN  36899  dihglblem2N  36900  dihglblem3N  36901  dihmeetlem2N  36905  dihglbcpreN  36906  dihmeetbclemN  36910  dihmeetlem3N  36911  dihmeetlem4preN  36912  dihmeetlem6  36915  dihjatc1  36917  dihmeetlem18N  36930  dih1dimatlem  36935  dihjatcclem1  37024  dihjatcclem2  37025  dihjatcclem4  37027
  Copyright terms: Public domain W3C validator