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 37016
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 4298 . . . 4 (𝑊𝐻 → ¬ 𝐻 = ∅)
2 lhpbase.h . . . . 5 𝐻 = (LHyp‘𝐾)
32eqeq1i 2826 . . . 4 (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
41, 3sylnib 329 . . 3 (𝑊𝐻 → ¬ (LHyp‘𝐾) = ∅)
5 fvprc 6657 . . 3 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
64, 5nsyl2 143 . 2 (𝑊𝐻𝐾 ∈ V)
7 lhpbase.b . . . 4 𝐵 = (Base‘𝐾)
8 eqid 2821 . . . 4 (1.‘𝐾) = (1.‘𝐾)
9 eqid 2821 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
107, 8, 9, 2islhp 37014 . . 3 (𝐾 ∈ V → (𝑊𝐻 ↔ (𝑊𝐵𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
1110simprbda 499 . 2 ((𝐾 ∈ V ∧ 𝑊𝐻) → 𝑊𝐵)
126, 11mpancom 684 1 (𝑊𝐻𝑊𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  Vcvv 3495  c0 4290   class class class wbr 5058  cfv 6349  Basecbs 16473  1.cp1 17638  ccvr 36280  LHypclh 37002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-iota 6308  df-fun 6351  df-fv 6357  df-lhyp 37006
This theorem is referenced by:  lhplt  37018  lhp2lt  37019  lhpexlt  37020  lhp0lt  37021  lhpexle  37023  lhpexnle  37024  lhpexle1  37026  lhpexle2lem  37027  lhpexle3lem  37029  lhpocnle  37034  lhpocat  37035  lhpjat1  37038  lhpjat2  37039  lhpj1  37040  lhpmcvr  37041  lhpmcvr2  37042  lhpmcvr3  37043  lhpmcvr4N  37044  lhpmcvr5N  37045  lhpmcvr6N  37046  lhpm0atN  37047  lhpmat  37048  lhpmatb  37049  lhp2at0  37050  lhpelim  37055  lhpmod2i2  37056  lhpmod6i1  37057  cdlemb2  37059  lhpat  37061  lhpat3  37064  4atexlemwb  37077  ltrnatb  37155  ltrnel  37157  ltrncnvel  37160  trlval2  37181  trlcl  37182  trljat1  37184  trljat2  37185  trlle  37202  trlval3  37205  cdlemc1  37209  cdlemc2  37210  cdlemc4  37212  cdlemc5  37213  cdlemc6  37214  cdlemd2  37217  cdleme0aa  37228  cdleme0b  37230  cdleme0c  37231  cdleme0cp  37232  cdleme0cq  37233  cdleme0e  37235  cdleme0fN  37236  cdlemeulpq  37238  cdleme01N  37239  cdleme0ex1N  37241  cdleme1b  37244  cdleme1  37245  cdleme2  37246  cdleme3b  37247  cdleme3c  37248  cdleme3g  37252  cdleme3h  37253  cdleme3  37255  cdleme4  37256  cdleme4a  37257  cdleme5  37258  cdleme7aa  37260  cdleme7c  37263  cdleme7d  37264  cdleme7e  37265  cdleme7ga  37266  cdleme7  37267  cdleme8  37268  cdleme9b  37270  cdleme9  37271  cdleme10  37272  cdleme11fN  37282  cdleme11g  37283  cdleme11k  37286  cdleme13  37290  cdleme15b  37293  cdleme15d  37295  cdleme15  37296  cdleme16e  37300  cdleme16f  37301  cdleme22gb  37312  cdlemedb  37315  cdlemednpq  37317  cdleme19b  37322  cdleme19c  37323  cdleme20aN  37327  cdleme20c  37329  cdleme20d  37330  cdleme20e  37331  cdleme20j  37336  cdleme21c  37345  cdleme21ct  37347  cdleme22aa  37357  cdleme22cN  37360  cdleme22d  37361  cdleme22e  37362  cdleme22eALTN  37363  cdleme22f  37364  cdleme22g  37366  cdleme23a  37367  cdleme23b  37368  cdleme23c  37369  cdleme28a  37388  cdleme28b  37389  cdleme29ex  37392  cdleme30a  37396  cdlemefr29exN  37420  cdleme32b  37460  cdleme32c  37461  cdleme32e  37463  cdleme35b  37468  cdleme35c  37469  cdleme35d  37470  cdleme35e  37471  cdleme35f  37472  cdleme42a  37489  cdleme42c  37490  cdleme42h  37500  cdleme42i  37501  cdleme48bw  37520  cdlemeg46frv  37543  cdlemeg46vrg  37545  cdlemeg46rgv  37546  cdlemeg46req  37547  cdlemf1  37579  cdlemf2  37580  trlord  37587  cdlemg2fv2  37618  cdlemg2m  37622  cdlemg7fvbwN  37625  cdlemg4  37635  cdlemg6c  37638  cdlemg10bALTN  37654  cdlemg10c  37657  cdlemg10  37659  cdlemg11b  37660  cdlemg12f  37666  cdlemg17a  37679  cdlemg17dALTN  37682  cdlemg19a  37701  cdlemg35  37731  trlcoabs2N  37740  trlcolem  37744  cdlemh2  37834  cdlemi1  37836  cdlemk3  37851  cdlemk4  37852  cdlemk9  37857  cdlemk9bN  37858  cdlemk10  37861  cdlemk39  37934  dia0eldmN  38058  dia1eldmN  38059  dia0  38070  dia1N  38071  diaglbN  38073  diaintclN  38076  dia2dimlem1  38082  dia2dimlem2  38083  dia2dimlem3  38084  dia2dimlem10  38091  dia2dimlem12  38093  cdlemm10N  38136  docaclN  38142  doca2N  38144  djajN  38155  dib0  38182  dibglbN  38184  dibintclN  38185  cdlemn2  38213  cdlemn10  38224  dihjustlem  38234  dihord1  38236  dihord2a  38237  dihord2b  38238  dihord2cN  38239  dihord11b  38240  dihord11c  38242  dihord2pre  38243  dihord2pre2  38244  dihlsscpre  38252  dib2dim  38261  dih2dimb  38262  dih2dimbALTN  38263  dihvalcq2  38265  dihopelvalcpre  38266  dihord6apre  38274  dihord5b  38277  dihord6b  38278  dihord5apre  38280  dih0  38298  dih1  38304  dihwN  38307  dihmeetlem1N  38308  dihglblem5apreN  38309  dihglblem5aN  38310  dihglblem2aN  38311  dihglblem2N  38312  dihglblem3N  38313  dihmeetlem2N  38317  dihglbcpreN  38318  dihmeetbclemN  38322  dihmeetlem3N  38323  dihmeetlem4preN  38324  dihmeetlem6  38327  dihjatc1  38329  dihmeetlem18N  38342  dih1dimatlem  38347  dihjatcclem1  38436  dihjatcclem2  38437  dihjatcclem4  38439
  Copyright terms: Public domain W3C validator