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 35799
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 4066 . . . 4 (𝑊𝐻 → ¬ 𝐻 = ∅)
2 lhpbase.h . . . . 5 𝐻 = (LHyp‘𝐾)
32eqeq1i 2775 . . . 4 (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
41, 3sylnib 317 . . 3 (𝑊𝐻 → ¬ (LHyp‘𝐾) = ∅)
5 fvprc 6326 . . 3 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
64, 5nsyl2 144 . 2 (𝑊𝐻𝐾 ∈ V)
7 lhpbase.b . . . 4 𝐵 = (Base‘𝐾)
8 eqid 2770 . . . 4 (1.‘𝐾) = (1.‘𝐾)
9 eqid 2770 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
107, 8, 9, 2islhp 35797 . . 3 (𝐾 ∈ V → (𝑊𝐻 ↔ (𝑊𝐵𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
1110simprbda 480 . 2 ((𝐾 ∈ V ∧ 𝑊𝐻) → 𝑊𝐵)
126, 11mpancom 660 1 (𝑊𝐻𝑊𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630  wcel 2144  Vcvv 3349  c0 4061   class class class wbr 4784  cfv 6031  Basecbs 16063  1.cp1 17245  ccvr 35064  LHypclh 35785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-opab 4845  df-mpt 4862  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-iota 5994  df-fun 6033  df-fv 6039  df-lhyp 35789
This theorem is referenced by:  lhplt  35801  lhp2lt  35802  lhpexlt  35803  lhp0lt  35804  lhpexle  35806  lhpexnle  35807  lhpexle1  35809  lhpexle2lem  35810  lhpexle3lem  35812  lhpocnle  35817  lhpocat  35818  lhpjat1  35821  lhpjat2  35822  lhpj1  35823  lhpmcvr  35824  lhpmcvr2  35825  lhpmcvr3  35826  lhpmcvr4N  35827  lhpmcvr5N  35828  lhpmcvr6N  35829  lhpm0atN  35830  lhpmat  35831  lhpmatb  35832  lhp2at0  35833  lhpelim  35838  lhpmod2i2  35839  lhpmod6i1  35840  cdlemb2  35842  lhpat  35844  lhpat3  35847  4atexlemwb  35860  ltrnatb  35938  ltrnel  35940  ltrncnvel  35943  ltrnmwOLD  35953  trlval2  35965  trlcl  35966  trljat1  35968  trljat2  35969  trlle  35986  trlval3  35989  cdlemc1  35993  cdlemc2  35994  cdlemc4  35996  cdlemc5  35997  cdlemc6  35998  cdlemd2  36001  cdleme0aa  36012  cdleme0b  36014  cdleme0c  36015  cdleme0cp  36016  cdleme0cq  36017  cdleme0e  36019  cdleme0fN  36020  cdlemeulpq  36022  cdleme01N  36023  cdleme0ex1N  36025  cdleme1b  36028  cdleme1  36029  cdleme2  36030  cdleme3b  36031  cdleme3c  36032  cdleme3g  36036  cdleme3h  36037  cdleme3  36039  cdleme4  36040  cdleme4a  36041  cdleme5  36042  cdleme7aa  36044  cdleme7c  36047  cdleme7d  36048  cdleme7e  36049  cdleme7ga  36050  cdleme7  36051  cdleme8  36052  cdleme9b  36054  cdleme9  36055  cdleme10  36056  cdleme11fN  36066  cdleme11g  36067  cdleme11k  36070  cdleme13  36074  cdleme15b  36077  cdleme15d  36079  cdleme15  36080  cdleme16e  36084  cdleme16f  36085  cdleme22gb  36096  cdlemedb  36099  cdlemednpq  36101  cdleme19b  36106  cdleme19c  36107  cdleme20aN  36111  cdleme20c  36113  cdleme20d  36114  cdleme20e  36115  cdleme20j  36120  cdleme21c  36129  cdleme21ct  36131  cdleme22aa  36141  cdleme22cN  36144  cdleme22d  36145  cdleme22e  36146  cdleme22eALTN  36147  cdleme22f  36148  cdleme22g  36150  cdleme23a  36151  cdleme23b  36152  cdleme23c  36153  cdleme28a  36172  cdleme28b  36173  cdleme29ex  36176  cdleme30a  36180  cdlemefr29exN  36204  cdleme32b  36244  cdleme32c  36245  cdleme32e  36247  cdleme35b  36252  cdleme35c  36253  cdleme35d  36254  cdleme35e  36255  cdleme35f  36256  cdleme42a  36273  cdleme42c  36274  cdleme42h  36284  cdleme42i  36285  cdleme48bw  36304  cdlemeg46frv  36327  cdlemeg46vrg  36329  cdlemeg46rgv  36330  cdlemeg46req  36331  cdlemf1  36363  cdlemf2  36364  trlord  36371  cdlemg2fv2  36402  cdlemg2m  36406  cdlemg7fvbwN  36409  cdlemg4  36419  cdlemg6c  36422  cdlemg10bALTN  36438  cdlemg10c  36441  cdlemg10  36443  cdlemg11b  36444  cdlemg12f  36450  cdlemg17a  36463  cdlemg17dALTN  36466  cdlemg19a  36485  cdlemg35  36515  trlcoabs2N  36524  trlcolem  36528  cdlemh2  36618  cdlemi1  36620  cdlemk3  36635  cdlemk4  36636  cdlemk9  36641  cdlemk9bN  36642  cdlemk10  36645  cdlemk39  36718  dia0eldmN  36843  dia1eldmN  36844  dia0  36855  dia1N  36856  diaglbN  36858  diaintclN  36861  dia2dimlem1  36867  dia2dimlem2  36868  dia2dimlem3  36869  dia2dimlem10  36876  dia2dimlem12  36878  cdlemm10N  36921  docaclN  36927  doca2N  36929  djajN  36940  dib0  36967  dibglbN  36969  dibintclN  36970  cdlemn2  36998  cdlemn10  37009  dihjustlem  37019  dihord1  37021  dihord2a  37022  dihord2b  37023  dihord2cN  37024  dihord11b  37025  dihord11c  37027  dihord2pre  37028  dihord2pre2  37029  dihlsscpre  37037  dib2dim  37046  dih2dimb  37047  dih2dimbALTN  37048  dihvalcq2  37050  dihopelvalcpre  37051  dihord6apre  37059  dihord5b  37062  dihord6b  37063  dihord5apre  37065  dih0  37083  dih1  37089  dihwN  37092  dihmeetlem1N  37093  dihglblem5apreN  37094  dihglblem5aN  37095  dihglblem2aN  37096  dihglblem2N  37097  dihglblem3N  37098  dihmeetlem2N  37102  dihglbcpreN  37103  dihmeetbclemN  37107  dihmeetlem3N  37108  dihmeetlem4preN  37109  dihmeetlem6  37112  dihjatc1  37114  dihmeetlem18N  37127  dih1dimatlem  37132  dihjatcclem1  37221  dihjatcclem2  37222  dihjatcclem4  37224
  Copyright terms: Public domain W3C validator