Theorem lhpbase 40634

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 4295	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2770	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6863	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 142	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2765	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2765	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 40632	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 503	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 700	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  Vcvv 3457  ∅c0 4288   class class class wbr 5105  ‘cfv 6525  Basecbs 17259  1.cp1 18468   ⋖ ccvr 39898  LHypclh 40620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-iota 6481  df-fun 6527  df-fv 6533  df-lhyp 40624

This theorem is referenced by:  lhplt  40636  lhp2lt  40637  lhpexlt  40638  lhp0lt  40639  lhpexle  40641  lhpexnle  40642  lhpexle1  40644  lhpexle2lem  40645  lhpexle3lem  40647  lhpocnle  40652  lhpocat  40653  lhpjat1  40656  lhpjat2  40657  lhpj1  40658  lhpmcvr  40659  lhpmcvr2  40660  lhpmcvr3  40661  lhpmcvr4N  40662  lhpmcvr5N  40663  lhpmcvr6N  40664  lhpm0atN  40665  lhpmat  40666  lhpmatb  40667  lhp2at0  40668  lhpelim  40673  lhpmod2i2  40674  lhpmod6i1  40675  cdlemb2  40677  lhpat  40679  lhpat3  40682  4atexlemwb  40695  ltrnatb  40773  ltrnel  40775  ltrncnvel  40778  trlval2  40799  trlcl  40800  trljat1  40802  trljat2  40803  trlle  40820  trlval3  40823  cdlemc1  40827  cdlemc2  40828  cdlemc4  40830  cdlemc5  40831  cdlemc6  40832  cdlemd2  40835  cdleme0aa  40846  cdleme0b  40848  cdleme0c  40849  cdleme0cp  40850  cdleme0cq  40851  cdleme0e  40853  cdleme0fN  40854  cdlemeulpq  40856  cdleme01N  40857  cdleme0ex1N  40859  cdleme1b  40862  cdleme1  40863  cdleme2  40864  cdleme3b  40865  cdleme3c  40866  cdleme3g  40870  cdleme3h  40871  cdleme3  40873  cdleme4  40874  cdleme4a  40875  cdleme5  40876  cdleme7aa  40878  cdleme7c  40881  cdleme7d  40882  cdleme7e  40883  cdleme7ga  40884  cdleme7  40885  cdleme8  40886  cdleme9b  40888  cdleme9  40889  cdleme10  40890  cdleme11fN  40900  cdleme11g  40901  cdleme11k  40904  cdleme13  40908  cdleme15b  40911  cdleme15d  40913  cdleme15  40914  cdleme16e  40918  cdleme16f  40919  cdleme22gb  40930  cdlemedb  40933  cdlemednpq  40935  cdleme19b  40940  cdleme19c  40941  cdleme20aN  40945  cdleme20c  40947  cdleme20d  40948  cdleme20e  40949  cdleme20j  40954  cdleme21c  40963  cdleme21ct  40965  cdleme22aa  40975  cdleme22cN  40978  cdleme22d  40979  cdleme22e  40980  cdleme22eALTN  40981  cdleme22f  40982  cdleme22g  40984  cdleme23a  40985  cdleme23b  40986  cdleme23c  40987  cdleme28a  41006  cdleme28b  41007  cdleme29ex  41010  cdleme30a  41014  cdlemefr29exN  41038  cdleme32b  41078  cdleme32c  41079  cdleme32e  41081  cdleme35b  41086  cdleme35c  41087  cdleme35d  41088  cdleme35e  41089  cdleme35f  41090  cdleme42a  41107  cdleme42c  41108  cdleme42h  41118  cdleme42i  41119  cdleme48bw  41138  cdlemeg46frv  41161  cdlemeg46vrg  41163  cdlemeg46rgv  41164  cdlemeg46req  41165  cdlemf1  41197  cdlemf2  41198  trlord  41205  cdlemg2fv2  41236  cdlemg2m  41240  cdlemg7fvbwN  41243  cdlemg4  41253  cdlemg6c  41256  cdlemg10bALTN  41272  cdlemg10c  41275  cdlemg10  41277  cdlemg11b  41278  cdlemg12f  41284  cdlemg17a  41297  cdlemg17dALTN  41300  cdlemg19a  41319  cdlemg35  41349  trlcoabs2N  41358  trlcolem  41362  cdlemh2  41452  cdlemi1  41454  cdlemk3  41469  cdlemk4  41470  cdlemk9  41475  cdlemk9bN  41476  cdlemk10  41479  cdlemk39  41552  dia0eldmN  41676  dia1eldmN  41677  dia0  41688  dia1N  41689  diaglbN  41691  diaintclN  41694  dia2dimlem1  41700  dia2dimlem2  41701  dia2dimlem3  41702  dia2dimlem10  41709  dia2dimlem12  41711  cdlemm10N  41754  docaclN  41760  doca2N  41762  djajN  41773  dib0  41800  dibglbN  41802  dibintclN  41803  cdlemn2  41831  cdlemn10  41842  dihjustlem  41852  dihord1  41854  dihord2a  41855  dihord2b  41856  dihord2cN  41857  dihord11b  41858  dihord11c  41860  dihord2pre  41861  dihord2pre2  41862  dihlsscpre  41870  dib2dim  41879  dih2dimb  41880  dih2dimbALTN  41881  dihvalcq2  41883  dihopelvalcpre  41884  dihord6apre  41892  dihord5b  41895  dihord6b  41896  dihord5apre  41898  dih0  41916  dih1  41922  dihwN  41925  dihmeetlem1N  41926  dihglblem5apreN  41927  dihglblem5aN  41928  dihglblem2aN  41929  dihglblem2N  41930  dihglblem3N  41931  dihmeetlem2N  41935  dihglbcpreN  41936  dihmeetbclemN  41940  dihmeetlem3N  41941  dihmeetlem4preN  41942  dihmeetlem6  41945  dihjatc1  41947  dihmeetlem18N  41960  dih1dimatlem  41965  dihjatcclem1  42054  dihjatcclem2  42055  dihjatcclem4  42057