Theorem lhpbase 40458

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ∅c0 4274   class class class wbr 5086  ‘cfv 6492  Basecbs 17170  1.cp1 18379   ⋖ ccvr 39722  LHypclh 40444

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 5231  ax-nul 5241  ax-pr 5370

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  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 40448

This theorem is referenced by:  lhplt  40460  lhp2lt  40461  lhpexlt  40462  lhp0lt  40463  lhpexle  40465  lhpexnle  40466  lhpexle1  40468  lhpexle2lem  40469  lhpexle3lem  40471  lhpocnle  40476  lhpocat  40477  lhpjat1  40480  lhpjat2  40481  lhpj1  40482  lhpmcvr  40483  lhpmcvr2  40484  lhpmcvr3  40485  lhpmcvr4N  40486  lhpmcvr5N  40487  lhpmcvr6N  40488  lhpm0atN  40489  lhpmat  40490  lhpmatb  40491  lhp2at0  40492  lhpelim  40497  lhpmod2i2  40498  lhpmod6i1  40499  cdlemb2  40501  lhpat  40503  lhpat3  40506  4atexlemwb  40519  ltrnatb  40597  ltrnel  40599  ltrncnvel  40602  trlval2  40623  trlcl  40624  trljat1  40626  trljat2  40627  trlle  40644  trlval3  40647  cdlemc1  40651  cdlemc2  40652  cdlemc4  40654  cdlemc5  40655  cdlemc6  40656  cdlemd2  40659  cdleme0aa  40670  cdleme0b  40672  cdleme0c  40673  cdleme0cp  40674  cdleme0cq  40675  cdleme0e  40677  cdleme0fN  40678  cdlemeulpq  40680  cdleme01N  40681  cdleme0ex1N  40683  cdleme1b  40686  cdleme1  40687  cdleme2  40688  cdleme3b  40689  cdleme3c  40690  cdleme3g  40694  cdleme3h  40695  cdleme3  40697  cdleme4  40698  cdleme4a  40699  cdleme5  40700  cdleme7aa  40702  cdleme7c  40705  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme7  40709  cdleme8  40710  cdleme9b  40712  cdleme9  40713  cdleme10  40714  cdleme11fN  40724  cdleme11g  40725  cdleme11k  40728  cdleme13  40732  cdleme15b  40735  cdleme15d  40737  cdleme15  40738  cdleme16e  40742  cdleme16f  40743  cdleme22gb  40754  cdlemedb  40757  cdlemednpq  40759  cdleme19b  40764  cdleme19c  40765  cdleme20aN  40769  cdleme20c  40771  cdleme20d  40772  cdleme20e  40773  cdleme20j  40778  cdleme21c  40787  cdleme21ct  40789  cdleme22aa  40799  cdleme22cN  40802  cdleme22d  40803  cdleme22e  40804  cdleme22eALTN  40805  cdleme22f  40806  cdleme22g  40808  cdleme23a  40809  cdleme23b  40810  cdleme23c  40811  cdleme28a  40830  cdleme28b  40831  cdleme29ex  40834  cdleme30a  40838  cdlemefr29exN  40862  cdleme32b  40902  cdleme32c  40903  cdleme32e  40905  cdleme35b  40910  cdleme35c  40911  cdleme35d  40912  cdleme35e  40913  cdleme35f  40914  cdleme42a  40931  cdleme42c  40932  cdleme42h  40942  cdleme42i  40943  cdleme48bw  40962  cdlemeg46frv  40985  cdlemeg46vrg  40987  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemf1  41021  cdlemf2  41022  trlord  41029  cdlemg2fv2  41060  cdlemg2m  41064  cdlemg7fvbwN  41067  cdlemg4  41077  cdlemg6c  41080  cdlemg10bALTN  41096  cdlemg10c  41099  cdlemg10  41101  cdlemg11b  41102  cdlemg12f  41108  cdlemg17a  41121  cdlemg17dALTN  41124  cdlemg19a  41143  cdlemg35  41173  trlcoabs2N  41182  trlcolem  41186  cdlemh2  41276  cdlemi1  41278  cdlemk3  41293  cdlemk4  41294  cdlemk9  41299  cdlemk9bN  41300  cdlemk10  41303  cdlemk39  41376  dia0eldmN  41500  dia1eldmN  41501  dia0  41512  dia1N  41513  diaglbN  41515  diaintclN  41518  dia2dimlem1  41524  dia2dimlem2  41525  dia2dimlem3  41526  dia2dimlem10  41533  dia2dimlem12  41535  cdlemm10N  41578  docaclN  41584  doca2N  41586  djajN  41597  dib0  41624  dibglbN  41626  dibintclN  41627  cdlemn2  41655  cdlemn10  41666  dihjustlem  41676  dihord1  41678  dihord2a  41679  dihord2b  41680  dihord2cN  41681  dihord11b  41682  dihord11c  41684  dihord2pre  41685  dihord2pre2  41686  dihlsscpre  41694  dib2dim  41703  dih2dimb  41704  dih2dimbALTN  41705  dihvalcq2  41707  dihopelvalcpre  41708  dihord6apre  41716  dihord5b  41719  dihord6b  41720  dihord5apre  41722  dih0  41740  dih1  41746  dihwN  41749  dihmeetlem1N  41750  dihglblem5apreN  41751  dihglblem5aN  41752  dihglblem2aN  41753  dihglblem2N  41754  dihglblem3N  41755  dihmeetlem2N  41759  dihglbcpreN  41760  dihmeetbclemN  41764  dihmeetlem3N  41765  dihmeetlem4preN  41766  dihmeetlem6  41769  dihjatc1  41771  dihmeetlem18N  41784  dih1dimatlem  41789  dihjatcclem1  41878  dihjatcclem2  41879  dihjatcclem4  41881