Theorem lhpbase 38012

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 4267	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2743	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 328	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6766	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 141	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2738	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2738	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 38010	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 499	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 685	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  Vcvv 3432  ∅c0 4256   class class class wbr 5074  ‘cfv 6433  Basecbs 16912  1.cp1 18142   ⋖ ccvr 37276  LHypclh 37998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441  df-lhyp 38002

This theorem is referenced by:  lhplt  38014  lhp2lt  38015  lhpexlt  38016  lhp0lt  38017  lhpexle  38019  lhpexnle  38020  lhpexle1  38022  lhpexle2lem  38023  lhpexle3lem  38025  lhpocnle  38030  lhpocat  38031  lhpjat1  38034  lhpjat2  38035  lhpj1  38036  lhpmcvr  38037  lhpmcvr2  38038  lhpmcvr3  38039  lhpmcvr4N  38040  lhpmcvr5N  38041  lhpmcvr6N  38042  lhpm0atN  38043  lhpmat  38044  lhpmatb  38045  lhp2at0  38046  lhpelim  38051  lhpmod2i2  38052  lhpmod6i1  38053  cdlemb2  38055  lhpat  38057  lhpat3  38060  4atexlemwb  38073  ltrnatb  38151  ltrnel  38153  ltrncnvel  38156  trlval2  38177  trlcl  38178  trljat1  38180  trljat2  38181  trlle  38198  trlval3  38201  cdlemc1  38205  cdlemc2  38206  cdlemc4  38208  cdlemc5  38209  cdlemc6  38210  cdlemd2  38213  cdleme0aa  38224  cdleme0b  38226  cdleme0c  38227  cdleme0cp  38228  cdleme0cq  38229  cdleme0e  38231  cdleme0fN  38232  cdlemeulpq  38234  cdleme01N  38235  cdleme0ex1N  38237  cdleme1b  38240  cdleme1  38241  cdleme2  38242  cdleme3b  38243  cdleme3c  38244  cdleme3g  38248  cdleme3h  38249  cdleme3  38251  cdleme4  38252  cdleme4a  38253  cdleme5  38254  cdleme7aa  38256  cdleme7c  38259  cdleme7d  38260  cdleme7e  38261  cdleme7ga  38262  cdleme7  38263  cdleme8  38264  cdleme9b  38266  cdleme9  38267  cdleme10  38268  cdleme11fN  38278  cdleme11g  38279  cdleme11k  38282  cdleme13  38286  cdleme15b  38289  cdleme15d  38291  cdleme15  38292  cdleme16e  38296  cdleme16f  38297  cdleme22gb  38308  cdlemedb  38311  cdlemednpq  38313  cdleme19b  38318  cdleme19c  38319  cdleme20aN  38323  cdleme20c  38325  cdleme20d  38326  cdleme20e  38327  cdleme20j  38332  cdleme21c  38341  cdleme21ct  38343  cdleme22aa  38353  cdleme22cN  38356  cdleme22d  38357  cdleme22e  38358  cdleme22eALTN  38359  cdleme22f  38360  cdleme22g  38362  cdleme23a  38363  cdleme23b  38364  cdleme23c  38365  cdleme28a  38384  cdleme28b  38385  cdleme29ex  38388  cdleme30a  38392  cdlemefr29exN  38416  cdleme32b  38456  cdleme32c  38457  cdleme32e  38459  cdleme35b  38464  cdleme35c  38465  cdleme35d  38466  cdleme35e  38467  cdleme35f  38468  cdleme42a  38485  cdleme42c  38486  cdleme42h  38496  cdleme42i  38497  cdleme48bw  38516  cdlemeg46frv  38539  cdlemeg46vrg  38541  cdlemeg46rgv  38542  cdlemeg46req  38543  cdlemf1  38575  cdlemf2  38576  trlord  38583  cdlemg2fv2  38614  cdlemg2m  38618  cdlemg7fvbwN  38621  cdlemg4  38631  cdlemg6c  38634  cdlemg10bALTN  38650  cdlemg10c  38653  cdlemg10  38655  cdlemg11b  38656  cdlemg12f  38662  cdlemg17a  38675  cdlemg17dALTN  38678  cdlemg19a  38697  cdlemg35  38727  trlcoabs2N  38736  trlcolem  38740  cdlemh2  38830  cdlemi1  38832  cdlemk3  38847  cdlemk4  38848  cdlemk9  38853  cdlemk9bN  38854  cdlemk10  38857  cdlemk39  38930  dia0eldmN  39054  dia1eldmN  39055  dia0  39066  dia1N  39067  diaglbN  39069  diaintclN  39072  dia2dimlem1  39078  dia2dimlem2  39079  dia2dimlem3  39080  dia2dimlem10  39087  dia2dimlem12  39089  cdlemm10N  39132  docaclN  39138  doca2N  39140  djajN  39151  dib0  39178  dibglbN  39180  dibintclN  39181  cdlemn2  39209  cdlemn10  39220  dihjustlem  39230  dihord1  39232  dihord2a  39233  dihord2b  39234  dihord2cN  39235  dihord11b  39236  dihord11c  39238  dihord2pre  39239  dihord2pre2  39240  dihlsscpre  39248  dib2dim  39257  dih2dimb  39258  dih2dimbALTN  39259  dihvalcq2  39261  dihopelvalcpre  39262  dihord6apre  39270  dihord5b  39273  dihord6b  39274  dihord5apre  39276  dih0  39294  dih1  39300  dihwN  39303  dihmeetlem1N  39304  dihglblem5apreN  39305  dihglblem5aN  39306  dihglblem2aN  39307  dihglblem2N  39308  dihglblem3N  39309  dihmeetlem2N  39313  dihglbcpreN  39314  dihmeetbclemN  39318  dihmeetlem3N  39319  dihmeetlem4preN  39320  dihmeetlem6  39323  dihjatc1  39325  dihmeetlem18N  39338  dih1dimatlem  39343  dihjatcclem1  39432  dihjatcclem2  39433  dihjatcclem4  39435