Theorem lhpbase 40103

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 4289	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2736	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 328	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6820	. . 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 40101	. . 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 4282   class class class wbr 5093  ‘cfv 6487  Basecbs 17126  1.cp1 18334   ⋖ ccvr 39367  LHypclh 40089

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 5236  ax-nul 5246  ax-pr 5372

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 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6443  df-fun 6489  df-fv 6495  df-lhyp 40093

This theorem is referenced by:  lhplt  40105  lhp2lt  40106  lhpexlt  40107  lhp0lt  40108  lhpexle  40110  lhpexnle  40111  lhpexle1  40113  lhpexle2lem  40114  lhpexle3lem  40116  lhpocnle  40121  lhpocat  40122  lhpjat1  40125  lhpjat2  40126  lhpj1  40127  lhpmcvr  40128  lhpmcvr2  40129  lhpmcvr3  40130  lhpmcvr4N  40131  lhpmcvr5N  40132  lhpmcvr6N  40133  lhpm0atN  40134  lhpmat  40135  lhpmatb  40136  lhp2at0  40137  lhpelim  40142  lhpmod2i2  40143  lhpmod6i1  40144  cdlemb2  40146  lhpat  40148  lhpat3  40151  4atexlemwb  40164  ltrnatb  40242  ltrnel  40244  ltrncnvel  40247  trlval2  40268  trlcl  40269  trljat1  40271  trljat2  40272  trlle  40289  trlval3  40292  cdlemc1  40296  cdlemc2  40297  cdlemc4  40299  cdlemc5  40300  cdlemc6  40301  cdlemd2  40304  cdleme0aa  40315  cdleme0b  40317  cdleme0c  40318  cdleme0cp  40319  cdleme0cq  40320  cdleme0e  40322  cdleme0fN  40323  cdlemeulpq  40325  cdleme01N  40326  cdleme0ex1N  40328  cdleme1b  40331  cdleme1  40332  cdleme2  40333  cdleme3b  40334  cdleme3c  40335  cdleme3g  40339  cdleme3h  40340  cdleme3  40342  cdleme4  40343  cdleme4a  40344  cdleme5  40345  cdleme7aa  40347  cdleme7c  40350  cdleme7d  40351  cdleme7e  40352  cdleme7ga  40353  cdleme7  40354  cdleme8  40355  cdleme9b  40357  cdleme9  40358  cdleme10  40359  cdleme11fN  40369  cdleme11g  40370  cdleme11k  40373  cdleme13  40377  cdleme15b  40380  cdleme15d  40382  cdleme15  40383  cdleme16e  40387  cdleme16f  40388  cdleme22gb  40399  cdlemedb  40402  cdlemednpq  40404  cdleme19b  40409  cdleme19c  40410  cdleme20aN  40414  cdleme20c  40416  cdleme20d  40417  cdleme20e  40418  cdleme20j  40423  cdleme21c  40432  cdleme21ct  40434  cdleme22aa  40444  cdleme22cN  40447  cdleme22d  40448  cdleme22e  40449  cdleme22eALTN  40450  cdleme22f  40451  cdleme22g  40453  cdleme23a  40454  cdleme23b  40455  cdleme23c  40456  cdleme28a  40475  cdleme28b  40476  cdleme29ex  40479  cdleme30a  40483  cdlemefr29exN  40507  cdleme32b  40547  cdleme32c  40548  cdleme32e  40550  cdleme35b  40555  cdleme35c  40556  cdleme35d  40557  cdleme35e  40558  cdleme35f  40559  cdleme42a  40576  cdleme42c  40577  cdleme42h  40587  cdleme42i  40588  cdleme48bw  40607  cdlemeg46frv  40630  cdlemeg46vrg  40632  cdlemeg46rgv  40633  cdlemeg46req  40634  cdlemf1  40666  cdlemf2  40667  trlord  40674  cdlemg2fv2  40705  cdlemg2m  40709  cdlemg7fvbwN  40712  cdlemg4  40722  cdlemg6c  40725  cdlemg10bALTN  40741  cdlemg10c  40744  cdlemg10  40746  cdlemg11b  40747  cdlemg12f  40753  cdlemg17a  40766  cdlemg17dALTN  40769  cdlemg19a  40788  cdlemg35  40818  trlcoabs2N  40827  trlcolem  40831  cdlemh2  40921  cdlemi1  40923  cdlemk3  40938  cdlemk4  40939  cdlemk9  40944  cdlemk9bN  40945  cdlemk10  40948  cdlemk39  41021  dia0eldmN  41145  dia1eldmN  41146  dia0  41157  dia1N  41158  diaglbN  41160  diaintclN  41163  dia2dimlem1  41169  dia2dimlem2  41170  dia2dimlem3  41171  dia2dimlem10  41178  dia2dimlem12  41180  cdlemm10N  41223  docaclN  41229  doca2N  41231  djajN  41242  dib0  41269  dibglbN  41271  dibintclN  41272  cdlemn2  41300  cdlemn10  41311  dihjustlem  41321  dihord1  41323  dihord2a  41324  dihord2b  41325  dihord2cN  41326  dihord11b  41327  dihord11c  41329  dihord2pre  41330  dihord2pre2  41331  dihlsscpre  41339  dib2dim  41348  dih2dimb  41349  dih2dimbALTN  41350  dihvalcq2  41352  dihopelvalcpre  41353  dihord6apre  41361  dihord5b  41364  dihord6b  41365  dihord5apre  41367  dih0  41385  dih1  41391  dihwN  41394  dihmeetlem1N  41395  dihglblem5apreN  41396  dihglblem5aN  41397  dihglblem2aN  41398  dihglblem2N  41399  dihglblem3N  41400  dihmeetlem2N  41404  dihglbcpreN  41405  dihmeetbclemN  41409  dihmeetlem3N  41410  dihmeetlem4preN  41411  dihmeetlem6  41414  dihjatc1  41416  dihmeetlem18N  41429  dih1dimatlem  41434  dihjatcclem1  41523  dihjatcclem2  41524  dihjatcclem4  41526