Theorem lhpbase 40017

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 4315	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2740	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 328	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6868	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 141	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2735	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2735	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 40015	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 498	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 688	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3459  ∅c0 4308   class class class wbr 5119  ‘cfv 6531  Basecbs 17228  1.cp1 18434   ⋖ ccvr 39280  LHypclh 40003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6484  df-fun 6533  df-fv 6539  df-lhyp 40007

This theorem is referenced by:  lhplt  40019  lhp2lt  40020  lhpexlt  40021  lhp0lt  40022  lhpexle  40024  lhpexnle  40025  lhpexle1  40027  lhpexle2lem  40028  lhpexle3lem  40030  lhpocnle  40035  lhpocat  40036  lhpjat1  40039  lhpjat2  40040  lhpj1  40041  lhpmcvr  40042  lhpmcvr2  40043  lhpmcvr3  40044  lhpmcvr4N  40045  lhpmcvr5N  40046  lhpmcvr6N  40047  lhpm0atN  40048  lhpmat  40049  lhpmatb  40050  lhp2at0  40051  lhpelim  40056  lhpmod2i2  40057  lhpmod6i1  40058  cdlemb2  40060  lhpat  40062  lhpat3  40065  4atexlemwb  40078  ltrnatb  40156  ltrnel  40158  ltrncnvel  40161  trlval2  40182  trlcl  40183  trljat1  40185  trljat2  40186  trlle  40203  trlval3  40206  cdlemc1  40210  cdlemc2  40211  cdlemc4  40213  cdlemc5  40214  cdlemc6  40215  cdlemd2  40218  cdleme0aa  40229  cdleme0b  40231  cdleme0c  40232  cdleme0cp  40233  cdleme0cq  40234  cdleme0e  40236  cdleme0fN  40237  cdlemeulpq  40239  cdleme01N  40240  cdleme0ex1N  40242  cdleme1b  40245  cdleme1  40246  cdleme2  40247  cdleme3b  40248  cdleme3c  40249  cdleme3g  40253  cdleme3h  40254  cdleme3  40256  cdleme4  40257  cdleme4a  40258  cdleme5  40259  cdleme7aa  40261  cdleme7c  40264  cdleme7d  40265  cdleme7e  40266  cdleme7ga  40267  cdleme7  40268  cdleme8  40269  cdleme9b  40271  cdleme9  40272  cdleme10  40273  cdleme11fN  40283  cdleme11g  40284  cdleme11k  40287  cdleme13  40291  cdleme15b  40294  cdleme15d  40296  cdleme15  40297  cdleme16e  40301  cdleme16f  40302  cdleme22gb  40313  cdlemedb  40316  cdlemednpq  40318  cdleme19b  40323  cdleme19c  40324  cdleme20aN  40328  cdleme20c  40330  cdleme20d  40331  cdleme20e  40332  cdleme20j  40337  cdleme21c  40346  cdleme21ct  40348  cdleme22aa  40358  cdleme22cN  40361  cdleme22d  40362  cdleme22e  40363  cdleme22eALTN  40364  cdleme22f  40365  cdleme22g  40367  cdleme23a  40368  cdleme23b  40369  cdleme23c  40370  cdleme28a  40389  cdleme28b  40390  cdleme29ex  40393  cdleme30a  40397  cdlemefr29exN  40421  cdleme32b  40461  cdleme32c  40462  cdleme32e  40464  cdleme35b  40469  cdleme35c  40470  cdleme35d  40471  cdleme35e  40472  cdleme35f  40473  cdleme42a  40490  cdleme42c  40491  cdleme42h  40501  cdleme42i  40502  cdleme48bw  40521  cdlemeg46frv  40544  cdlemeg46vrg  40546  cdlemeg46rgv  40547  cdlemeg46req  40548  cdlemf1  40580  cdlemf2  40581  trlord  40588  cdlemg2fv2  40619  cdlemg2m  40623  cdlemg7fvbwN  40626  cdlemg4  40636  cdlemg6c  40639  cdlemg10bALTN  40655  cdlemg10c  40658  cdlemg10  40660  cdlemg11b  40661  cdlemg12f  40667  cdlemg17a  40680  cdlemg17dALTN  40683  cdlemg19a  40702  cdlemg35  40732  trlcoabs2N  40741  trlcolem  40745  cdlemh2  40835  cdlemi1  40837  cdlemk3  40852  cdlemk4  40853  cdlemk9  40858  cdlemk9bN  40859  cdlemk10  40862  cdlemk39  40935  dia0eldmN  41059  dia1eldmN  41060  dia0  41071  dia1N  41072  diaglbN  41074  diaintclN  41077  dia2dimlem1  41083  dia2dimlem2  41084  dia2dimlem3  41085  dia2dimlem10  41092  dia2dimlem12  41094  cdlemm10N  41137  docaclN  41143  doca2N  41145  djajN  41156  dib0  41183  dibglbN  41185  dibintclN  41186  cdlemn2  41214  cdlemn10  41225  dihjustlem  41235  dihord1  41237  dihord2a  41238  dihord2b  41239  dihord2cN  41240  dihord11b  41241  dihord11c  41243  dihord2pre  41244  dihord2pre2  41245  dihlsscpre  41253  dib2dim  41262  dih2dimb  41263  dih2dimbALTN  41264  dihvalcq2  41266  dihopelvalcpre  41267  dihord6apre  41275  dihord5b  41278  dihord6b  41279  dihord5apre  41281  dih0  41299  dih1  41305  dihwN  41308  dihmeetlem1N  41309  dihglblem5apreN  41310  dihglblem5aN  41311  dihglblem2aN  41312  dihglblem2N  41313  dihglblem3N  41314  dihmeetlem2N  41318  dihglbcpreN  41319  dihmeetbclemN  41323  dihmeetlem3N  41324  dihmeetlem4preN  41325  dihmeetlem6  41328  dihjatc1  41330  dihmeetlem18N  41343  dih1dimatlem  41348  dihjatcclem1  41437  dihjatcclem2  41438  dihjatcclem4  41440