Theorem lhpbase 38857

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 4332	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2737	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 327	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6880	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 141	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2732	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2732	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 38855	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 499	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 686	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3474  ∅c0 4321   class class class wbr 5147  ‘cfv 6540  Basecbs 17140  1.cp1 18373   ⋖ ccvr 38120  LHypclh 38843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6492  df-fun 6542  df-fv 6548  df-lhyp 38847

This theorem is referenced by:  lhplt  38859  lhp2lt  38860  lhpexlt  38861  lhp0lt  38862  lhpexle  38864  lhpexnle  38865  lhpexle1  38867  lhpexle2lem  38868  lhpexle3lem  38870  lhpocnle  38875  lhpocat  38876  lhpjat1  38879  lhpjat2  38880  lhpj1  38881  lhpmcvr  38882  lhpmcvr2  38883  lhpmcvr3  38884  lhpmcvr4N  38885  lhpmcvr5N  38886  lhpmcvr6N  38887  lhpm0atN  38888  lhpmat  38889  lhpmatb  38890  lhp2at0  38891  lhpelim  38896  lhpmod2i2  38897  lhpmod6i1  38898  cdlemb2  38900  lhpat  38902  lhpat3  38905  4atexlemwb  38918  ltrnatb  38996  ltrnel  38998  ltrncnvel  39001  trlval2  39022  trlcl  39023  trljat1  39025  trljat2  39026  trlle  39043  trlval3  39046  cdlemc1  39050  cdlemc2  39051  cdlemc4  39053  cdlemc5  39054  cdlemc6  39055  cdlemd2  39058  cdleme0aa  39069  cdleme0b  39071  cdleme0c  39072  cdleme0cp  39073  cdleme0cq  39074  cdleme0e  39076  cdleme0fN  39077  cdlemeulpq  39079  cdleme01N  39080  cdleme0ex1N  39082  cdleme1b  39085  cdleme1  39086  cdleme2  39087  cdleme3b  39088  cdleme3c  39089  cdleme3g  39093  cdleme3h  39094  cdleme3  39096  cdleme4  39097  cdleme4a  39098  cdleme5  39099  cdleme7aa  39101  cdleme7c  39104  cdleme7d  39105  cdleme7e  39106  cdleme7ga  39107  cdleme7  39108  cdleme8  39109  cdleme9b  39111  cdleme9  39112  cdleme10  39113  cdleme11fN  39123  cdleme11g  39124  cdleme11k  39127  cdleme13  39131  cdleme15b  39134  cdleme15d  39136  cdleme15  39137  cdleme16e  39141  cdleme16f  39142  cdleme22gb  39153  cdlemedb  39156  cdlemednpq  39158  cdleme19b  39163  cdleme19c  39164  cdleme20aN  39168  cdleme20c  39170  cdleme20d  39171  cdleme20e  39172  cdleme20j  39177  cdleme21c  39186  cdleme21ct  39188  cdleme22aa  39198  cdleme22cN  39201  cdleme22d  39202  cdleme22e  39203  cdleme22eALTN  39204  cdleme22f  39205  cdleme22g  39207  cdleme23a  39208  cdleme23b  39209  cdleme23c  39210  cdleme28a  39229  cdleme28b  39230  cdleme29ex  39233  cdleme30a  39237  cdlemefr29exN  39261  cdleme32b  39301  cdleme32c  39302  cdleme32e  39304  cdleme35b  39309  cdleme35c  39310  cdleme35d  39311  cdleme35e  39312  cdleme35f  39313  cdleme42a  39330  cdleme42c  39331  cdleme42h  39341  cdleme42i  39342  cdleme48bw  39361  cdlemeg46frv  39384  cdlemeg46vrg  39386  cdlemeg46rgv  39387  cdlemeg46req  39388  cdlemf1  39420  cdlemf2  39421  trlord  39428  cdlemg2fv2  39459  cdlemg2m  39463  cdlemg7fvbwN  39466  cdlemg4  39476  cdlemg6c  39479  cdlemg10bALTN  39495  cdlemg10c  39498  cdlemg10  39500  cdlemg11b  39501  cdlemg12f  39507  cdlemg17a  39520  cdlemg17dALTN  39523  cdlemg19a  39542  cdlemg35  39572  trlcoabs2N  39581  trlcolem  39585  cdlemh2  39675  cdlemi1  39677  cdlemk3  39692  cdlemk4  39693  cdlemk9  39698  cdlemk9bN  39699  cdlemk10  39702  cdlemk39  39775  dia0eldmN  39899  dia1eldmN  39900  dia0  39911  dia1N  39912  diaglbN  39914  diaintclN  39917  dia2dimlem1  39923  dia2dimlem2  39924  dia2dimlem3  39925  dia2dimlem10  39932  dia2dimlem12  39934  cdlemm10N  39977  docaclN  39983  doca2N  39985  djajN  39996  dib0  40023  dibglbN  40025  dibintclN  40026  cdlemn2  40054  cdlemn10  40065  dihjustlem  40075  dihord1  40077  dihord2a  40078  dihord2b  40079  dihord2cN  40080  dihord11b  40081  dihord11c  40083  dihord2pre  40084  dihord2pre2  40085  dihlsscpre  40093  dib2dim  40102  dih2dimb  40103  dih2dimbALTN  40104  dihvalcq2  40106  dihopelvalcpre  40107  dihord6apre  40115  dihord5b  40118  dihord6b  40119  dihord5apre  40121  dih0  40139  dih1  40145  dihwN  40148  dihmeetlem1N  40149  dihglblem5apreN  40150  dihglblem5aN  40151  dihglblem2aN  40152  dihglblem2N  40153  dihglblem3N  40154  dihmeetlem2N  40158  dihglbcpreN  40159  dihmeetbclemN  40163  dihmeetlem3N  40164  dihmeetlem4preN  40165  dihmeetlem6  40168  dihjatc1  40170  dihmeetlem18N  40183  dih1dimatlem  40188  dihjatcclem1  40277  dihjatcclem2  40278  dihjatcclem4  40280