Theorem lhpbase 38869

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 4334	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2738	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 328	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6884	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 141	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2733	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2733	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 38867	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 500	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 687	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  Vcvv 3475  ∅c0 4323   class class class wbr 5149  ‘cfv 6544  Basecbs 17144  1.cp1 18377   ⋖ ccvr 38132  LHypclh 38855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-iota 6496  df-fun 6546  df-fv 6552  df-lhyp 38859

This theorem is referenced by:  lhplt  38871  lhp2lt  38872  lhpexlt  38873  lhp0lt  38874  lhpexle  38876  lhpexnle  38877  lhpexle1  38879  lhpexle2lem  38880  lhpexle3lem  38882  lhpocnle  38887  lhpocat  38888  lhpjat1  38891  lhpjat2  38892  lhpj1  38893  lhpmcvr  38894  lhpmcvr2  38895  lhpmcvr3  38896  lhpmcvr4N  38897  lhpmcvr5N  38898  lhpmcvr6N  38899  lhpm0atN  38900  lhpmat  38901  lhpmatb  38902  lhp2at0  38903  lhpelim  38908  lhpmod2i2  38909  lhpmod6i1  38910  cdlemb2  38912  lhpat  38914  lhpat3  38917  4atexlemwb  38930  ltrnatb  39008  ltrnel  39010  ltrncnvel  39013  trlval2  39034  trlcl  39035  trljat1  39037  trljat2  39038  trlle  39055  trlval3  39058  cdlemc1  39062  cdlemc2  39063  cdlemc4  39065  cdlemc5  39066  cdlemc6  39067  cdlemd2  39070  cdleme0aa  39081  cdleme0b  39083  cdleme0c  39084  cdleme0cp  39085  cdleme0cq  39086  cdleme0e  39088  cdleme0fN  39089  cdlemeulpq  39091  cdleme01N  39092  cdleme0ex1N  39094  cdleme1b  39097  cdleme1  39098  cdleme2  39099  cdleme3b  39100  cdleme3c  39101  cdleme3g  39105  cdleme3h  39106  cdleme3  39108  cdleme4  39109  cdleme4a  39110  cdleme5  39111  cdleme7aa  39113  cdleme7c  39116  cdleme7d  39117  cdleme7e  39118  cdleme7ga  39119  cdleme7  39120  cdleme8  39121  cdleme9b  39123  cdleme9  39124  cdleme10  39125  cdleme11fN  39135  cdleme11g  39136  cdleme11k  39139  cdleme13  39143  cdleme15b  39146  cdleme15d  39148  cdleme15  39149  cdleme16e  39153  cdleme16f  39154  cdleme22gb  39165  cdlemedb  39168  cdlemednpq  39170  cdleme19b  39175  cdleme19c  39176  cdleme20aN  39180  cdleme20c  39182  cdleme20d  39183  cdleme20e  39184  cdleme20j  39189  cdleme21c  39198  cdleme21ct  39200  cdleme22aa  39210  cdleme22cN  39213  cdleme22d  39214  cdleme22e  39215  cdleme22eALTN  39216  cdleme22f  39217  cdleme22g  39219  cdleme23a  39220  cdleme23b  39221  cdleme23c  39222  cdleme28a  39241  cdleme28b  39242  cdleme29ex  39245  cdleme30a  39249  cdlemefr29exN  39273  cdleme32b  39313  cdleme32c  39314  cdleme32e  39316  cdleme35b  39321  cdleme35c  39322  cdleme35d  39323  cdleme35e  39324  cdleme35f  39325  cdleme42a  39342  cdleme42c  39343  cdleme42h  39353  cdleme42i  39354  cdleme48bw  39373  cdlemeg46frv  39396  cdlemeg46vrg  39398  cdlemeg46rgv  39399  cdlemeg46req  39400  cdlemf1  39432  cdlemf2  39433  trlord  39440  cdlemg2fv2  39471  cdlemg2m  39475  cdlemg7fvbwN  39478  cdlemg4  39488  cdlemg6c  39491  cdlemg10bALTN  39507  cdlemg10c  39510  cdlemg10  39512  cdlemg11b  39513  cdlemg12f  39519  cdlemg17a  39532  cdlemg17dALTN  39535  cdlemg19a  39554  cdlemg35  39584  trlcoabs2N  39593  trlcolem  39597  cdlemh2  39687  cdlemi1  39689  cdlemk3  39704  cdlemk4  39705  cdlemk9  39710  cdlemk9bN  39711  cdlemk10  39714  cdlemk39  39787  dia0eldmN  39911  dia1eldmN  39912  dia0  39923  dia1N  39924  diaglbN  39926  diaintclN  39929  dia2dimlem1  39935  dia2dimlem2  39936  dia2dimlem3  39937  dia2dimlem10  39944  dia2dimlem12  39946  cdlemm10N  39989  docaclN  39995  doca2N  39997  djajN  40008  dib0  40035  dibglbN  40037  dibintclN  40038  cdlemn2  40066  cdlemn10  40077  dihjustlem  40087  dihord1  40089  dihord2a  40090  dihord2b  40091  dihord2cN  40092  dihord11b  40093  dihord11c  40095  dihord2pre  40096  dihord2pre2  40097  dihlsscpre  40105  dib2dim  40114  dih2dimb  40115  dih2dimbALTN  40116  dihvalcq2  40118  dihopelvalcpre  40119  dihord6apre  40127  dihord5b  40130  dihord6b  40131  dihord5apre  40133  dih0  40151  dih1  40157  dihwN  40160  dihmeetlem1N  40161  dihglblem5apreN  40162  dihglblem5aN  40163  dihglblem2aN  40164  dihglblem2N  40165  dihglblem3N  40166  dihmeetlem2N  40170  dihglbcpreN  40171  dihmeetbclemN  40175  dihmeetlem3N  40176  dihmeetlem4preN  40177  dihmeetlem6  40180  dihjatc1  40182  dihmeetlem18N  40195  dih1dimatlem  40200  dihjatcclem1  40289  dihjatcclem2  40290  dihjatcclem4  40292