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 35797
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 4132 . . . 4 (𝑊𝐻 → ¬ 𝐻 = ∅)
2 lhpbase.h . . . . 5 𝐻 = (LHyp‘𝐾)
32eqeq1i 2822 . . . 4 (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
41, 3sylnib 319 . . 3 (𝑊𝐻 → ¬ (LHyp‘𝐾) = ∅)
5 fvprc 6411 . . 3 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
64, 5nsyl2 144 . 2 (𝑊𝐻𝐾 ∈ V)
7 lhpbase.b . . . 4 𝐵 = (Base‘𝐾)
8 eqid 2817 . . . 4 (1.‘𝐾) = (1.‘𝐾)
9 eqid 2817 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
107, 8, 9, 2islhp 35795 . . 3 (𝐾 ∈ V → (𝑊𝐻 ↔ (𝑊𝐵𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
1110simprbda 488 . 2 ((𝐾 ∈ V ∧ 𝑊𝐻) → 𝑊𝐵)
126, 11mpancom 671 1 (𝑊𝐻𝑊𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2157  Vcvv 3402  c0 4127   class class class wbr 4855  cfv 6111  Basecbs 16088  1.cp1 17263  ccvr 35061  LHypclh 35783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-sbc 3645  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-opab 4918  df-mpt 4935  df-id 5232  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-iota 6074  df-fun 6113  df-fv 6119  df-lhyp 35787
This theorem is referenced by:  lhplt  35799  lhp2lt  35800  lhpexlt  35801  lhp0lt  35802  lhpexle  35804  lhpexnle  35805  lhpexle1  35807  lhpexle2lem  35808  lhpexle3lem  35810  lhpocnle  35815  lhpocat  35816  lhpjat1  35819  lhpjat2  35820  lhpj1  35821  lhpmcvr  35822  lhpmcvr2  35823  lhpmcvr3  35824  lhpmcvr4N  35825  lhpmcvr5N  35826  lhpmcvr6N  35827  lhpm0atN  35828  lhpmat  35829  lhpmatb  35830  lhp2at0  35831  lhpelim  35836  lhpmod2i2  35837  lhpmod6i1  35838  cdlemb2  35840  lhpat  35842  lhpat3  35845  4atexlemwb  35858  ltrnatb  35936  ltrnel  35938  ltrncnvel  35941  trlval2  35962  trlcl  35963  trljat1  35965  trljat2  35966  trlle  35983  trlval3  35986  cdlemc1  35990  cdlemc2  35991  cdlemc4  35993  cdlemc5  35994  cdlemc6  35995  cdlemd2  35998  cdleme0aa  36009  cdleme0b  36011  cdleme0c  36012  cdleme0cp  36013  cdleme0cq  36014  cdleme0e  36016  cdleme0fN  36017  cdlemeulpq  36019  cdleme01N  36020  cdleme0ex1N  36022  cdleme1b  36025  cdleme1  36026  cdleme2  36027  cdleme3b  36028  cdleme3c  36029  cdleme3g  36033  cdleme3h  36034  cdleme3  36036  cdleme4  36037  cdleme4a  36038  cdleme5  36039  cdleme7aa  36041  cdleme7c  36044  cdleme7d  36045  cdleme7e  36046  cdleme7ga  36047  cdleme7  36048  cdleme8  36049  cdleme9b  36051  cdleme9  36052  cdleme10  36053  cdleme11fN  36063  cdleme11g  36064  cdleme11k  36067  cdleme13  36071  cdleme15b  36074  cdleme15d  36076  cdleme15  36077  cdleme16e  36081  cdleme16f  36082  cdleme22gb  36093  cdlemedb  36096  cdlemednpq  36098  cdleme19b  36103  cdleme19c  36104  cdleme20aN  36108  cdleme20c  36110  cdleme20d  36111  cdleme20e  36112  cdleme20j  36117  cdleme21c  36126  cdleme21ct  36128  cdleme22aa  36138  cdleme22cN  36141  cdleme22d  36142  cdleme22e  36143  cdleme22eALTN  36144  cdleme22f  36145  cdleme22g  36147  cdleme23a  36148  cdleme23b  36149  cdleme23c  36150  cdleme28a  36169  cdleme28b  36170  cdleme29ex  36173  cdleme30a  36177  cdlemefr29exN  36201  cdleme32b  36241  cdleme32c  36242  cdleme32e  36244  cdleme35b  36249  cdleme35c  36250  cdleme35d  36251  cdleme35e  36252  cdleme35f  36253  cdleme42a  36270  cdleme42c  36271  cdleme42h  36281  cdleme42i  36282  cdleme48bw  36301  cdlemeg46frv  36324  cdlemeg46vrg  36326  cdlemeg46rgv  36327  cdlemeg46req  36328  cdlemf1  36360  cdlemf2  36361  trlord  36368  cdlemg2fv2  36399  cdlemg2m  36403  cdlemg7fvbwN  36406  cdlemg4  36416  cdlemg6c  36419  cdlemg10bALTN  36435  cdlemg10c  36438  cdlemg10  36440  cdlemg11b  36441  cdlemg12f  36447  cdlemg17a  36460  cdlemg17dALTN  36463  cdlemg19a  36482  cdlemg35  36512  trlcoabs2N  36521  trlcolem  36525  cdlemh2  36615  cdlemi1  36617  cdlemk3  36632  cdlemk4  36633  cdlemk9  36638  cdlemk9bN  36639  cdlemk10  36642  cdlemk39  36715  dia0eldmN  36839  dia1eldmN  36840  dia0  36851  dia1N  36852  diaglbN  36854  diaintclN  36857  dia2dimlem1  36863  dia2dimlem2  36864  dia2dimlem3  36865  dia2dimlem10  36872  dia2dimlem12  36874  cdlemm10N  36917  docaclN  36923  doca2N  36925  djajN  36936  dib0  36963  dibglbN  36965  dibintclN  36966  cdlemn2  36994  cdlemn10  37005  dihjustlem  37015  dihord1  37017  dihord2a  37018  dihord2b  37019  dihord2cN  37020  dihord11b  37021  dihord11c  37023  dihord2pre  37024  dihord2pre2  37025  dihlsscpre  37033  dib2dim  37042  dih2dimb  37043  dih2dimbALTN  37044  dihvalcq2  37046  dihopelvalcpre  37047  dihord6apre  37055  dihord5b  37058  dihord6b  37059  dihord5apre  37061  dih0  37079  dih1  37085  dihwN  37088  dihmeetlem1N  37089  dihglblem5apreN  37090  dihglblem5aN  37091  dihglblem2aN  37092  dihglblem2N  37093  dihglblem3N  37094  dihmeetlem2N  37098  dihglbcpreN  37099  dihmeetbclemN  37103  dihmeetlem3N  37104  dihmeetlem4preN  37105  dihmeetlem6  37108  dihjatc1  37110  dihmeetlem18N  37123  dih1dimatlem  37128  dihjatcclem1  37217  dihjatcclem2  37218  dihjatcclem4  37220
  Copyright terms: Public domain W3C validator