Theorem lhpbase 40497

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 4275	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2745	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 329	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6826	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 141	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2740	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2740	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 40495	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 499	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 694	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Vcvv 3432  ∅c0 4268   class class class wbr 5079  ‘cfv 6492  Basecbs 17177  1.cp1 18386   ⋖ ccvr 39761  LHypclh 40483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-lhyp 40487

This theorem is referenced by:  lhplt  40499  lhp2lt  40500  lhpexlt  40501  lhp0lt  40502  lhpexle  40504  lhpexnle  40505  lhpexle1  40507  lhpexle2lem  40508  lhpexle3lem  40510  lhpocnle  40515  lhpocat  40516  lhpjat1  40519  lhpjat2  40520  lhpj1  40521  lhpmcvr  40522  lhpmcvr2  40523  lhpmcvr3  40524  lhpmcvr4N  40525  lhpmcvr5N  40526  lhpmcvr6N  40527  lhpm0atN  40528  lhpmat  40529  lhpmatb  40530  lhp2at0  40531  lhpelim  40536  lhpmod2i2  40537  lhpmod6i1  40538  cdlemb2  40540  lhpat  40542  lhpat3  40545  4atexlemwb  40558  ltrnatb  40636  ltrnel  40638  ltrncnvel  40641  trlval2  40662  trlcl  40663  trljat1  40665  trljat2  40666  trlle  40683  trlval3  40686  cdlemc1  40690  cdlemc2  40691  cdlemc4  40693  cdlemc5  40694  cdlemc6  40695  cdlemd2  40698  cdleme0aa  40709  cdleme0b  40711  cdleme0c  40712  cdleme0cp  40713  cdleme0cq  40714  cdleme0e  40716  cdleme0fN  40717  cdlemeulpq  40719  cdleme01N  40720  cdleme0ex1N  40722  cdleme1b  40725  cdleme1  40726  cdleme2  40727  cdleme3b  40728  cdleme3c  40729  cdleme3g  40733  cdleme3h  40734  cdleme3  40736  cdleme4  40737  cdleme4a  40738  cdleme5  40739  cdleme7aa  40741  cdleme7c  40744  cdleme7d  40745  cdleme7e  40746  cdleme7ga  40747  cdleme7  40748  cdleme8  40749  cdleme9b  40751  cdleme9  40752  cdleme10  40753  cdleme11fN  40763  cdleme11g  40764  cdleme11k  40767  cdleme13  40771  cdleme15b  40774  cdleme15d  40776  cdleme15  40777  cdleme16e  40781  cdleme16f  40782  cdleme22gb  40793  cdlemedb  40796  cdlemednpq  40798  cdleme19b  40803  cdleme19c  40804  cdleme20aN  40808  cdleme20c  40810  cdleme20d  40811  cdleme20e  40812  cdleme20j  40817  cdleme21c  40826  cdleme21ct  40828  cdleme22aa  40838  cdleme22cN  40841  cdleme22d  40842  cdleme22e  40843  cdleme22eALTN  40844  cdleme22f  40845  cdleme22g  40847  cdleme23a  40848  cdleme23b  40849  cdleme23c  40850  cdleme28a  40869  cdleme28b  40870  cdleme29ex  40873  cdleme30a  40877  cdlemefr29exN  40901  cdleme32b  40941  cdleme32c  40942  cdleme32e  40944  cdleme35b  40949  cdleme35c  40950  cdleme35d  40951  cdleme35e  40952  cdleme35f  40953  cdleme42a  40970  cdleme42c  40971  cdleme42h  40981  cdleme42i  40982  cdleme48bw  41001  cdlemeg46frv  41024  cdlemeg46vrg  41026  cdlemeg46rgv  41027  cdlemeg46req  41028  cdlemf1  41060  cdlemf2  41061  trlord  41068  cdlemg2fv2  41099  cdlemg2m  41103  cdlemg7fvbwN  41106  cdlemg4  41116  cdlemg6c  41119  cdlemg10bALTN  41135  cdlemg10c  41138  cdlemg10  41140  cdlemg11b  41141  cdlemg12f  41147  cdlemg17a  41160  cdlemg17dALTN  41163  cdlemg19a  41182  cdlemg35  41212  trlcoabs2N  41221  trlcolem  41225  cdlemh2  41315  cdlemi1  41317  cdlemk3  41332  cdlemk4  41333  cdlemk9  41338  cdlemk9bN  41339  cdlemk10  41342  cdlemk39  41415  dia0eldmN  41539  dia1eldmN  41540  dia0  41551  dia1N  41552  diaglbN  41554  diaintclN  41557  dia2dimlem1  41563  dia2dimlem2  41564  dia2dimlem3  41565  dia2dimlem10  41572  dia2dimlem12  41574  cdlemm10N  41617  docaclN  41623  doca2N  41625  djajN  41636  dib0  41663  dibglbN  41665  dibintclN  41666  cdlemn2  41694  cdlemn10  41705  dihjustlem  41715  dihord1  41717  dihord2a  41718  dihord2b  41719  dihord2cN  41720  dihord11b  41721  dihord11c  41723  dihord2pre  41724  dihord2pre2  41725  dihlsscpre  41733  dib2dim  41742  dih2dimb  41743  dih2dimbALTN  41744  dihvalcq2  41746  dihopelvalcpre  41747  dihord6apre  41755  dihord5b  41758  dihord6b  41759  dihord5apre  41761  dih0  41779  dih1  41785  dihwN  41788  dihmeetlem1N  41789  dihglblem5apreN  41790  dihglblem5aN  41791  dihglblem2aN  41792  dihglblem2N  41793  dihglblem3N  41794  dihmeetlem2N  41798  dihglbcpreN  41799  dihmeetbclemN  41803  dihmeetlem3N  41804  dihmeetlem4preN  41805  dihmeetlem6  41808  dihjatc1  41810  dihmeetlem18N  41823  dih1dimatlem  41828  dihjatcclem1  41917  dihjatcclem2  41918  dihjatcclem4  41920