Theorem lhpbase 40254

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3440  ∅c0 4285   class class class wbr 5098  ‘cfv 6492  Basecbs 17136  1.cp1 18345   ⋖ ccvr 39518  LHypclh 40240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-lhyp 40244

This theorem is referenced by:  lhplt  40256  lhp2lt  40257  lhpexlt  40258  lhp0lt  40259  lhpexle  40261  lhpexnle  40262  lhpexle1  40264  lhpexle2lem  40265  lhpexle3lem  40267  lhpocnle  40272  lhpocat  40273  lhpjat1  40276  lhpjat2  40277  lhpj1  40278  lhpmcvr  40279  lhpmcvr2  40280  lhpmcvr3  40281  lhpmcvr4N  40282  lhpmcvr5N  40283  lhpmcvr6N  40284  lhpm0atN  40285  lhpmat  40286  lhpmatb  40287  lhp2at0  40288  lhpelim  40293  lhpmod2i2  40294  lhpmod6i1  40295  cdlemb2  40297  lhpat  40299  lhpat3  40302  4atexlemwb  40315  ltrnatb  40393  ltrnel  40395  ltrncnvel  40398  trlval2  40419  trlcl  40420  trljat1  40422  trljat2  40423  trlle  40440  trlval3  40443  cdlemc1  40447  cdlemc2  40448  cdlemc4  40450  cdlemc5  40451  cdlemc6  40452  cdlemd2  40455  cdleme0aa  40466  cdleme0b  40468  cdleme0c  40469  cdleme0cp  40470  cdleme0cq  40471  cdleme0e  40473  cdleme0fN  40474  cdlemeulpq  40476  cdleme01N  40477  cdleme0ex1N  40479  cdleme1b  40482  cdleme1  40483  cdleme2  40484  cdleme3b  40485  cdleme3c  40486  cdleme3g  40490  cdleme3h  40491  cdleme3  40493  cdleme4  40494  cdleme4a  40495  cdleme5  40496  cdleme7aa  40498  cdleme7c  40501  cdleme7d  40502  cdleme7e  40503  cdleme7ga  40504  cdleme7  40505  cdleme8  40506  cdleme9b  40508  cdleme9  40509  cdleme10  40510  cdleme11fN  40520  cdleme11g  40521  cdleme11k  40524  cdleme13  40528  cdleme15b  40531  cdleme15d  40533  cdleme15  40534  cdleme16e  40538  cdleme16f  40539  cdleme22gb  40550  cdlemedb  40553  cdlemednpq  40555  cdleme19b  40560  cdleme19c  40561  cdleme20aN  40565  cdleme20c  40567  cdleme20d  40568  cdleme20e  40569  cdleme20j  40574  cdleme21c  40583  cdleme21ct  40585  cdleme22aa  40595  cdleme22cN  40598  cdleme22d  40599  cdleme22e  40600  cdleme22eALTN  40601  cdleme22f  40602  cdleme22g  40604  cdleme23a  40605  cdleme23b  40606  cdleme23c  40607  cdleme28a  40626  cdleme28b  40627  cdleme29ex  40630  cdleme30a  40634  cdlemefr29exN  40658  cdleme32b  40698  cdleme32c  40699  cdleme32e  40701  cdleme35b  40706  cdleme35c  40707  cdleme35d  40708  cdleme35e  40709  cdleme35f  40710  cdleme42a  40727  cdleme42c  40728  cdleme42h  40738  cdleme42i  40739  cdleme48bw  40758  cdlemeg46frv  40781  cdlemeg46vrg  40783  cdlemeg46rgv  40784  cdlemeg46req  40785  cdlemf1  40817  cdlemf2  40818  trlord  40825  cdlemg2fv2  40856  cdlemg2m  40860  cdlemg7fvbwN  40863  cdlemg4  40873  cdlemg6c  40876  cdlemg10bALTN  40892  cdlemg10c  40895  cdlemg10  40897  cdlemg11b  40898  cdlemg12f  40904  cdlemg17a  40917  cdlemg17dALTN  40920  cdlemg19a  40939  cdlemg35  40969  trlcoabs2N  40978  trlcolem  40982  cdlemh2  41072  cdlemi1  41074  cdlemk3  41089  cdlemk4  41090  cdlemk9  41095  cdlemk9bN  41096  cdlemk10  41099  cdlemk39  41172  dia0eldmN  41296  dia1eldmN  41297  dia0  41308  dia1N  41309  diaglbN  41311  diaintclN  41314  dia2dimlem1  41320  dia2dimlem2  41321  dia2dimlem3  41322  dia2dimlem10  41329  dia2dimlem12  41331  cdlemm10N  41374  docaclN  41380  doca2N  41382  djajN  41393  dib0  41420  dibglbN  41422  dibintclN  41423  cdlemn2  41451  cdlemn10  41462  dihjustlem  41472  dihord1  41474  dihord2a  41475  dihord2b  41476  dihord2cN  41477  dihord11b  41478  dihord11c  41480  dihord2pre  41481  dihord2pre2  41482  dihlsscpre  41490  dib2dim  41499  dih2dimb  41500  dih2dimbALTN  41501  dihvalcq2  41503  dihopelvalcpre  41504  dihord6apre  41512  dihord5b  41515  dihord6b  41516  dihord5apre  41518  dih0  41536  dih1  41542  dihwN  41545  dihmeetlem1N  41546  dihglblem5apreN  41547  dihglblem5aN  41548  dihglblem2aN  41549  dihglblem2N  41550  dihglblem3N  41551  dihmeetlem2N  41555  dihglbcpreN  41556  dihmeetbclemN  41560  dihmeetlem3N  41561  dihmeetlem4preN  41562  dihmeetlem6  41565  dihjatc1  41567  dihmeetlem18N  41580  dih1dimatlem  41585  dihjatcclem1  41674  dihjatcclem2  41675  dihjatcclem4  41677