Theorem lhpbase 37939

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 4264	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2743	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 327	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6748	. . 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 37937	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 498	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 684	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  Vcvv 3422  ∅c0 4253   class class class wbr 5070  ‘cfv 6418  Basecbs 16840  1.cp1 18057   ⋖ ccvr 37203  LHypclh 37925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426  df-lhyp 37929

This theorem is referenced by:  lhplt  37941  lhp2lt  37942  lhpexlt  37943  lhp0lt  37944  lhpexle  37946  lhpexnle  37947  lhpexle1  37949  lhpexle2lem  37950  lhpexle3lem  37952  lhpocnle  37957  lhpocat  37958  lhpjat1  37961  lhpjat2  37962  lhpj1  37963  lhpmcvr  37964  lhpmcvr2  37965  lhpmcvr3  37966  lhpmcvr4N  37967  lhpmcvr5N  37968  lhpmcvr6N  37969  lhpm0atN  37970  lhpmat  37971  lhpmatb  37972  lhp2at0  37973  lhpelim  37978  lhpmod2i2  37979  lhpmod6i1  37980  cdlemb2  37982  lhpat  37984  lhpat3  37987  4atexlemwb  38000  ltrnatb  38078  ltrnel  38080  ltrncnvel  38083  trlval2  38104  trlcl  38105  trljat1  38107  trljat2  38108  trlle  38125  trlval3  38128  cdlemc1  38132  cdlemc2  38133  cdlemc4  38135  cdlemc5  38136  cdlemc6  38137  cdlemd2  38140  cdleme0aa  38151  cdleme0b  38153  cdleme0c  38154  cdleme0cp  38155  cdleme0cq  38156  cdleme0e  38158  cdleme0fN  38159  cdlemeulpq  38161  cdleme01N  38162  cdleme0ex1N  38164  cdleme1b  38167  cdleme1  38168  cdleme2  38169  cdleme3b  38170  cdleme3c  38171  cdleme3g  38175  cdleme3h  38176  cdleme3  38178  cdleme4  38179  cdleme4a  38180  cdleme5  38181  cdleme7aa  38183  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme7  38190  cdleme8  38191  cdleme9b  38193  cdleme9  38194  cdleme10  38195  cdleme11fN  38205  cdleme11g  38206  cdleme11k  38209  cdleme13  38213  cdleme15b  38216  cdleme15d  38218  cdleme15  38219  cdleme16e  38223  cdleme16f  38224  cdleme22gb  38235  cdlemedb  38238  cdlemednpq  38240  cdleme19b  38245  cdleme19c  38246  cdleme20aN  38250  cdleme20c  38252  cdleme20d  38253  cdleme20e  38254  cdleme20j  38259  cdleme21c  38268  cdleme21ct  38270  cdleme22aa  38280  cdleme22cN  38283  cdleme22d  38284  cdleme22e  38285  cdleme22eALTN  38286  cdleme22f  38287  cdleme22g  38289  cdleme23a  38290  cdleme23b  38291  cdleme23c  38292  cdleme28a  38311  cdleme28b  38312  cdleme29ex  38315  cdleme30a  38319  cdlemefr29exN  38343  cdleme32b  38383  cdleme32c  38384  cdleme32e  38386  cdleme35b  38391  cdleme35c  38392  cdleme35d  38393  cdleme35e  38394  cdleme35f  38395  cdleme42a  38412  cdleme42c  38413  cdleme42h  38423  cdleme42i  38424  cdleme48bw  38443  cdlemeg46frv  38466  cdlemeg46vrg  38468  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemf1  38502  cdlemf2  38503  trlord  38510  cdlemg2fv2  38541  cdlemg2m  38545  cdlemg7fvbwN  38548  cdlemg4  38558  cdlemg6c  38561  cdlemg10bALTN  38577  cdlemg10c  38580  cdlemg10  38582  cdlemg11b  38583  cdlemg12f  38589  cdlemg17a  38602  cdlemg17dALTN  38605  cdlemg19a  38624  cdlemg35  38654  trlcoabs2N  38663  trlcolem  38667  cdlemh2  38757  cdlemi1  38759  cdlemk3  38774  cdlemk4  38775  cdlemk9  38780  cdlemk9bN  38781  cdlemk10  38784  cdlemk39  38857  dia0eldmN  38981  dia1eldmN  38982  dia0  38993  dia1N  38994  diaglbN  38996  diaintclN  38999  dia2dimlem1  39005  dia2dimlem2  39006  dia2dimlem3  39007  dia2dimlem10  39014  dia2dimlem12  39016  cdlemm10N  39059  docaclN  39065  doca2N  39067  djajN  39078  dib0  39105  dibglbN  39107  dibintclN  39108  cdlemn2  39136  cdlemn10  39147  dihjustlem  39157  dihord1  39159  dihord2a  39160  dihord2b  39161  dihord2cN  39162  dihord11b  39163  dihord11c  39165  dihord2pre  39166  dihord2pre2  39167  dihlsscpre  39175  dib2dim  39184  dih2dimb  39185  dih2dimbALTN  39186  dihvalcq2  39188  dihopelvalcpre  39189  dihord6apre  39197  dihord5b  39200  dihord6b  39201  dihord5apre  39203  dih0  39221  dih1  39227  dihwN  39230  dihmeetlem1N  39231  dihglblem5apreN  39232  dihglblem5aN  39233  dihglblem2aN  39234  dihglblem2N  39235  dihglblem3N  39236  dihmeetlem2N  39240  dihglbcpreN  39241  dihmeetbclemN  39245  dihmeetlem3N  39246  dihmeetlem4preN  39247  dihmeetlem6  39250  dihjatc1  39252  dihmeetlem18N  39265  dih1dimatlem  39270  dihjatcclem1  39359  dihjatcclem2  39360  dihjatcclem4  39362