Theorem lhpbase 39172

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 4333	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2737	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 327	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6883	. . 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 39170	. . 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 4322   class class class wbr 5148  ‘cfv 6543  Basecbs 17148  1.cp1 18381   ⋖ ccvr 38435  LHypclh 39158

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 5299  ax-nul 5306  ax-pr 5427

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-lhyp 39162

This theorem is referenced by:  lhplt  39174  lhp2lt  39175  lhpexlt  39176  lhp0lt  39177  lhpexle  39179  lhpexnle  39180  lhpexle1  39182  lhpexle2lem  39183  lhpexle3lem  39185  lhpocnle  39190  lhpocat  39191  lhpjat1  39194  lhpjat2  39195  lhpj1  39196  lhpmcvr  39197  lhpmcvr2  39198  lhpmcvr3  39199  lhpmcvr4N  39200  lhpmcvr5N  39201  lhpmcvr6N  39202  lhpm0atN  39203  lhpmat  39204  lhpmatb  39205  lhp2at0  39206  lhpelim  39211  lhpmod2i2  39212  lhpmod6i1  39213  cdlemb2  39215  lhpat  39217  lhpat3  39220  4atexlemwb  39233  ltrnatb  39311  ltrnel  39313  ltrncnvel  39316  trlval2  39337  trlcl  39338  trljat1  39340  trljat2  39341  trlle  39358  trlval3  39361  cdlemc1  39365  cdlemc2  39366  cdlemc4  39368  cdlemc5  39369  cdlemc6  39370  cdlemd2  39373  cdleme0aa  39384  cdleme0b  39386  cdleme0c  39387  cdleme0cp  39388  cdleme0cq  39389  cdleme0e  39391  cdleme0fN  39392  cdlemeulpq  39394  cdleme01N  39395  cdleme0ex1N  39397  cdleme1b  39400  cdleme1  39401  cdleme2  39402  cdleme3b  39403  cdleme3c  39404  cdleme3g  39408  cdleme3h  39409  cdleme3  39411  cdleme4  39412  cdleme4a  39413  cdleme5  39414  cdleme7aa  39416  cdleme7c  39419  cdleme7d  39420  cdleme7e  39421  cdleme7ga  39422  cdleme7  39423  cdleme8  39424  cdleme9b  39426  cdleme9  39427  cdleme10  39428  cdleme11fN  39438  cdleme11g  39439  cdleme11k  39442  cdleme13  39446  cdleme15b  39449  cdleme15d  39451  cdleme15  39452  cdleme16e  39456  cdleme16f  39457  cdleme22gb  39468  cdlemedb  39471  cdlemednpq  39473  cdleme19b  39478  cdleme19c  39479  cdleme20aN  39483  cdleme20c  39485  cdleme20d  39486  cdleme20e  39487  cdleme20j  39492  cdleme21c  39501  cdleme21ct  39503  cdleme22aa  39513  cdleme22cN  39516  cdleme22d  39517  cdleme22e  39518  cdleme22eALTN  39519  cdleme22f  39520  cdleme22g  39522  cdleme23a  39523  cdleme23b  39524  cdleme23c  39525  cdleme28a  39544  cdleme28b  39545  cdleme29ex  39548  cdleme30a  39552  cdlemefr29exN  39576  cdleme32b  39616  cdleme32c  39617  cdleme32e  39619  cdleme35b  39624  cdleme35c  39625  cdleme35d  39626  cdleme35e  39627  cdleme35f  39628  cdleme42a  39645  cdleme42c  39646  cdleme42h  39656  cdleme42i  39657  cdleme48bw  39676  cdlemeg46frv  39699  cdlemeg46vrg  39701  cdlemeg46rgv  39702  cdlemeg46req  39703  cdlemf1  39735  cdlemf2  39736  trlord  39743  cdlemg2fv2  39774  cdlemg2m  39778  cdlemg7fvbwN  39781  cdlemg4  39791  cdlemg6c  39794  cdlemg10bALTN  39810  cdlemg10c  39813  cdlemg10  39815  cdlemg11b  39816  cdlemg12f  39822  cdlemg17a  39835  cdlemg17dALTN  39838  cdlemg19a  39857  cdlemg35  39887  trlcoabs2N  39896  trlcolem  39900  cdlemh2  39990  cdlemi1  39992  cdlemk3  40007  cdlemk4  40008  cdlemk9  40013  cdlemk9bN  40014  cdlemk10  40017  cdlemk39  40090  dia0eldmN  40214  dia1eldmN  40215  dia0  40226  dia1N  40227  diaglbN  40229  diaintclN  40232  dia2dimlem1  40238  dia2dimlem2  40239  dia2dimlem3  40240  dia2dimlem10  40247  dia2dimlem12  40249  cdlemm10N  40292  docaclN  40298  doca2N  40300  djajN  40311  dib0  40338  dibglbN  40340  dibintclN  40341  cdlemn2  40369  cdlemn10  40380  dihjustlem  40390  dihord1  40392  dihord2a  40393  dihord2b  40394  dihord2cN  40395  dihord11b  40396  dihord11c  40398  dihord2pre  40399  dihord2pre2  40400  dihlsscpre  40408  dib2dim  40417  dih2dimb  40418  dih2dimbALTN  40419  dihvalcq2  40421  dihopelvalcpre  40422  dihord6apre  40430  dihord5b  40433  dihord6b  40434  dihord5apre  40436  dih0  40454  dih1  40460  dihwN  40463  dihmeetlem1N  40464  dihglblem5apreN  40465  dihglblem5aN  40466  dihglblem2aN  40467  dihglblem2N  40468  dihglblem3N  40469  dihmeetlem2N  40473  dihglbcpreN  40474  dihmeetbclemN  40478  dihmeetlem3N  40479  dihmeetlem4preN  40480  dihmeetlem6  40483  dihjatc1  40485  dihmeetlem18N  40498  dih1dimatlem  40503  dihjatcclem1  40592  dihjatcclem2  40593  dihjatcclem4  40595