Theorem lhpbase 39999

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3450  ∅c0 4299   class class class wbr 5110  ‘cfv 6514  Basecbs 17186  1.cp1 18390   ⋖ ccvr 39262  LHypclh 39985

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-lhyp 39989

This theorem is referenced by:  lhplt  40001  lhp2lt  40002  lhpexlt  40003  lhp0lt  40004  lhpexle  40006  lhpexnle  40007  lhpexle1  40009  lhpexle2lem  40010  lhpexle3lem  40012  lhpocnle  40017  lhpocat  40018  lhpjat1  40021  lhpjat2  40022  lhpj1  40023  lhpmcvr  40024  lhpmcvr2  40025  lhpmcvr3  40026  lhpmcvr4N  40027  lhpmcvr5N  40028  lhpmcvr6N  40029  lhpm0atN  40030  lhpmat  40031  lhpmatb  40032  lhp2at0  40033  lhpelim  40038  lhpmod2i2  40039  lhpmod6i1  40040  cdlemb2  40042  lhpat  40044  lhpat3  40047  4atexlemwb  40060  ltrnatb  40138  ltrnel  40140  ltrncnvel  40143  trlval2  40164  trlcl  40165  trljat1  40167  trljat2  40168  trlle  40185  trlval3  40188  cdlemc1  40192  cdlemc2  40193  cdlemc4  40195  cdlemc5  40196  cdlemc6  40197  cdlemd2  40200  cdleme0aa  40211  cdleme0b  40213  cdleme0c  40214  cdleme0cp  40215  cdleme0cq  40216  cdleme0e  40218  cdleme0fN  40219  cdlemeulpq  40221  cdleme01N  40222  cdleme0ex1N  40224  cdleme1b  40227  cdleme1  40228  cdleme2  40229  cdleme3b  40230  cdleme3c  40231  cdleme3g  40235  cdleme3h  40236  cdleme3  40238  cdleme4  40239  cdleme4a  40240  cdleme5  40241  cdleme7aa  40243  cdleme7c  40246  cdleme7d  40247  cdleme7e  40248  cdleme7ga  40249  cdleme7  40250  cdleme8  40251  cdleme9b  40253  cdleme9  40254  cdleme10  40255  cdleme11fN  40265  cdleme11g  40266  cdleme11k  40269  cdleme13  40273  cdleme15b  40276  cdleme15d  40278  cdleme15  40279  cdleme16e  40283  cdleme16f  40284  cdleme22gb  40295  cdlemedb  40298  cdlemednpq  40300  cdleme19b  40305  cdleme19c  40306  cdleme20aN  40310  cdleme20c  40312  cdleme20d  40313  cdleme20e  40314  cdleme20j  40319  cdleme21c  40328  cdleme21ct  40330  cdleme22aa  40340  cdleme22cN  40343  cdleme22d  40344  cdleme22e  40345  cdleme22eALTN  40346  cdleme22f  40347  cdleme22g  40349  cdleme23a  40350  cdleme23b  40351  cdleme23c  40352  cdleme28a  40371  cdleme28b  40372  cdleme29ex  40375  cdleme30a  40379  cdlemefr29exN  40403  cdleme32b  40443  cdleme32c  40444  cdleme32e  40446  cdleme35b  40451  cdleme35c  40452  cdleme35d  40453  cdleme35e  40454  cdleme35f  40455  cdleme42a  40472  cdleme42c  40473  cdleme42h  40483  cdleme42i  40484  cdleme48bw  40503  cdlemeg46frv  40526  cdlemeg46vrg  40528  cdlemeg46rgv  40529  cdlemeg46req  40530  cdlemf1  40562  cdlemf2  40563  trlord  40570  cdlemg2fv2  40601  cdlemg2m  40605  cdlemg7fvbwN  40608  cdlemg4  40618  cdlemg6c  40621  cdlemg10bALTN  40637  cdlemg10c  40640  cdlemg10  40642  cdlemg11b  40643  cdlemg12f  40649  cdlemg17a  40662  cdlemg17dALTN  40665  cdlemg19a  40684  cdlemg35  40714  trlcoabs2N  40723  trlcolem  40727  cdlemh2  40817  cdlemi1  40819  cdlemk3  40834  cdlemk4  40835  cdlemk9  40840  cdlemk9bN  40841  cdlemk10  40844  cdlemk39  40917  dia0eldmN  41041  dia1eldmN  41042  dia0  41053  dia1N  41054  diaglbN  41056  diaintclN  41059  dia2dimlem1  41065  dia2dimlem2  41066  dia2dimlem3  41067  dia2dimlem10  41074  dia2dimlem12  41076  cdlemm10N  41119  docaclN  41125  doca2N  41127  djajN  41138  dib0  41165  dibglbN  41167  dibintclN  41168  cdlemn2  41196  cdlemn10  41207  dihjustlem  41217  dihord1  41219  dihord2a  41220  dihord2b  41221  dihord2cN  41222  dihord11b  41223  dihord11c  41225  dihord2pre  41226  dihord2pre2  41227  dihlsscpre  41235  dib2dim  41244  dih2dimb  41245  dih2dimbALTN  41246  dihvalcq2  41248  dihopelvalcpre  41249  dihord6apre  41257  dihord5b  41260  dihord6b  41261  dihord5apre  41263  dih0  41281  dih1  41287  dihwN  41290  dihmeetlem1N  41291  dihglblem5apreN  41292  dihglblem5aN  41293  dihglblem2aN  41294  dihglblem2N  41295  dihglblem3N  41296  dihmeetlem2N  41300  dihglbcpreN  41301  dihmeetbclemN  41305  dihmeetlem3N  41306  dihmeetlem4preN  41307  dihmeetlem6  41310  dihjatc1  41312  dihmeetlem18N  41325  dih1dimatlem  41330  dihjatcclem1  41419  dihjatcclem2  41420  dihjatcclem4  41422