Theorem lhpbase 40586

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 330	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6855	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 141	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2761	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2761	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 40584	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 502	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 698	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  Vcvv 3453  ∅c0 4285   class class class wbr 5099  ‘cfv 6517  Basecbs 17228  1.cp1 18437   ⋖ ccvr 39850  LHypclh 40572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-iota 6473  df-fun 6519  df-fv 6525  df-lhyp 40576

This theorem is referenced by:  lhplt  40588  lhp2lt  40589  lhpexlt  40590  lhp0lt  40591  lhpexle  40593  lhpexnle  40594  lhpexle1  40596  lhpexle2lem  40597  lhpexle3lem  40599  lhpocnle  40604  lhpocat  40605  lhpjat1  40608  lhpjat2  40609  lhpj1  40610  lhpmcvr  40611  lhpmcvr2  40612  lhpmcvr3  40613  lhpmcvr4N  40614  lhpmcvr5N  40615  lhpmcvr6N  40616  lhpm0atN  40617  lhpmat  40618  lhpmatb  40619  lhp2at0  40620  lhpelim  40625  lhpmod2i2  40626  lhpmod6i1  40627  cdlemb2  40629  lhpat  40631  lhpat3  40634  4atexlemwb  40647  ltrnatb  40725  ltrnel  40727  ltrncnvel  40730  trlval2  40751  trlcl  40752  trljat1  40754  trljat2  40755  trlle  40772  trlval3  40775  cdlemc1  40779  cdlemc2  40780  cdlemc4  40782  cdlemc5  40783  cdlemc6  40784  cdlemd2  40787  cdleme0aa  40798  cdleme0b  40800  cdleme0c  40801  cdleme0cp  40802  cdleme0cq  40803  cdleme0e  40805  cdleme0fN  40806  cdlemeulpq  40808  cdleme01N  40809  cdleme0ex1N  40811  cdleme1b  40814  cdleme1  40815  cdleme2  40816  cdleme3b  40817  cdleme3c  40818  cdleme3g  40822  cdleme3h  40823  cdleme3  40825  cdleme4  40826  cdleme4a  40827  cdleme5  40828  cdleme7aa  40830  cdleme7c  40833  cdleme7d  40834  cdleme7e  40835  cdleme7ga  40836  cdleme7  40837  cdleme8  40838  cdleme9b  40840  cdleme9  40841  cdleme10  40842  cdleme11fN  40852  cdleme11g  40853  cdleme11k  40856  cdleme13  40860  cdleme15b  40863  cdleme15d  40865  cdleme15  40866  cdleme16e  40870  cdleme16f  40871  cdleme22gb  40882  cdlemedb  40885  cdlemednpq  40887  cdleme19b  40892  cdleme19c  40893  cdleme20aN  40897  cdleme20c  40899  cdleme20d  40900  cdleme20e  40901  cdleme20j  40906  cdleme21c  40915  cdleme21ct  40917  cdleme22aa  40927  cdleme22cN  40930  cdleme22d  40931  cdleme22e  40932  cdleme22eALTN  40933  cdleme22f  40934  cdleme22g  40936  cdleme23a  40937  cdleme23b  40938  cdleme23c  40939  cdleme28a  40958  cdleme28b  40959  cdleme29ex  40962  cdleme30a  40966  cdlemefr29exN  40990  cdleme32b  41030  cdleme32c  41031  cdleme32e  41033  cdleme35b  41038  cdleme35c  41039  cdleme35d  41040  cdleme35e  41041  cdleme35f  41042  cdleme42a  41059  cdleme42c  41060  cdleme42h  41070  cdleme42i  41071  cdleme48bw  41090  cdlemeg46frv  41113  cdlemeg46vrg  41115  cdlemeg46rgv  41116  cdlemeg46req  41117  cdlemf1  41149  cdlemf2  41150  trlord  41157  cdlemg2fv2  41188  cdlemg2m  41192  cdlemg7fvbwN  41195  cdlemg4  41205  cdlemg6c  41208  cdlemg10bALTN  41224  cdlemg10c  41227  cdlemg10  41229  cdlemg11b  41230  cdlemg12f  41236  cdlemg17a  41249  cdlemg17dALTN  41252  cdlemg19a  41271  cdlemg35  41301  trlcoabs2N  41310  trlcolem  41314  cdlemh2  41404  cdlemi1  41406  cdlemk3  41421  cdlemk4  41422  cdlemk9  41427  cdlemk9bN  41428  cdlemk10  41431  cdlemk39  41504  dia0eldmN  41628  dia1eldmN  41629  dia0  41640  dia1N  41641  diaglbN  41643  diaintclN  41646  dia2dimlem1  41652  dia2dimlem2  41653  dia2dimlem3  41654  dia2dimlem10  41661  dia2dimlem12  41663  cdlemm10N  41706  docaclN  41712  doca2N  41714  djajN  41725  dib0  41752  dibglbN  41754  dibintclN  41755  cdlemn2  41783  cdlemn10  41794  dihjustlem  41804  dihord1  41806  dihord2a  41807  dihord2b  41808  dihord2cN  41809  dihord11b  41810  dihord11c  41812  dihord2pre  41813  dihord2pre2  41814  dihlsscpre  41822  dib2dim  41831  dih2dimb  41832  dih2dimbALTN  41833  dihvalcq2  41835  dihopelvalcpre  41836  dihord6apre  41844  dihord5b  41847  dihord6b  41848  dihord5apre  41850  dih0  41868  dih1  41874  dihwN  41877  dihmeetlem1N  41878  dihglblem5apreN  41879  dihglblem5aN  41880  dihglblem2aN  41881  dihglblem2N  41882  dihglblem3N  41883  dihmeetlem2N  41887  dihglbcpreN  41888  dihmeetbclemN  41892  dihmeetlem3N  41893  dihmeetlem4preN  41894  dihmeetlem6  41897  dihjatc1  41899  dihmeetlem18N  41912  dih1dimatlem  41917  dihjatcclem1  42006  dihjatcclem2  42007  dihjatcclem4  42009