Theorem lhpbase 37149

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 4299	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2826	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 330	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6663	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 143	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2821	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2821	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 37147	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 501	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 686	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  Vcvv 3494  ∅c0 4291   class class class wbr 5066  ‘cfv 6355  Basecbs 16483  1.cp1 17648   ⋖ ccvr 36413  LHypclh 37135

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-iota 6314  df-fun 6357  df-fv 6363  df-lhyp 37139

This theorem is referenced by:  lhplt  37151  lhp2lt  37152  lhpexlt  37153  lhp0lt  37154  lhpexle  37156  lhpexnle  37157  lhpexle1  37159  lhpexle2lem  37160  lhpexle3lem  37162  lhpocnle  37167  lhpocat  37168  lhpjat1  37171  lhpjat2  37172  lhpj1  37173  lhpmcvr  37174  lhpmcvr2  37175  lhpmcvr3  37176  lhpmcvr4N  37177  lhpmcvr5N  37178  lhpmcvr6N  37179  lhpm0atN  37180  lhpmat  37181  lhpmatb  37182  lhp2at0  37183  lhpelim  37188  lhpmod2i2  37189  lhpmod6i1  37190  cdlemb2  37192  lhpat  37194  lhpat3  37197  4atexlemwb  37210  ltrnatb  37288  ltrnel  37290  ltrncnvel  37293  trlval2  37314  trlcl  37315  trljat1  37317  trljat2  37318  trlle  37335  trlval3  37338  cdlemc1  37342  cdlemc2  37343  cdlemc4  37345  cdlemc5  37346  cdlemc6  37347  cdlemd2  37350  cdleme0aa  37361  cdleme0b  37363  cdleme0c  37364  cdleme0cp  37365  cdleme0cq  37366  cdleme0e  37368  cdleme0fN  37369  cdlemeulpq  37371  cdleme01N  37372  cdleme0ex1N  37374  cdleme1b  37377  cdleme1  37378  cdleme2  37379  cdleme3b  37380  cdleme3c  37381  cdleme3g  37385  cdleme3h  37386  cdleme3  37388  cdleme4  37389  cdleme4a  37390  cdleme5  37391  cdleme7aa  37393  cdleme7c  37396  cdleme7d  37397  cdleme7e  37398  cdleme7ga  37399  cdleme7  37400  cdleme8  37401  cdleme9b  37403  cdleme9  37404  cdleme10  37405  cdleme11fN  37415  cdleme11g  37416  cdleme11k  37419  cdleme13  37423  cdleme15b  37426  cdleme15d  37428  cdleme15  37429  cdleme16e  37433  cdleme16f  37434  cdleme22gb  37445  cdlemedb  37448  cdlemednpq  37450  cdleme19b  37455  cdleme19c  37456  cdleme20aN  37460  cdleme20c  37462  cdleme20d  37463  cdleme20e  37464  cdleme20j  37469  cdleme21c  37478  cdleme21ct  37480  cdleme22aa  37490  cdleme22cN  37493  cdleme22d  37494  cdleme22e  37495  cdleme22eALTN  37496  cdleme22f  37497  cdleme22g  37499  cdleme23a  37500  cdleme23b  37501  cdleme23c  37502  cdleme28a  37521  cdleme28b  37522  cdleme29ex  37525  cdleme30a  37529  cdlemefr29exN  37553  cdleme32b  37593  cdleme32c  37594  cdleme32e  37596  cdleme35b  37601  cdleme35c  37602  cdleme35d  37603  cdleme35e  37604  cdleme35f  37605  cdleme42a  37622  cdleme42c  37623  cdleme42h  37633  cdleme42i  37634  cdleme48bw  37653  cdlemeg46frv  37676  cdlemeg46vrg  37678  cdlemeg46rgv  37679  cdlemeg46req  37680  cdlemf1  37712  cdlemf2  37713  trlord  37720  cdlemg2fv2  37751  cdlemg2m  37755  cdlemg7fvbwN  37758  cdlemg4  37768  cdlemg6c  37771  cdlemg10bALTN  37787  cdlemg10c  37790  cdlemg10  37792  cdlemg11b  37793  cdlemg12f  37799  cdlemg17a  37812  cdlemg17dALTN  37815  cdlemg19a  37834  cdlemg35  37864  trlcoabs2N  37873  trlcolem  37877  cdlemh2  37967  cdlemi1  37969  cdlemk3  37984  cdlemk4  37985  cdlemk9  37990  cdlemk9bN  37991  cdlemk10  37994  cdlemk39  38067  dia0eldmN  38191  dia1eldmN  38192  dia0  38203  dia1N  38204  diaglbN  38206  diaintclN  38209  dia2dimlem1  38215  dia2dimlem2  38216  dia2dimlem3  38217  dia2dimlem10  38224  dia2dimlem12  38226  cdlemm10N  38269  docaclN  38275  doca2N  38277  djajN  38288  dib0  38315  dibglbN  38317  dibintclN  38318  cdlemn2  38346  cdlemn10  38357  dihjustlem  38367  dihord1  38369  dihord2a  38370  dihord2b  38371  dihord2cN  38372  dihord11b  38373  dihord11c  38375  dihord2pre  38376  dihord2pre2  38377  dihlsscpre  38385  dib2dim  38394  dih2dimb  38395  dih2dimbALTN  38396  dihvalcq2  38398  dihopelvalcpre  38399  dihord6apre  38407  dihord5b  38410  dihord6b  38411  dihord5apre  38413  dih0  38431  dih1  38437  dihwN  38440  dihmeetlem1N  38441  dihglblem5apreN  38442  dihglblem5aN  38443  dihglblem2aN  38444  dihglblem2N  38445  dihglblem3N  38446  dihmeetlem2N  38450  dihglbcpreN  38451  dihmeetbclemN  38455  dihmeetlem3N  38456  dihmeetlem4preN  38457  dihmeetlem6  38460  dihjatc1  38462  dihmeetlem18N  38475  dih1dimatlem  38480  dihjatcclem1  38569  dihjatcclem2  38570  dihjatcclem4  38572