Theorem lhpbase 41258

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 4289	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2768	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6903	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 142	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2763	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2763	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 41256	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 504	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 701	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  Vcvv 3454  ∅c0 4281   class class class wbr 5106  ‘cfv 6561  Basecbs 17419  1.cp1 18628   ⋖ ccvr 40522  LHypclh 41244

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-iota 6515  df-fun 6563  df-fv 6569  df-lhyp 41248

This theorem is used by:  lhplt  41260  lhp2lt  41261  lhpexlt  41262  lhp0lt  41263  lhpexle  41265  lhpexnle  41266  lhpexle1  41268  lhpexle2lem  41269  lhpexle3lem  41271  lhpocnle  41276  lhpocat  41277  lhpjat1  41280  lhpjat2  41281  lhpj1  41282  lhpmcvr  41283  lhpmcvr2  41284  lhpmcvr3  41285  lhpmcvr4N  41286  lhpmcvr5N  41287  lhpmcvr6N  41288  lhpm0atN  41289  lhpmat  41290  lhpmatb  41291  lhp2at0  41292  lhpelim  41297  lhpmod2i2  41298  lhpmod6i1  41299  cdlemb2  41301  lhpat  41303  lhpat3  41306  4atexlemwb  41319  ltrnatb  41397  ltrnel  41399  ltrncnvel  41402  trlval2  41423  trlcl  41424  trljat1  41426  trljat2  41427  trlle  41444  trlval3  41447  cdlemc1  41451  cdlemc2  41452  cdlemc4  41454  cdlemc5  41455  cdlemc6  41456  cdlemd2  41459  cdleme0aa  41470  cdleme0b  41472  cdleme0c  41473  cdleme0cp  41474  cdleme0cq  41475  cdleme0e  41477  cdleme0fN  41478  cdlemeulpq  41480  cdleme01N  41481  cdleme0ex1N  41483  cdleme1b  41486  cdleme1  41487  cdleme2  41488  cdleme3b  41489  cdleme3c  41490  cdleme3g  41494  cdleme3h  41495  cdleme3  41497  cdleme4  41498  cdleme4a  41499  cdleme5  41500  cdleme7aa  41502  cdleme7c  41505  cdleme7d  41506  cdleme7e  41507  cdleme7ga  41508  cdleme7  41509  cdleme8  41510  cdleme9b  41512  cdleme9  41513  cdleme10  41514  cdleme11fN  41524  cdleme11g  41525  cdleme11k  41528  cdleme13  41532  cdleme15b  41535  cdleme15d  41537  cdleme15  41538  cdleme16e  41542  cdleme16f  41543  cdleme22gb  41554  cdlemedb  41557  cdlemednpq  41559  cdleme19b  41564  cdleme19c  41565  cdleme20aN  41569  cdleme20c  41571  cdleme20d  41572  cdleme20e  41573  cdleme20j  41578  cdleme21c  41587  cdleme21ct  41589  cdleme22aa  41599  cdleme22cN  41602  cdleme22d  41603  cdleme22e  41604  cdleme22eALTN  41605  cdleme22f  41606  cdleme22g  41608  cdleme23a  41609  cdleme23b  41610  cdleme23c  41611  cdleme28a  41630  cdleme28b  41631  cdleme29ex  41634  cdleme30a  41638  cdlemefr29exN  41662  cdleme32b  41702  cdleme32c  41703  cdleme32e  41705  cdleme35b  41710  cdleme35c  41711  cdleme35d  41712  cdleme35e  41713  cdleme35f  41714  cdleme42a  41731  cdleme42c  41732  cdleme42h  41742  cdleme42i  41743  cdleme48bw  41762  cdlemeg46frv  41785  cdlemeg46vrg  41787  cdlemeg46rgv  41788  cdlemeg46req  41789  cdlemf1  41821  cdlemf2  41822  trlord  41829  cdlemg2fv2  41860  cdlemg2m  41864  cdlemg7fvbwN  41867  cdlemg4  41877  cdlemg6c  41880  cdlemg10bALTN  41896  cdlemg10c  41899  cdlemg10  41901  cdlemg11b  41902  cdlemg12f  41908  cdlemg17a  41921  cdlemg17dALTN  41924  cdlemg19a  41943  cdlemg35  41973  trlcoabs2N  41982  trlcolem  41986  cdlemh2  42076  cdlemi1  42078  cdlemk3  42093  cdlemk4  42094  cdlemk9  42099  cdlemk9bN  42100  cdlemk10  42103  cdlemk39  42176  dia0eldmN  42300  dia1eldmN  42301  dia0  42312  dia1N  42313  diaglbN  42315  diaintclN  42318  dia2dimlem1  42324  dia2dimlem2  42325  dia2dimlem3  42326  dia2dimlem10  42333  dia2dimlem12  42335  cdlemm10N  42378  docaclN  42384  doca2N  42386  djajN  42397  dib0  42424  dibglbN  42426  dibintclN  42427  cdlemn2  42455  cdlemn10  42466  dihjustlem  42476  dihord1  42478  dihord2a  42479  dihord2b  42480  dihord2cN  42481  dihord11b  42482  dihord11c  42484  dihord2pre  42485  dihord2pre2  42486  dihlsscpre  42494  dib2dim  42503  dih2dimb  42504  dih2dimbALTN  42505  dihvalcq2  42507  dihopelvalcpre  42508  dihord6apre  42516  dihord5b  42519  dihord6b  42520  dihord5apre  42522  dih0  42540  dih1  42546  dihwN  42549  dihmeetlem1N  42550  dihglblem5apreN  42551  dihglblem5aN  42552  dihglblem2aN  42553  dihglblem2N  42554  dihglblem3N  42555  dihmeetlem2N  42559  dihglbcpreN  42560  dihmeetbclemN  42564  dihmeetlem3N  42565  dihmeetlem4preN  42566  dihmeetlem6  42569  dihjatc1  42571  dihmeetlem18N  42584  dih1dimatlem  42589  dihjatcclem1  42678  dihjatcclem2  42679  dihjatcclem4  42681