Theorem lhpbase 41148

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

Step	Hyp	Ref	Expression
1		n0i 4285	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2765	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6877	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 142	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2760	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2760	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 41146	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 504	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 701	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  Vcvv 3450  ∅c0 4278   class class class wbr 5102  ‘cfv 6538  Basecbs 17392  1.cp1 18601   ⋖ ccvr 40412  LHypclh 41134

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6540  df-fv 6546  df-lhyp 41138

This theorem is used by:  lhplt  41150  lhp2lt  41151  lhpexlt  41152  lhp0lt  41153  lhpexle  41155  lhpexnle  41156  lhpexle1  41158  lhpexle2lem  41159  lhpexle3lem  41161  lhpocnle  41166  lhpocat  41167  lhpjat1  41170  lhpjat2  41171  lhpj1  41172  lhpmcvr  41173  lhpmcvr2  41174  lhpmcvr3  41175  lhpmcvr4N  41176  lhpmcvr5N  41177  lhpmcvr6N  41178  lhpm0atN  41179  lhpmat  41180  lhpmatb  41181  lhp2at0  41182  lhpelim  41187  lhpmod2i2  41188  lhpmod6i1  41189  cdlemb2  41191  lhpat  41193  lhpat3  41196  4atexlemwb  41209  ltrnatb  41287  ltrnel  41289  ltrncnvel  41292  trlval2  41313  trlcl  41314  trljat1  41316  trljat2  41317  trlle  41334  trlval3  41337  cdlemc1  41341  cdlemc2  41342  cdlemc4  41344  cdlemc5  41345  cdlemc6  41346  cdlemd2  41349  cdleme0aa  41360  cdleme0b  41362  cdleme0c  41363  cdleme0cp  41364  cdleme0cq  41365  cdleme0e  41367  cdleme0fN  41368  cdlemeulpq  41370  cdleme01N  41371  cdleme0ex1N  41373  cdleme1b  41376  cdleme1  41377  cdleme2  41378  cdleme3b  41379  cdleme3c  41380  cdleme3g  41384  cdleme3h  41385  cdleme3  41387  cdleme4  41388  cdleme4a  41389  cdleme5  41390  cdleme7aa  41392  cdleme7c  41395  cdleme7d  41396  cdleme7e  41397  cdleme7ga  41398  cdleme7  41399  cdleme8  41400  cdleme9b  41402  cdleme9  41403  cdleme10  41404  cdleme11fN  41414  cdleme11g  41415  cdleme11k  41418  cdleme13  41422  cdleme15b  41425  cdleme15d  41427  cdleme15  41428  cdleme16e  41432  cdleme16f  41433  cdleme22gb  41444  cdlemedb  41447  cdlemednpq  41449  cdleme19b  41454  cdleme19c  41455  cdleme20aN  41459  cdleme20c  41461  cdleme20d  41462  cdleme20e  41463  cdleme20j  41468  cdleme21c  41477  cdleme21ct  41479  cdleme22aa  41489  cdleme22cN  41492  cdleme22d  41493  cdleme22e  41494  cdleme22eALTN  41495  cdleme22f  41496  cdleme22g  41498  cdleme23a  41499  cdleme23b  41500  cdleme23c  41501  cdleme28a  41520  cdleme28b  41521  cdleme29ex  41524  cdleme30a  41528  cdlemefr29exN  41552  cdleme32b  41592  cdleme32c  41593  cdleme32e  41595  cdleme35b  41600  cdleme35c  41601  cdleme35d  41602  cdleme35e  41603  cdleme35f  41604  cdleme42a  41621  cdleme42c  41622  cdleme42h  41632  cdleme42i  41633  cdleme48bw  41652  cdlemeg46frv  41675  cdlemeg46vrg  41677  cdlemeg46rgv  41678  cdlemeg46req  41679  cdlemf1  41711  cdlemf2  41712  trlord  41719  cdlemg2fv2  41750  cdlemg2m  41754  cdlemg7fvbwN  41757  cdlemg4  41767  cdlemg6c  41770  cdlemg10bALTN  41786  cdlemg10c  41789  cdlemg10  41791  cdlemg11b  41792  cdlemg12f  41798  cdlemg17a  41811  cdlemg17dALTN  41814  cdlemg19a  41833  cdlemg35  41863  trlcoabs2N  41872  trlcolem  41876  cdlemh2  41966  cdlemi1  41968  cdlemk3  41983  cdlemk4  41984  cdlemk9  41989  cdlemk9bN  41990  cdlemk10  41993  cdlemk39  42066  dia0eldmN  42190  dia1eldmN  42191  dia0  42202  dia1N  42203  diaglbN  42205  diaintclN  42208  dia2dimlem1  42214  dia2dimlem2  42215  dia2dimlem3  42216  dia2dimlem10  42223  dia2dimlem12  42225  cdlemm10N  42268  docaclN  42274  doca2N  42276  djajN  42287  dib0  42314  dibglbN  42316  dibintclN  42317  cdlemn2  42345  cdlemn10  42356  dihjustlem  42366  dihord1  42368  dihord2a  42369  dihord2b  42370  dihord2cN  42371  dihord11b  42372  dihord11c  42374  dihord2pre  42375  dihord2pre2  42376  dihlsscpre  42384  dib2dim  42393  dih2dimb  42394  dih2dimbALTN  42395  dihvalcq2  42397  dihopelvalcpre  42398  dihord6apre  42406  dihord5b  42409  dihord6b  42410  dihord5apre  42412  dih0  42430  dih1  42436  dihwN  42439  dihmeetlem1N  42440  dihglblem5apreN  42441  dihglblem5aN  42442  dihglblem2aN  42443  dihglblem2N  42444  dihglblem3N  42445  dihmeetlem2N  42449  dihglbcpreN  42450  dihmeetbclemN  42454  dihmeetlem3N  42455  dihmeetlem4preN  42456  dihmeetlem6  42459  dihjatc1  42461  dihmeetlem18N  42474  dih1dimatlem  42479  dihjatcclem1  42568  dihjatcclem2  42569  dihjatcclem4  42571