Theorem lhpbase 40036

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  Vcvv 3436  ∅c0 4283   class class class wbr 5091  ‘cfv 6481  Basecbs 17117  1.cp1 18325   ⋖ ccvr 39300  LHypclh 40022

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-iota 6437  df-fun 6483  df-fv 6489  df-lhyp 40026

This theorem is referenced by:  lhplt  40038  lhp2lt  40039  lhpexlt  40040  lhp0lt  40041  lhpexle  40043  lhpexnle  40044  lhpexle1  40046  lhpexle2lem  40047  lhpexle3lem  40049  lhpocnle  40054  lhpocat  40055  lhpjat1  40058  lhpjat2  40059  lhpj1  40060  lhpmcvr  40061  lhpmcvr2  40062  lhpmcvr3  40063  lhpmcvr4N  40064  lhpmcvr5N  40065  lhpmcvr6N  40066  lhpm0atN  40067  lhpmat  40068  lhpmatb  40069  lhp2at0  40070  lhpelim  40075  lhpmod2i2  40076  lhpmod6i1  40077  cdlemb2  40079  lhpat  40081  lhpat3  40084  4atexlemwb  40097  ltrnatb  40175  ltrnel  40177  ltrncnvel  40180  trlval2  40201  trlcl  40202  trljat1  40204  trljat2  40205  trlle  40222  trlval3  40225  cdlemc1  40229  cdlemc2  40230  cdlemc4  40232  cdlemc5  40233  cdlemc6  40234  cdlemd2  40237  cdleme0aa  40248  cdleme0b  40250  cdleme0c  40251  cdleme0cp  40252  cdleme0cq  40253  cdleme0e  40255  cdleme0fN  40256  cdlemeulpq  40258  cdleme01N  40259  cdleme0ex1N  40261  cdleme1b  40264  cdleme1  40265  cdleme2  40266  cdleme3b  40267  cdleme3c  40268  cdleme3g  40272  cdleme3h  40273  cdleme3  40275  cdleme4  40276  cdleme4a  40277  cdleme5  40278  cdleme7aa  40280  cdleme7c  40283  cdleme7d  40284  cdleme7e  40285  cdleme7ga  40286  cdleme7  40287  cdleme8  40288  cdleme9b  40290  cdleme9  40291  cdleme10  40292  cdleme11fN  40302  cdleme11g  40303  cdleme11k  40306  cdleme13  40310  cdleme15b  40313  cdleme15d  40315  cdleme15  40316  cdleme16e  40320  cdleme16f  40321  cdleme22gb  40332  cdlemedb  40335  cdlemednpq  40337  cdleme19b  40342  cdleme19c  40343  cdleme20aN  40347  cdleme20c  40349  cdleme20d  40350  cdleme20e  40351  cdleme20j  40356  cdleme21c  40365  cdleme21ct  40367  cdleme22aa  40377  cdleme22cN  40380  cdleme22d  40381  cdleme22e  40382  cdleme22eALTN  40383  cdleme22f  40384  cdleme22g  40386  cdleme23a  40387  cdleme23b  40388  cdleme23c  40389  cdleme28a  40408  cdleme28b  40409  cdleme29ex  40412  cdleme30a  40416  cdlemefr29exN  40440  cdleme32b  40480  cdleme32c  40481  cdleme32e  40483  cdleme35b  40488  cdleme35c  40489  cdleme35d  40490  cdleme35e  40491  cdleme35f  40492  cdleme42a  40509  cdleme42c  40510  cdleme42h  40520  cdleme42i  40521  cdleme48bw  40540  cdlemeg46frv  40563  cdlemeg46vrg  40565  cdlemeg46rgv  40566  cdlemeg46req  40567  cdlemf1  40599  cdlemf2  40600  trlord  40607  cdlemg2fv2  40638  cdlemg2m  40642  cdlemg7fvbwN  40645  cdlemg4  40655  cdlemg6c  40658  cdlemg10bALTN  40674  cdlemg10c  40677  cdlemg10  40679  cdlemg11b  40680  cdlemg12f  40686  cdlemg17a  40699  cdlemg17dALTN  40702  cdlemg19a  40721  cdlemg35  40751  trlcoabs2N  40760  trlcolem  40764  cdlemh2  40854  cdlemi1  40856  cdlemk3  40871  cdlemk4  40872  cdlemk9  40877  cdlemk9bN  40878  cdlemk10  40881  cdlemk39  40954  dia0eldmN  41078  dia1eldmN  41079  dia0  41090  dia1N  41091  diaglbN  41093  diaintclN  41096  dia2dimlem1  41102  dia2dimlem2  41103  dia2dimlem3  41104  dia2dimlem10  41111  dia2dimlem12  41113  cdlemm10N  41156  docaclN  41162  doca2N  41164  djajN  41175  dib0  41202  dibglbN  41204  dibintclN  41205  cdlemn2  41233  cdlemn10  41244  dihjustlem  41254  dihord1  41256  dihord2a  41257  dihord2b  41258  dihord2cN  41259  dihord11b  41260  dihord11c  41262  dihord2pre  41263  dihord2pre2  41264  dihlsscpre  41272  dib2dim  41281  dih2dimb  41282  dih2dimbALTN  41283  dihvalcq2  41285  dihopelvalcpre  41286  dihord6apre  41294  dihord5b  41297  dihord6b  41298  dihord5apre  41300  dih0  41318  dih1  41324  dihwN  41327  dihmeetlem1N  41328  dihglblem5apreN  41329  dihglblem5aN  41330  dihglblem2aN  41331  dihglblem2N  41332  dihglblem3N  41333  dihmeetlem2N  41337  dihglbcpreN  41338  dihmeetbclemN  41342  dihmeetlem3N  41343  dihmeetlem4preN  41344  dihmeetlem6  41347  dihjatc1  41349  dihmeetlem18N  41362  dih1dimatlem  41367  dihjatcclem1  41456  dihjatcclem2  41457  dihjatcclem4  41459