Theorem lhpbase 40368

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3442  ∅c0 4287   class class class wbr 5100  ‘cfv 6500  Basecbs 17148  1.cp1 18357   ⋖ ccvr 39632  LHypclh 40354

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-lhyp 40358

This theorem is referenced by:  lhplt  40370  lhp2lt  40371  lhpexlt  40372  lhp0lt  40373  lhpexle  40375  lhpexnle  40376  lhpexle1  40378  lhpexle2lem  40379  lhpexle3lem  40381  lhpocnle  40386  lhpocat  40387  lhpjat1  40390  lhpjat2  40391  lhpj1  40392  lhpmcvr  40393  lhpmcvr2  40394  lhpmcvr3  40395  lhpmcvr4N  40396  lhpmcvr5N  40397  lhpmcvr6N  40398  lhpm0atN  40399  lhpmat  40400  lhpmatb  40401  lhp2at0  40402  lhpelim  40407  lhpmod2i2  40408  lhpmod6i1  40409  cdlemb2  40411  lhpat  40413  lhpat3  40416  4atexlemwb  40429  ltrnatb  40507  ltrnel  40509  ltrncnvel  40512  trlval2  40533  trlcl  40534  trljat1  40536  trljat2  40537  trlle  40554  trlval3  40557  cdlemc1  40561  cdlemc2  40562  cdlemc4  40564  cdlemc5  40565  cdlemc6  40566  cdlemd2  40569  cdleme0aa  40580  cdleme0b  40582  cdleme0c  40583  cdleme0cp  40584  cdleme0cq  40585  cdleme0e  40587  cdleme0fN  40588  cdlemeulpq  40590  cdleme01N  40591  cdleme0ex1N  40593  cdleme1b  40596  cdleme1  40597  cdleme2  40598  cdleme3b  40599  cdleme3c  40600  cdleme3g  40604  cdleme3h  40605  cdleme3  40607  cdleme4  40608  cdleme4a  40609  cdleme5  40610  cdleme7aa  40612  cdleme7c  40615  cdleme7d  40616  cdleme7e  40617  cdleme7ga  40618  cdleme7  40619  cdleme8  40620  cdleme9b  40622  cdleme9  40623  cdleme10  40624  cdleme11fN  40634  cdleme11g  40635  cdleme11k  40638  cdleme13  40642  cdleme15b  40645  cdleme15d  40647  cdleme15  40648  cdleme16e  40652  cdleme16f  40653  cdleme22gb  40664  cdlemedb  40667  cdlemednpq  40669  cdleme19b  40674  cdleme19c  40675  cdleme20aN  40679  cdleme20c  40681  cdleme20d  40682  cdleme20e  40683  cdleme20j  40688  cdleme21c  40697  cdleme21ct  40699  cdleme22aa  40709  cdleme22cN  40712  cdleme22d  40713  cdleme22e  40714  cdleme22eALTN  40715  cdleme22f  40716  cdleme22g  40718  cdleme23a  40719  cdleme23b  40720  cdleme23c  40721  cdleme28a  40740  cdleme28b  40741  cdleme29ex  40744  cdleme30a  40748  cdlemefr29exN  40772  cdleme32b  40812  cdleme32c  40813  cdleme32e  40815  cdleme35b  40820  cdleme35c  40821  cdleme35d  40822  cdleme35e  40823  cdleme35f  40824  cdleme42a  40841  cdleme42c  40842  cdleme42h  40852  cdleme42i  40853  cdleme48bw  40872  cdlemeg46frv  40895  cdlemeg46vrg  40897  cdlemeg46rgv  40898  cdlemeg46req  40899  cdlemf1  40931  cdlemf2  40932  trlord  40939  cdlemg2fv2  40970  cdlemg2m  40974  cdlemg7fvbwN  40977  cdlemg4  40987  cdlemg6c  40990  cdlemg10bALTN  41006  cdlemg10c  41009  cdlemg10  41011  cdlemg11b  41012  cdlemg12f  41018  cdlemg17a  41031  cdlemg17dALTN  41034  cdlemg19a  41053  cdlemg35  41083  trlcoabs2N  41092  trlcolem  41096  cdlemh2  41186  cdlemi1  41188  cdlemk3  41203  cdlemk4  41204  cdlemk9  41209  cdlemk9bN  41210  cdlemk10  41213  cdlemk39  41286  dia0eldmN  41410  dia1eldmN  41411  dia0  41422  dia1N  41423  diaglbN  41425  diaintclN  41428  dia2dimlem1  41434  dia2dimlem2  41435  dia2dimlem3  41436  dia2dimlem10  41443  dia2dimlem12  41445  cdlemm10N  41488  docaclN  41494  doca2N  41496  djajN  41507  dib0  41534  dibglbN  41536  dibintclN  41537  cdlemn2  41565  cdlemn10  41576  dihjustlem  41586  dihord1  41588  dihord2a  41589  dihord2b  41590  dihord2cN  41591  dihord11b  41592  dihord11c  41594  dihord2pre  41595  dihord2pre2  41596  dihlsscpre  41604  dib2dim  41613  dih2dimb  41614  dih2dimbALTN  41615  dihvalcq2  41617  dihopelvalcpre  41618  dihord6apre  41626  dihord5b  41629  dihord6b  41630  dihord5apre  41632  dih0  41650  dih1  41656  dihwN  41659  dihmeetlem1N  41660  dihglblem5apreN  41661  dihglblem5aN  41662  dihglblem2aN  41663  dihglblem2N  41664  dihglblem3N  41665  dihmeetlem2N  41669  dihglbcpreN  41670  dihmeetbclemN  41674  dihmeetlem3N  41675  dihmeetlem4preN  41676  dihmeetlem6  41679  dihjatc1  41681  dihmeetlem18N  41694  dih1dimatlem  41699  dihjatcclem1  41788  dihjatcclem2  41789  dihjatcclem4  41791