Theorem lhpbase 39977

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3438  ∅c0 4286   class class class wbr 5095  ‘cfv 6486  Basecbs 17138  1.cp1 18346   ⋖ ccvr 39240  LHypclh 39963

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 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494  df-lhyp 39967

This theorem is referenced by:  lhplt  39979  lhp2lt  39980  lhpexlt  39981  lhp0lt  39982  lhpexle  39984  lhpexnle  39985  lhpexle1  39987  lhpexle2lem  39988  lhpexle3lem  39990  lhpocnle  39995  lhpocat  39996  lhpjat1  39999  lhpjat2  40000  lhpj1  40001  lhpmcvr  40002  lhpmcvr2  40003  lhpmcvr3  40004  lhpmcvr4N  40005  lhpmcvr5N  40006  lhpmcvr6N  40007  lhpm0atN  40008  lhpmat  40009  lhpmatb  40010  lhp2at0  40011  lhpelim  40016  lhpmod2i2  40017  lhpmod6i1  40018  cdlemb2  40020  lhpat  40022  lhpat3  40025  4atexlemwb  40038  ltrnatb  40116  ltrnel  40118  ltrncnvel  40121  trlval2  40142  trlcl  40143  trljat1  40145  trljat2  40146  trlle  40163  trlval3  40166  cdlemc1  40170  cdlemc2  40171  cdlemc4  40173  cdlemc5  40174  cdlemc6  40175  cdlemd2  40178  cdleme0aa  40189  cdleme0b  40191  cdleme0c  40192  cdleme0cp  40193  cdleme0cq  40194  cdleme0e  40196  cdleme0fN  40197  cdlemeulpq  40199  cdleme01N  40200  cdleme0ex1N  40202  cdleme1b  40205  cdleme1  40206  cdleme2  40207  cdleme3b  40208  cdleme3c  40209  cdleme3g  40213  cdleme3h  40214  cdleme3  40216  cdleme4  40217  cdleme4a  40218  cdleme5  40219  cdleme7aa  40221  cdleme7c  40224  cdleme7d  40225  cdleme7e  40226  cdleme7ga  40227  cdleme7  40228  cdleme8  40229  cdleme9b  40231  cdleme9  40232  cdleme10  40233  cdleme11fN  40243  cdleme11g  40244  cdleme11k  40247  cdleme13  40251  cdleme15b  40254  cdleme15d  40256  cdleme15  40257  cdleme16e  40261  cdleme16f  40262  cdleme22gb  40273  cdlemedb  40276  cdlemednpq  40278  cdleme19b  40283  cdleme19c  40284  cdleme20aN  40288  cdleme20c  40290  cdleme20d  40291  cdleme20e  40292  cdleme20j  40297  cdleme21c  40306  cdleme21ct  40308  cdleme22aa  40318  cdleme22cN  40321  cdleme22d  40322  cdleme22e  40323  cdleme22eALTN  40324  cdleme22f  40325  cdleme22g  40327  cdleme23a  40328  cdleme23b  40329  cdleme23c  40330  cdleme28a  40349  cdleme28b  40350  cdleme29ex  40353  cdleme30a  40357  cdlemefr29exN  40381  cdleme32b  40421  cdleme32c  40422  cdleme32e  40424  cdleme35b  40429  cdleme35c  40430  cdleme35d  40431  cdleme35e  40432  cdleme35f  40433  cdleme42a  40450  cdleme42c  40451  cdleme42h  40461  cdleme42i  40462  cdleme48bw  40481  cdlemeg46frv  40504  cdlemeg46vrg  40506  cdlemeg46rgv  40507  cdlemeg46req  40508  cdlemf1  40540  cdlemf2  40541  trlord  40548  cdlemg2fv2  40579  cdlemg2m  40583  cdlemg7fvbwN  40586  cdlemg4  40596  cdlemg6c  40599  cdlemg10bALTN  40615  cdlemg10c  40618  cdlemg10  40620  cdlemg11b  40621  cdlemg12f  40627  cdlemg17a  40640  cdlemg17dALTN  40643  cdlemg19a  40662  cdlemg35  40692  trlcoabs2N  40701  trlcolem  40705  cdlemh2  40795  cdlemi1  40797  cdlemk3  40812  cdlemk4  40813  cdlemk9  40818  cdlemk9bN  40819  cdlemk10  40822  cdlemk39  40895  dia0eldmN  41019  dia1eldmN  41020  dia0  41031  dia1N  41032  diaglbN  41034  diaintclN  41037  dia2dimlem1  41043  dia2dimlem2  41044  dia2dimlem3  41045  dia2dimlem10  41052  dia2dimlem12  41054  cdlemm10N  41097  docaclN  41103  doca2N  41105  djajN  41116  dib0  41143  dibglbN  41145  dibintclN  41146  cdlemn2  41174  cdlemn10  41185  dihjustlem  41195  dihord1  41197  dihord2a  41198  dihord2b  41199  dihord2cN  41200  dihord11b  41201  dihord11c  41203  dihord2pre  41204  dihord2pre2  41205  dihlsscpre  41213  dib2dim  41222  dih2dimb  41223  dih2dimbALTN  41224  dihvalcq2  41226  dihopelvalcpre  41227  dihord6apre  41235  dihord5b  41238  dihord6b  41239  dihord5apre  41241  dih0  41259  dih1  41265  dihwN  41268  dihmeetlem1N  41269  dihglblem5apreN  41270  dihglblem5aN  41271  dihglblem2aN  41272  dihglblem2N  41273  dihglblem3N  41274  dihmeetlem2N  41278  dihglbcpreN  41279  dihmeetbclemN  41283  dihmeetlem3N  41284  dihmeetlem4preN  41285  dihmeetlem6  41288  dihjatc1  41290  dihmeetlem18N  41303  dih1dimatlem  41308  dihjatcclem1  41397  dihjatcclem2  41398  dihjatcclem4  41400