Theorem lhpbase 39992

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 4303	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2734	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 328	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6850	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 141	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2729	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2729	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 39990	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 498	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 688	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3447  ∅c0 4296   class class class wbr 5107  ‘cfv 6511  Basecbs 17179  1.cp1 18383   ⋖ ccvr 39255  LHypclh 39978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-lhyp 39982

This theorem is referenced by:  lhplt  39994  lhp2lt  39995  lhpexlt  39996  lhp0lt  39997  lhpexle  39999  lhpexnle  40000  lhpexle1  40002  lhpexle2lem  40003  lhpexle3lem  40005  lhpocnle  40010  lhpocat  40011  lhpjat1  40014  lhpjat2  40015  lhpj1  40016  lhpmcvr  40017  lhpmcvr2  40018  lhpmcvr3  40019  lhpmcvr4N  40020  lhpmcvr5N  40021  lhpmcvr6N  40022  lhpm0atN  40023  lhpmat  40024  lhpmatb  40025  lhp2at0  40026  lhpelim  40031  lhpmod2i2  40032  lhpmod6i1  40033  cdlemb2  40035  lhpat  40037  lhpat3  40040  4atexlemwb  40053  ltrnatb  40131  ltrnel  40133  ltrncnvel  40136  trlval2  40157  trlcl  40158  trljat1  40160  trljat2  40161  trlle  40178  trlval3  40181  cdlemc1  40185  cdlemc2  40186  cdlemc4  40188  cdlemc5  40189  cdlemc6  40190  cdlemd2  40193  cdleme0aa  40204  cdleme0b  40206  cdleme0c  40207  cdleme0cp  40208  cdleme0cq  40209  cdleme0e  40211  cdleme0fN  40212  cdlemeulpq  40214  cdleme01N  40215  cdleme0ex1N  40217  cdleme1b  40220  cdleme1  40221  cdleme2  40222  cdleme3b  40223  cdleme3c  40224  cdleme3g  40228  cdleme3h  40229  cdleme3  40231  cdleme4  40232  cdleme4a  40233  cdleme5  40234  cdleme7aa  40236  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme8  40244  cdleme9b  40246  cdleme9  40247  cdleme10  40248  cdleme11fN  40258  cdleme11g  40259  cdleme11k  40262  cdleme13  40266  cdleme15b  40269  cdleme15d  40271  cdleme15  40272  cdleme16e  40276  cdleme16f  40277  cdleme22gb  40288  cdlemedb  40291  cdlemednpq  40293  cdleme19b  40298  cdleme19c  40299  cdleme20aN  40303  cdleme20c  40305  cdleme20d  40306  cdleme20e  40307  cdleme20j  40312  cdleme21c  40321  cdleme21ct  40323  cdleme22aa  40333  cdleme22cN  40336  cdleme22d  40337  cdleme22e  40338  cdleme22eALTN  40339  cdleme22f  40340  cdleme22g  40342  cdleme23a  40343  cdleme23b  40344  cdleme23c  40345  cdleme28a  40364  cdleme28b  40365  cdleme29ex  40368  cdleme30a  40372  cdlemefr29exN  40396  cdleme32b  40436  cdleme32c  40437  cdleme32e  40439  cdleme35b  40444  cdleme35c  40445  cdleme35d  40446  cdleme35e  40447  cdleme35f  40448  cdleme42a  40465  cdleme42c  40466  cdleme42h  40476  cdleme42i  40477  cdleme48bw  40496  cdlemeg46frv  40519  cdlemeg46vrg  40521  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemf1  40555  cdlemf2  40556  trlord  40563  cdlemg2fv2  40594  cdlemg2m  40598  cdlemg7fvbwN  40601  cdlemg4  40611  cdlemg6c  40614  cdlemg10bALTN  40630  cdlemg10c  40633  cdlemg10  40635  cdlemg11b  40636  cdlemg12f  40642  cdlemg17a  40655  cdlemg17dALTN  40658  cdlemg19a  40677  cdlemg35  40707  trlcoabs2N  40716  trlcolem  40720  cdlemh2  40810  cdlemi1  40812  cdlemk3  40827  cdlemk4  40828  cdlemk9  40833  cdlemk9bN  40834  cdlemk10  40837  cdlemk39  40910  dia0eldmN  41034  dia1eldmN  41035  dia0  41046  dia1N  41047  diaglbN  41049  diaintclN  41052  dia2dimlem1  41058  dia2dimlem2  41059  dia2dimlem3  41060  dia2dimlem10  41067  dia2dimlem12  41069  cdlemm10N  41112  docaclN  41118  doca2N  41120  djajN  41131  dib0  41158  dibglbN  41160  dibintclN  41161  cdlemn2  41189  cdlemn10  41200  dihjustlem  41210  dihord1  41212  dihord2a  41213  dihord2b  41214  dihord2cN  41215  dihord11b  41216  dihord11c  41218  dihord2pre  41219  dihord2pre2  41220  dihlsscpre  41228  dib2dim  41237  dih2dimb  41238  dih2dimbALTN  41239  dihvalcq2  41241  dihopelvalcpre  41242  dihord6apre  41250  dihord5b  41253  dihord6b  41254  dihord5apre  41256  dih0  41274  dih1  41280  dihwN  41283  dihmeetlem1N  41284  dihglblem5apreN  41285  dihglblem5aN  41286  dihglblem2aN  41287  dihglblem2N  41288  dihglblem3N  41289  dihmeetlem2N  41293  dihglbcpreN  41294  dihmeetbclemN  41298  dihmeetlem3N  41299  dihmeetlem4preN  41300  dihmeetlem6  41303  dihjatc1  41305  dihmeetlem18N  41318  dih1dimatlem  41323  dihjatcclem1  41412  dihjatcclem2  41413  dihjatcclem4  41415