Theorem lhpbase 36684

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 4219	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2800	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 329	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6531	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 143	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2795	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2795	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 36682	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 499	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 684	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1522   ∈ wcel 2081  Vcvv 3437  ∅c0 4211   class class class wbr 4962  ‘cfv 6225  Basecbs 16312  1.cp1 17477   ⋖ ccvr 35948  LHypclh 36670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-iota 6189  df-fun 6227  df-fv 6233  df-lhyp 36674

This theorem is referenced by:  lhplt  36686  lhp2lt  36687  lhpexlt  36688  lhp0lt  36689  lhpexle  36691  lhpexnle  36692  lhpexle1  36694  lhpexle2lem  36695  lhpexle3lem  36697  lhpocnle  36702  lhpocat  36703  lhpjat1  36706  lhpjat2  36707  lhpj1  36708  lhpmcvr  36709  lhpmcvr2  36710  lhpmcvr3  36711  lhpmcvr4N  36712  lhpmcvr5N  36713  lhpmcvr6N  36714  lhpm0atN  36715  lhpmat  36716  lhpmatb  36717  lhp2at0  36718  lhpelim  36723  lhpmod2i2  36724  lhpmod6i1  36725  cdlemb2  36727  lhpat  36729  lhpat3  36732  4atexlemwb  36745  ltrnatb  36823  ltrnel  36825  ltrncnvel  36828  trlval2  36849  trlcl  36850  trljat1  36852  trljat2  36853  trlle  36870  trlval3  36873  cdlemc1  36877  cdlemc2  36878  cdlemc4  36880  cdlemc5  36881  cdlemc6  36882  cdlemd2  36885  cdleme0aa  36896  cdleme0b  36898  cdleme0c  36899  cdleme0cp  36900  cdleme0cq  36901  cdleme0e  36903  cdleme0fN  36904  cdlemeulpq  36906  cdleme01N  36907  cdleme0ex1N  36909  cdleme1b  36912  cdleme1  36913  cdleme2  36914  cdleme3b  36915  cdleme3c  36916  cdleme3g  36920  cdleme3h  36921  cdleme3  36923  cdleme4  36924  cdleme4a  36925  cdleme5  36926  cdleme7aa  36928  cdleme7c  36931  cdleme7d  36932  cdleme7e  36933  cdleme7ga  36934  cdleme7  36935  cdleme8  36936  cdleme9b  36938  cdleme9  36939  cdleme10  36940  cdleme11fN  36950  cdleme11g  36951  cdleme11k  36954  cdleme13  36958  cdleme15b  36961  cdleme15d  36963  cdleme15  36964  cdleme16e  36968  cdleme16f  36969  cdleme22gb  36980  cdlemedb  36983  cdlemednpq  36985  cdleme19b  36990  cdleme19c  36991  cdleme20aN  36995  cdleme20c  36997  cdleme20d  36998  cdleme20e  36999  cdleme20j  37004  cdleme21c  37013  cdleme21ct  37015  cdleme22aa  37025  cdleme22cN  37028  cdleme22d  37029  cdleme22e  37030  cdleme22eALTN  37031  cdleme22f  37032  cdleme22g  37034  cdleme23a  37035  cdleme23b  37036  cdleme23c  37037  cdleme28a  37056  cdleme28b  37057  cdleme29ex  37060  cdleme30a  37064  cdlemefr29exN  37088  cdleme32b  37128  cdleme32c  37129  cdleme32e  37131  cdleme35b  37136  cdleme35c  37137  cdleme35d  37138  cdleme35e  37139  cdleme35f  37140  cdleme42a  37157  cdleme42c  37158  cdleme42h  37168  cdleme42i  37169  cdleme48bw  37188  cdlemeg46frv  37211  cdlemeg46vrg  37213  cdlemeg46rgv  37214  cdlemeg46req  37215  cdlemf1  37247  cdlemf2  37248  trlord  37255  cdlemg2fv2  37286  cdlemg2m  37290  cdlemg7fvbwN  37293  cdlemg4  37303  cdlemg6c  37306  cdlemg10bALTN  37322  cdlemg10c  37325  cdlemg10  37327  cdlemg11b  37328  cdlemg12f  37334  cdlemg17a  37347  cdlemg17dALTN  37350  cdlemg19a  37369  cdlemg35  37399  trlcoabs2N  37408  trlcolem  37412  cdlemh2  37502  cdlemi1  37504  cdlemk3  37519  cdlemk4  37520  cdlemk9  37525  cdlemk9bN  37526  cdlemk10  37529  cdlemk39  37602  dia0eldmN  37726  dia1eldmN  37727  dia0  37738  dia1N  37739  diaglbN  37741  diaintclN  37744  dia2dimlem1  37750  dia2dimlem2  37751  dia2dimlem3  37752  dia2dimlem10  37759  dia2dimlem12  37761  cdlemm10N  37804  docaclN  37810  doca2N  37812  djajN  37823  dib0  37850  dibglbN  37852  dibintclN  37853  cdlemn2  37881  cdlemn10  37892  dihjustlem  37902  dihord1  37904  dihord2a  37905  dihord2b  37906  dihord2cN  37907  dihord11b  37908  dihord11c  37910  dihord2pre  37911  dihord2pre2  37912  dihlsscpre  37920  dib2dim  37929  dih2dimb  37930  dih2dimbALTN  37931  dihvalcq2  37933  dihopelvalcpre  37934  dihord6apre  37942  dihord5b  37945  dihord6b  37946  dihord5apre  37948  dih0  37966  dih1  37972  dihwN  37975  dihmeetlem1N  37976  dihglblem5apreN  37977  dihglblem5aN  37978  dihglblem2aN  37979  dihglblem2N  37980  dihglblem3N  37981  dihmeetlem2N  37985  dihglbcpreN  37986  dihmeetbclemN  37990  dihmeetlem3N  37991  dihmeetlem4preN  37992  dihmeetlem6  37995  dihjatc1  37997  dihmeetlem18N  38010  dih1dimatlem  38015  dihjatcclem1  38104  dihjatcclem2  38105  dihjatcclem4  38107