Theorem lhpbase 34302

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 3879	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2615	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 317	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6097	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 141	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2610	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2610	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 34300	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 651	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 700	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  Vcvv 3173  ∅c0 3874   class class class wbr 4583  ‘cfv 5804  Basecbs 15695  1.cp1 16861   ⋖ ccvr 33567  LHypclh 34288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fv 5812  df-lhyp 34292

This theorem is referenced by:  lhplt  34304  lhp2lt  34305  lhpexlt  34306  lhp0lt  34307  lhpexle  34309  lhpexnle  34310  lhpexle1  34312  lhpexle2lem  34313  lhpexle3lem  34315  lhpocnle  34320  lhpocat  34321  lhpjat1  34324  lhpjat2  34325  lhpj1  34326  lhpmcvr  34327  lhpmcvr2  34328  lhpmcvr3  34329  lhpmcvr4N  34330  lhpmcvr5N  34331  lhpmcvr6N  34332  lhpm0atN  34333  lhpmat  34334  lhpmatb  34335  lhp2at0  34336  lhpelim  34341  lhpmod2i2  34342  lhpmod6i1  34343  cdlemb2  34345  lhpat  34347  lhpat3  34350  4atexlemwb  34363  ltrnatb  34441  ltrnel  34443  ltrncnvel  34446  ltrnmwOLD  34456  trlval2  34468  trlcl  34469  trljat1  34471  trljat2  34472  trlle  34489  trlval3  34492  cdlemc1  34496  cdlemc2  34497  cdlemc4  34499  cdlemc5  34500  cdlemc6  34501  cdlemd2  34504  cdleme0aa  34515  cdleme0b  34517  cdleme0c  34518  cdleme0cp  34519  cdleme0cq  34520  cdleme0e  34522  cdleme0fN  34523  cdlemeulpq  34525  cdleme01N  34526  cdleme0ex1N  34528  cdleme1b  34531  cdleme1  34532  cdleme2  34533  cdleme3b  34534  cdleme3c  34535  cdleme3g  34539  cdleme3h  34540  cdleme3  34542  cdleme4  34543  cdleme4a  34544  cdleme5  34545  cdleme7aa  34547  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme8  34555  cdleme9b  34557  cdleme9  34558  cdleme10  34559  cdleme11fN  34569  cdleme11g  34570  cdleme11k  34573  cdleme13  34577  cdleme15b  34580  cdleme15d  34582  cdleme15  34583  cdleme16e  34587  cdleme16f  34588  cdleme22gb  34599  cdlemedb  34602  cdlemednpq  34604  cdleme19b  34610  cdleme19c  34611  cdleme20aN  34615  cdleme20c  34617  cdleme20d  34618  cdleme20e  34619  cdleme20j  34624  cdleme21c  34633  cdleme21ct  34635  cdleme22aa  34645  cdleme22cN  34648  cdleme22d  34649  cdleme22e  34650  cdleme22eALTN  34651  cdleme22f  34652  cdleme22g  34654  cdleme23a  34655  cdleme23b  34656  cdleme23c  34657  cdleme28a  34676  cdleme28b  34677  cdleme29ex  34680  cdleme30a  34684  cdlemefr29exN  34708  cdleme32b  34748  cdleme32c  34749  cdleme32e  34751  cdleme35b  34756  cdleme35c  34757  cdleme35d  34758  cdleme35e  34759  cdleme35f  34760  cdleme42a  34777  cdleme42c  34778  cdleme42h  34788  cdleme42i  34789  cdleme48bw  34808  cdlemeg46frv  34831  cdlemeg46vrg  34833  cdlemeg46rgv  34834  cdlemeg46req  34835  cdlemf1  34867  cdlemf2  34868  trlord  34875  cdlemg2fv2  34906  cdlemg2m  34910  cdlemg7fvbwN  34913  cdlemg4  34923  cdlemg6c  34926  cdlemg10bALTN  34942  cdlemg10c  34945  cdlemg10  34947  cdlemg11b  34948  cdlemg12f  34954  cdlemg17a  34967  cdlemg17dALTN  34970  cdlemg19a  34989  cdlemg35  35019  trlcoabs2N  35028  trlcolem  35032  cdlemh2  35122  cdlemi1  35124  cdlemk3  35139  cdlemk4  35140  cdlemk9  35145  cdlemk9bN  35146  cdlemk10  35149  cdlemk39  35222  dia0eldmN  35347  dia1eldmN  35348  dia0  35359  dia1N  35360  diaglbN  35362  diaintclN  35365  dia2dimlem1  35371  dia2dimlem2  35372  dia2dimlem3  35373  dia2dimlem10  35380  dia2dimlem12  35382  cdlemm10N  35425  docaclN  35431  doca2N  35433  djajN  35444  dib0  35471  dibglbN  35473  dibintclN  35474  cdlemn2  35502  cdlemn10  35513  dihjustlem  35523  dihord1  35525  dihord2a  35526  dihord2b  35527  dihord2cN  35528  dihord11b  35529  dihord11c  35531  dihord2pre  35532  dihord2pre2  35533  dihlsscpre  35541  dib2dim  35550  dih2dimb  35551  dih2dimbALTN  35552  dihvalcq2  35554  dihopelvalcpre  35555  dihord6apre  35563  dihord5b  35566  dihord6b  35567  dihord5apre  35569  dih0  35587  dih1  35593  dihwN  35596  dihmeetlem1N  35597  dihglblem5apreN  35598  dihglblem5aN  35599  dihglblem2aN  35600  dihglblem2N  35601  dihglblem3N  35602  dihmeetlem2N  35606  dihglbcpreN  35607  dihmeetbclemN  35611  dihmeetlem3N  35612  dihmeetlem4preN  35613  dihmeetlem6  35616  dihjatc1  35618  dihmeetlem18N  35631  dih1dimatlem  35636  dihjatcclem1  35725  dihjatcclem2  35726  dihjatcclem4  35728