Theorem lhpbase 40813

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 4296	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2771	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6880	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 142	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2766	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2766	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 40811	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 504	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 701	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  Vcvv 3458  ∅c0 4289   class class class wbr 5114  ‘cfv 6543  Basecbs 17294  1.cp1 18503   ⋖ ccvr 40077  LHypclh 40799

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6499  df-fun 6545  df-fv 6551  df-lhyp 40803

This theorem is used by:  lhplt  40815  lhp2lt  40816  lhpexlt  40817  lhp0lt  40818  lhpexle  40820  lhpexnle  40821  lhpexle1  40823  lhpexle2lem  40824  lhpexle3lem  40826  lhpocnle  40831  lhpocat  40832  lhpjat1  40835  lhpjat2  40836  lhpj1  40837  lhpmcvr  40838  lhpmcvr2  40839  lhpmcvr3  40840  lhpmcvr4N  40841  lhpmcvr5N  40842  lhpmcvr6N  40843  lhpm0atN  40844  lhpmat  40845  lhpmatb  40846  lhp2at0  40847  lhpelim  40852  lhpmod2i2  40853  lhpmod6i1  40854  cdlemb2  40856  lhpat  40858  lhpat3  40861  4atexlemwb  40874  ltrnatb  40952  ltrnel  40954  ltrncnvel  40957  trlval2  40978  trlcl  40979  trljat1  40981  trljat2  40982  trlle  40999  trlval3  41002  cdlemc1  41006  cdlemc2  41007  cdlemc4  41009  cdlemc5  41010  cdlemc6  41011  cdlemd2  41014  cdleme0aa  41025  cdleme0b  41027  cdleme0c  41028  cdleme0cp  41029  cdleme0cq  41030  cdleme0e  41032  cdleme0fN  41033  cdlemeulpq  41035  cdleme01N  41036  cdleme0ex1N  41038  cdleme1b  41041  cdleme1  41042  cdleme2  41043  cdleme3b  41044  cdleme3c  41045  cdleme3g  41049  cdleme3h  41050  cdleme3  41052  cdleme4  41053  cdleme4a  41054  cdleme5  41055  cdleme7aa  41057  cdleme7c  41060  cdleme7d  41061  cdleme7e  41062  cdleme7ga  41063  cdleme7  41064  cdleme8  41065  cdleme9b  41067  cdleme9  41068  cdleme10  41069  cdleme11fN  41079  cdleme11g  41080  cdleme11k  41083  cdleme13  41087  cdleme15b  41090  cdleme15d  41092  cdleme15  41093  cdleme16e  41097  cdleme16f  41098  cdleme22gb  41109  cdlemedb  41112  cdlemednpq  41114  cdleme19b  41119  cdleme19c  41120  cdleme20aN  41124  cdleme20c  41126  cdleme20d  41127  cdleme20e  41128  cdleme20j  41133  cdleme21c  41142  cdleme21ct  41144  cdleme22aa  41154  cdleme22cN  41157  cdleme22d  41158  cdleme22e  41159  cdleme22eALTN  41160  cdleme22f  41161  cdleme22g  41163  cdleme23a  41164  cdleme23b  41165  cdleme23c  41166  cdleme28a  41185  cdleme28b  41186  cdleme29ex  41189  cdleme30a  41193  cdlemefr29exN  41217  cdleme32b  41257  cdleme32c  41258  cdleme32e  41260  cdleme35b  41265  cdleme35c  41266  cdleme35d  41267  cdleme35e  41268  cdleme35f  41269  cdleme42a  41286  cdleme42c  41287  cdleme42h  41297  cdleme42i  41298  cdleme48bw  41317  cdlemeg46frv  41340  cdlemeg46vrg  41342  cdlemeg46rgv  41343  cdlemeg46req  41344  cdlemf1  41376  cdlemf2  41377  trlord  41384  cdlemg2fv2  41415  cdlemg2m  41419  cdlemg7fvbwN  41422  cdlemg4  41432  cdlemg6c  41435  cdlemg10bALTN  41451  cdlemg10c  41454  cdlemg10  41456  cdlemg11b  41457  cdlemg12f  41463  cdlemg17a  41476  cdlemg17dALTN  41479  cdlemg19a  41498  cdlemg35  41528  trlcoabs2N  41537  trlcolem  41541  cdlemh2  41631  cdlemi1  41633  cdlemk3  41648  cdlemk4  41649  cdlemk9  41654  cdlemk9bN  41655  cdlemk10  41658  cdlemk39  41731  dia0eldmN  41855  dia1eldmN  41856  dia0  41867  dia1N  41868  diaglbN  41870  diaintclN  41873  dia2dimlem1  41879  dia2dimlem2  41880  dia2dimlem3  41881  dia2dimlem10  41888  dia2dimlem12  41890  cdlemm10N  41933  docaclN  41939  doca2N  41941  djajN  41952  dib0  41979  dibglbN  41981  dibintclN  41982  cdlemn2  42010  cdlemn10  42021  dihjustlem  42031  dihord1  42033  dihord2a  42034  dihord2b  42035  dihord2cN  42036  dihord11b  42037  dihord11c  42039  dihord2pre  42040  dihord2pre2  42041  dihlsscpre  42049  dib2dim  42058  dih2dimb  42059  dih2dimbALTN  42060  dihvalcq2  42062  dihopelvalcpre  42063  dihord6apre  42071  dihord5b  42074  dihord6b  42075  dihord5apre  42077  dih0  42095  dih1  42101  dihwN  42104  dihmeetlem1N  42105  dihglblem5apreN  42106  dihglblem5aN  42107  dihglblem2aN  42108  dihglblem2N  42109  dihglblem3N  42110  dihmeetlem2N  42114  dihglbcpreN  42115  dihmeetbclemN  42119  dihmeetlem3N  42120  dihmeetlem4preN  42121  dihmeetlem6  42124  dihjatc1  42126  dihmeetlem18N  42139  dih1dimatlem  42144  dihjatcclem1  42233  dihjatcclem2  42234  dihjatcclem4  42236