Theorem lhpbase 40444

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3429  ∅c0 4273   class class class wbr 5085  ‘cfv 6498  Basecbs 17179  1.cp1 18388   ⋖ ccvr 39708  LHypclh 40430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fv 6506  df-lhyp 40434

This theorem is referenced by:  lhplt  40446  lhp2lt  40447  lhpexlt  40448  lhp0lt  40449  lhpexle  40451  lhpexnle  40452  lhpexle1  40454  lhpexle2lem  40455  lhpexle3lem  40457  lhpocnle  40462  lhpocat  40463  lhpjat1  40466  lhpjat2  40467  lhpj1  40468  lhpmcvr  40469  lhpmcvr2  40470  lhpmcvr3  40471  lhpmcvr4N  40472  lhpmcvr5N  40473  lhpmcvr6N  40474  lhpm0atN  40475  lhpmat  40476  lhpmatb  40477  lhp2at0  40478  lhpelim  40483  lhpmod2i2  40484  lhpmod6i1  40485  cdlemb2  40487  lhpat  40489  lhpat3  40492  4atexlemwb  40505  ltrnatb  40583  ltrnel  40585  ltrncnvel  40588  trlval2  40609  trlcl  40610  trljat1  40612  trljat2  40613  trlle  40630  trlval3  40633  cdlemc1  40637  cdlemc2  40638  cdlemc4  40640  cdlemc5  40641  cdlemc6  40642  cdlemd2  40645  cdleme0aa  40656  cdleme0b  40658  cdleme0c  40659  cdleme0cp  40660  cdleme0cq  40661  cdleme0e  40663  cdleme0fN  40664  cdlemeulpq  40666  cdleme01N  40667  cdleme0ex1N  40669  cdleme1b  40672  cdleme1  40673  cdleme2  40674  cdleme3b  40675  cdleme3c  40676  cdleme3g  40680  cdleme3h  40681  cdleme3  40683  cdleme4  40684  cdleme4a  40685  cdleme5  40686  cdleme7aa  40688  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme8  40696  cdleme9b  40698  cdleme9  40699  cdleme10  40700  cdleme11fN  40710  cdleme11g  40711  cdleme11k  40714  cdleme13  40718  cdleme15b  40721  cdleme15d  40723  cdleme15  40724  cdleme16e  40728  cdleme16f  40729  cdleme22gb  40740  cdlemedb  40743  cdlemednpq  40745  cdleme19b  40750  cdleme19c  40751  cdleme20aN  40755  cdleme20c  40757  cdleme20d  40758  cdleme20e  40759  cdleme20j  40764  cdleme21c  40773  cdleme21ct  40775  cdleme22aa  40785  cdleme22cN  40788  cdleme22d  40789  cdleme22e  40790  cdleme22eALTN  40791  cdleme22f  40792  cdleme22g  40794  cdleme23a  40795  cdleme23b  40796  cdleme23c  40797  cdleme28a  40816  cdleme28b  40817  cdleme29ex  40820  cdleme30a  40824  cdlemefr29exN  40848  cdleme32b  40888  cdleme32c  40889  cdleme32e  40891  cdleme35b  40896  cdleme35c  40897  cdleme35d  40898  cdleme35e  40899  cdleme35f  40900  cdleme42a  40917  cdleme42c  40918  cdleme42h  40928  cdleme42i  40929  cdleme48bw  40948  cdlemeg46frv  40971  cdlemeg46vrg  40973  cdlemeg46rgv  40974  cdlemeg46req  40975  cdlemf1  41007  cdlemf2  41008  trlord  41015  cdlemg2fv2  41046  cdlemg2m  41050  cdlemg7fvbwN  41053  cdlemg4  41063  cdlemg6c  41066  cdlemg10bALTN  41082  cdlemg10c  41085  cdlemg10  41087  cdlemg11b  41088  cdlemg12f  41094  cdlemg17a  41107  cdlemg17dALTN  41110  cdlemg19a  41129  cdlemg35  41159  trlcoabs2N  41168  trlcolem  41172  cdlemh2  41262  cdlemi1  41264  cdlemk3  41279  cdlemk4  41280  cdlemk9  41285  cdlemk9bN  41286  cdlemk10  41289  cdlemk39  41362  dia0eldmN  41486  dia1eldmN  41487  dia0  41498  dia1N  41499  diaglbN  41501  diaintclN  41504  dia2dimlem1  41510  dia2dimlem2  41511  dia2dimlem3  41512  dia2dimlem10  41519  dia2dimlem12  41521  cdlemm10N  41564  docaclN  41570  doca2N  41572  djajN  41583  dib0  41610  dibglbN  41612  dibintclN  41613  cdlemn2  41641  cdlemn10  41652  dihjustlem  41662  dihord1  41664  dihord2a  41665  dihord2b  41666  dihord2cN  41667  dihord11b  41668  dihord11c  41670  dihord2pre  41671  dihord2pre2  41672  dihlsscpre  41680  dib2dim  41689  dih2dimb  41690  dih2dimbALTN  41691  dihvalcq2  41693  dihopelvalcpre  41694  dihord6apre  41702  dihord5b  41705  dihord6b  41706  dihord5apre  41708  dih0  41726  dih1  41732  dihwN  41735  dihmeetlem1N  41736  dihglblem5apreN  41737  dihglblem5aN  41738  dihglblem2aN  41739  dihglblem2N  41740  dihglblem3N  41741  dihmeetlem2N  41745  dihglbcpreN  41746  dihmeetbclemN  41750  dihmeetlem3N  41751  dihmeetlem4preN  41752  dihmeetlem6  41755  dihjatc1  41757  dihmeetlem18N  41770  dih1dimatlem  41775  dihjatcclem1  41864  dihjatcclem2  41865  dihjatcclem4  41867