Theorem lhpbase 41023

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 4286	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2766	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6869	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 142	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2761	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2761	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 41021	. . 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 2145  Vcvv 3451  ∅c0 4279   class class class wbr 5103  ‘cfv 6531  Basecbs 17367  1.cp1 18576   ⋖ ccvr 40287  LHypclh 41009

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6487  df-fun 6533  df-fv 6539  df-lhyp 41013

This theorem is used by:  lhplt  41025  lhp2lt  41026  lhpexlt  41027  lhp0lt  41028  lhpexle  41030  lhpexnle  41031  lhpexle1  41033  lhpexle2lem  41034  lhpexle3lem  41036  lhpocnle  41041  lhpocat  41042  lhpjat1  41045  lhpjat2  41046  lhpj1  41047  lhpmcvr  41048  lhpmcvr2  41049  lhpmcvr3  41050  lhpmcvr4N  41051  lhpmcvr5N  41052  lhpmcvr6N  41053  lhpm0atN  41054  lhpmat  41055  lhpmatb  41056  lhp2at0  41057  lhpelim  41062  lhpmod2i2  41063  lhpmod6i1  41064  cdlemb2  41066  lhpat  41068  lhpat3  41071  4atexlemwb  41084  ltrnatb  41162  ltrnel  41164  ltrncnvel  41167  trlval2  41188  trlcl  41189  trljat1  41191  trljat2  41192  trlle  41209  trlval3  41212  cdlemc1  41216  cdlemc2  41217  cdlemc4  41219  cdlemc5  41220  cdlemc6  41221  cdlemd2  41224  cdleme0aa  41235  cdleme0b  41237  cdleme0c  41238  cdleme0cp  41239  cdleme0cq  41240  cdleme0e  41242  cdleme0fN  41243  cdlemeulpq  41245  cdleme01N  41246  cdleme0ex1N  41248  cdleme1b  41251  cdleme1  41252  cdleme2  41253  cdleme3b  41254  cdleme3c  41255  cdleme3g  41259  cdleme3h  41260  cdleme3  41262  cdleme4  41263  cdleme4a  41264  cdleme5  41265  cdleme7aa  41267  cdleme7c  41270  cdleme7d  41271  cdleme7e  41272  cdleme7ga  41273  cdleme7  41274  cdleme8  41275  cdleme9b  41277  cdleme9  41278  cdleme10  41279  cdleme11fN  41289  cdleme11g  41290  cdleme11k  41293  cdleme13  41297  cdleme15b  41300  cdleme15d  41302  cdleme15  41303  cdleme16e  41307  cdleme16f  41308  cdleme22gb  41319  cdlemedb  41322  cdlemednpq  41324  cdleme19b  41329  cdleme19c  41330  cdleme20aN  41334  cdleme20c  41336  cdleme20d  41337  cdleme20e  41338  cdleme20j  41343  cdleme21c  41352  cdleme21ct  41354  cdleme22aa  41364  cdleme22cN  41367  cdleme22d  41368  cdleme22e  41369  cdleme22eALTN  41370  cdleme22f  41371  cdleme22g  41373  cdleme23a  41374  cdleme23b  41375  cdleme23c  41376  cdleme28a  41395  cdleme28b  41396  cdleme29ex  41399  cdleme30a  41403  cdlemefr29exN  41427  cdleme32b  41467  cdleme32c  41468  cdleme32e  41470  cdleme35b  41475  cdleme35c  41476  cdleme35d  41477  cdleme35e  41478  cdleme35f  41479  cdleme42a  41496  cdleme42c  41497  cdleme42h  41507  cdleme42i  41508  cdleme48bw  41527  cdlemeg46frv  41550  cdlemeg46vrg  41552  cdlemeg46rgv  41553  cdlemeg46req  41554  cdlemf1  41586  cdlemf2  41587  trlord  41594  cdlemg2fv2  41625  cdlemg2m  41629  cdlemg7fvbwN  41632  cdlemg4  41642  cdlemg6c  41645  cdlemg10bALTN  41661  cdlemg10c  41664  cdlemg10  41666  cdlemg11b  41667  cdlemg12f  41673  cdlemg17a  41686  cdlemg17dALTN  41689  cdlemg19a  41708  cdlemg35  41738  trlcoabs2N  41747  trlcolem  41751  cdlemh2  41841  cdlemi1  41843  cdlemk3  41858  cdlemk4  41859  cdlemk9  41864  cdlemk9bN  41865  cdlemk10  41868  cdlemk39  41941  dia0eldmN  42065  dia1eldmN  42066  dia0  42077  dia1N  42078  diaglbN  42080  diaintclN  42083  dia2dimlem1  42089  dia2dimlem2  42090  dia2dimlem3  42091  dia2dimlem10  42098  dia2dimlem12  42100  cdlemm10N  42143  docaclN  42149  doca2N  42151  djajN  42162  dib0  42189  dibglbN  42191  dibintclN  42192  cdlemn2  42220  cdlemn10  42231  dihjustlem  42241  dihord1  42243  dihord2a  42244  dihord2b  42245  dihord2cN  42246  dihord11b  42247  dihord11c  42249  dihord2pre  42250  dihord2pre2  42251  dihlsscpre  42259  dib2dim  42268  dih2dimb  42269  dih2dimbALTN  42270  dihvalcq2  42272  dihopelvalcpre  42273  dihord6apre  42281  dihord5b  42284  dihord6b  42285  dihord5apre  42287  dih0  42305  dih1  42311  dihwN  42314  dihmeetlem1N  42315  dihglblem5apreN  42316  dihglblem5aN  42317  dihglblem2aN  42318  dihglblem2N  42319  dihglblem3N  42320  dihmeetlem2N  42324  dihglbcpreN  42325  dihmeetbclemN  42329  dihmeetlem3N  42330  dihmeetlem4preN  42331  dihmeetlem6  42334  dihjatc1  42336  dihmeetlem18N  42349  dih1dimatlem  42354  dihjatcclem1  42443  dihjatcclem2  42444  dihjatcclem4  42446