Theorem lhpbase 40718

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 4292	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2766	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6873	. . 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 40716	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 503	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 700	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  Vcvv 3453  ∅c0 4285   class class class wbr 5108  ‘cfv 6536  Basecbs 17268  1.cp1 18477   ⋖ ccvr 39982  LHypclh 40704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  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 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-iota 6492  df-fun 6538  df-fv 6544  df-lhyp 40708

This theorem is referenced by:  lhplt  40720  lhp2lt  40721  lhpexlt  40722  lhp0lt  40723  lhpexle  40725  lhpexnle  40726  lhpexle1  40728  lhpexle2lem  40729  lhpexle3lem  40731  lhpocnle  40736  lhpocat  40737  lhpjat1  40740  lhpjat2  40741  lhpj1  40742  lhpmcvr  40743  lhpmcvr2  40744  lhpmcvr3  40745  lhpmcvr4N  40746  lhpmcvr5N  40747  lhpmcvr6N  40748  lhpm0atN  40749  lhpmat  40750  lhpmatb  40751  lhp2at0  40752  lhpelim  40757  lhpmod2i2  40758  lhpmod6i1  40759  cdlemb2  40761  lhpat  40763  lhpat3  40766  4atexlemwb  40779  ltrnatb  40857  ltrnel  40859  ltrncnvel  40862  trlval2  40883  trlcl  40884  trljat1  40886  trljat2  40887  trlle  40904  trlval3  40907  cdlemc1  40911  cdlemc2  40912  cdlemc4  40914  cdlemc5  40915  cdlemc6  40916  cdlemd2  40919  cdleme0aa  40930  cdleme0b  40932  cdleme0c  40933  cdleme0cp  40934  cdleme0cq  40935  cdleme0e  40937  cdleme0fN  40938  cdlemeulpq  40940  cdleme01N  40941  cdleme0ex1N  40943  cdleme1b  40946  cdleme1  40947  cdleme2  40948  cdleme3b  40949  cdleme3c  40950  cdleme3g  40954  cdleme3h  40955  cdleme3  40957  cdleme4  40958  cdleme4a  40959  cdleme5  40960  cdleme7aa  40962  cdleme7c  40965  cdleme7d  40966  cdleme7e  40967  cdleme7ga  40968  cdleme7  40969  cdleme8  40970  cdleme9b  40972  cdleme9  40973  cdleme10  40974  cdleme11fN  40984  cdleme11g  40985  cdleme11k  40988  cdleme13  40992  cdleme15b  40995  cdleme15d  40997  cdleme15  40998  cdleme16e  41002  cdleme16f  41003  cdleme22gb  41014  cdlemedb  41017  cdlemednpq  41019  cdleme19b  41024  cdleme19c  41025  cdleme20aN  41029  cdleme20c  41031  cdleme20d  41032  cdleme20e  41033  cdleme20j  41038  cdleme21c  41047  cdleme21ct  41049  cdleme22aa  41059  cdleme22cN  41062  cdleme22d  41063  cdleme22e  41064  cdleme22eALTN  41065  cdleme22f  41066  cdleme22g  41068  cdleme23a  41069  cdleme23b  41070  cdleme23c  41071  cdleme28a  41090  cdleme28b  41091  cdleme29ex  41094  cdleme30a  41098  cdlemefr29exN  41122  cdleme32b  41162  cdleme32c  41163  cdleme32e  41165  cdleme35b  41170  cdleme35c  41171  cdleme35d  41172  cdleme35e  41173  cdleme35f  41174  cdleme42a  41191  cdleme42c  41192  cdleme42h  41202  cdleme42i  41203  cdleme48bw  41222  cdlemeg46frv  41245  cdlemeg46vrg  41247  cdlemeg46rgv  41248  cdlemeg46req  41249  cdlemf1  41281  cdlemf2  41282  trlord  41289  cdlemg2fv2  41320  cdlemg2m  41324  cdlemg7fvbwN  41327  cdlemg4  41337  cdlemg6c  41340  cdlemg10bALTN  41356  cdlemg10c  41359  cdlemg10  41361  cdlemg11b  41362  cdlemg12f  41368  cdlemg17a  41381  cdlemg17dALTN  41384  cdlemg19a  41403  cdlemg35  41433  trlcoabs2N  41442  trlcolem  41446  cdlemh2  41536  cdlemi1  41538  cdlemk3  41553  cdlemk4  41554  cdlemk9  41559  cdlemk9bN  41560  cdlemk10  41563  cdlemk39  41636  dia0eldmN  41760  dia1eldmN  41761  dia0  41772  dia1N  41773  diaglbN  41775  diaintclN  41778  dia2dimlem1  41784  dia2dimlem2  41785  dia2dimlem3  41786  dia2dimlem10  41793  dia2dimlem12  41795  cdlemm10N  41838  docaclN  41844  doca2N  41846  djajN  41857  dib0  41884  dibglbN  41886  dibintclN  41887  cdlemn2  41915  cdlemn10  41926  dihjustlem  41936  dihord1  41938  dihord2a  41939  dihord2b  41940  dihord2cN  41941  dihord11b  41942  dihord11c  41944  dihord2pre  41945  dihord2pre2  41946  dihlsscpre  41954  dib2dim  41963  dih2dimb  41964  dih2dimbALTN  41965  dihvalcq2  41967  dihopelvalcpre  41968  dihord6apre  41976  dihord5b  41979  dihord6b  41980  dihord5apre  41982  dih0  42000  dih1  42006  dihwN  42009  dihmeetlem1N  42010  dihglblem5apreN  42011  dihglblem5aN  42012  dihglblem2aN  42013  dihglblem2N  42014  dihglblem3N  42015  dihmeetlem2N  42019  dihglbcpreN  42020  dihmeetbclemN  42024  dihmeetlem3N  42025  dihmeetlem4preN  42026  dihmeetlem6  42029  dihjatc1  42031  dihmeetlem18N  42044  dih1dimatlem  42049  dihjatcclem1  42138  dihjatcclem2  42139  dihjatcclem4  42141