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 35103
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 3912 . . . 4 (𝑊𝐻 → ¬ 𝐻 = ∅)
2 lhpbase.h . . . . 5 𝐻 = (LHyp‘𝐾)
32eqeq1i 2625 . . . 4 (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
41, 3sylnib 318 . . 3 (𝑊𝐻 → ¬ (LHyp‘𝐾) = ∅)
5 fvprc 6172 . . 3 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
64, 5nsyl2 142 . 2 (𝑊𝐻𝐾 ∈ V)
7 lhpbase.b . . . 4 𝐵 = (Base‘𝐾)
8 eqid 2620 . . . 4 (1.‘𝐾) = (1.‘𝐾)
9 eqid 2620 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
107, 8, 9, 2islhp 35101 . . 3 (𝐾 ∈ V → (𝑊𝐻 ↔ (𝑊𝐵𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
1110simprbda 652 . 2 ((𝐾 ∈ V ∧ 𝑊𝐻) → 𝑊𝐵)
126, 11mpancom 702 1 (𝑊𝐻𝑊𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wcel 1988  Vcvv 3195  c0 3907   class class class wbr 4644  cfv 5876  Basecbs 15838  1.cp1 17019  ccvr 34368  LHypclh 35089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-iota 5839  df-fun 5878  df-fv 5884  df-lhyp 35093
This theorem is referenced by:  lhplt  35105  lhp2lt  35106  lhpexlt  35107  lhp0lt  35108  lhpexle  35110  lhpexnle  35111  lhpexle1  35113  lhpexle2lem  35114  lhpexle3lem  35116  lhpocnle  35121  lhpocat  35122  lhpjat1  35125  lhpjat2  35126  lhpj1  35127  lhpmcvr  35128  lhpmcvr2  35129  lhpmcvr3  35130  lhpmcvr4N  35131  lhpmcvr5N  35132  lhpmcvr6N  35133  lhpm0atN  35134  lhpmat  35135  lhpmatb  35136  lhp2at0  35137  lhpelim  35142  lhpmod2i2  35143  lhpmod6i1  35144  cdlemb2  35146  lhpat  35148  lhpat3  35151  4atexlemwb  35164  ltrnatb  35242  ltrnel  35244  ltrncnvel  35247  ltrnmwOLD  35257  trlval2  35269  trlcl  35270  trljat1  35272  trljat2  35273  trlle  35290  trlval3  35293  cdlemc1  35297  cdlemc2  35298  cdlemc4  35300  cdlemc5  35301  cdlemc6  35302  cdlemd2  35305  cdleme0aa  35316  cdleme0b  35318  cdleme0c  35319  cdleme0cp  35320  cdleme0cq  35321  cdleme0e  35323  cdleme0fN  35324  cdlemeulpq  35326  cdleme01N  35327  cdleme0ex1N  35329  cdleme1b  35332  cdleme1  35333  cdleme2  35334  cdleme3b  35335  cdleme3c  35336  cdleme3g  35340  cdleme3h  35341  cdleme3  35343  cdleme4  35344  cdleme4a  35345  cdleme5  35346  cdleme7aa  35348  cdleme7c  35351  cdleme7d  35352  cdleme7e  35353  cdleme7ga  35354  cdleme7  35355  cdleme8  35356  cdleme9b  35358  cdleme9  35359  cdleme10  35360  cdleme11fN  35370  cdleme11g  35371  cdleme11k  35374  cdleme13  35378  cdleme15b  35381  cdleme15d  35383  cdleme15  35384  cdleme16e  35388  cdleme16f  35389  cdleme22gb  35400  cdlemedb  35403  cdlemednpq  35405  cdleme19b  35411  cdleme19c  35412  cdleme20aN  35416  cdleme20c  35418  cdleme20d  35419  cdleme20e  35420  cdleme20j  35425  cdleme21c  35434  cdleme21ct  35436  cdleme22aa  35446  cdleme22cN  35449  cdleme22d  35450  cdleme22e  35451  cdleme22eALTN  35452  cdleme22f  35453  cdleme22g  35455  cdleme23a  35456  cdleme23b  35457  cdleme23c  35458  cdleme28a  35477  cdleme28b  35478  cdleme29ex  35481  cdleme30a  35485  cdlemefr29exN  35509  cdleme32b  35549  cdleme32c  35550  cdleme32e  35552  cdleme35b  35557  cdleme35c  35558  cdleme35d  35559  cdleme35e  35560  cdleme35f  35561  cdleme42a  35578  cdleme42c  35579  cdleme42h  35589  cdleme42i  35590  cdleme48bw  35609  cdlemeg46frv  35632  cdlemeg46vrg  35634  cdlemeg46rgv  35635  cdlemeg46req  35636  cdlemf1  35668  cdlemf2  35669  trlord  35676  cdlemg2fv2  35707  cdlemg2m  35711  cdlemg7fvbwN  35714  cdlemg4  35724  cdlemg6c  35727  cdlemg10bALTN  35743  cdlemg10c  35746  cdlemg10  35748  cdlemg11b  35749  cdlemg12f  35755  cdlemg17a  35768  cdlemg17dALTN  35771  cdlemg19a  35790  cdlemg35  35820  trlcoabs2N  35829  trlcolem  35833  cdlemh2  35923  cdlemi1  35925  cdlemk3  35940  cdlemk4  35941  cdlemk9  35946  cdlemk9bN  35947  cdlemk10  35950  cdlemk39  36023  dia0eldmN  36148  dia1eldmN  36149  dia0  36160  dia1N  36161  diaglbN  36163  diaintclN  36166  dia2dimlem1  36172  dia2dimlem2  36173  dia2dimlem3  36174  dia2dimlem10  36181  dia2dimlem12  36183  cdlemm10N  36226  docaclN  36232  doca2N  36234  djajN  36245  dib0  36272  dibglbN  36274  dibintclN  36275  cdlemn2  36303  cdlemn10  36314  dihjustlem  36324  dihord1  36326  dihord2a  36327  dihord2b  36328  dihord2cN  36329  dihord11b  36330  dihord11c  36332  dihord2pre  36333  dihord2pre2  36334  dihlsscpre  36342  dib2dim  36351  dih2dimb  36352  dih2dimbALTN  36353  dihvalcq2  36355  dihopelvalcpre  36356  dihord6apre  36364  dihord5b  36367  dihord6b  36368  dihord5apre  36370  dih0  36388  dih1  36394  dihwN  36397  dihmeetlem1N  36398  dihglblem5apreN  36399  dihglblem5aN  36400  dihglblem2aN  36401  dihglblem2N  36402  dihglblem3N  36403  dihmeetlem2N  36407  dihglbcpreN  36408  dihmeetbclemN  36412  dihmeetlem3N  36413  dihmeetlem4preN  36414  dihmeetlem6  36417  dihjatc1  36419  dihmeetlem18N  36432  dih1dimatlem  36437  dihjatcclem1  36526  dihjatcclem2  36527  dihjatcclem4  36529
  Copyright terms: Public domain W3C validator