Theorem lhpbase 40879

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 4289	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2767	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6874	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 142	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2762	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2762	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 40877	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 504	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 701	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3453  ∅c0 4282   class class class wbr 5107  ‘cfv 6537  Basecbs 17307  1.cp1 18516   ⋖ ccvr 40143  LHypclh 40865

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545  df-lhyp 40869

This theorem is used by:  lhplt  40881  lhp2lt  40882  lhpexlt  40883  lhp0lt  40884  lhpexle  40886  lhpexnle  40887  lhpexle1  40889  lhpexle2lem  40890  lhpexle3lem  40892  lhpocnle  40897  lhpocat  40898  lhpjat1  40901  lhpjat2  40902  lhpj1  40903  lhpmcvr  40904  lhpmcvr2  40905  lhpmcvr3  40906  lhpmcvr4N  40907  lhpmcvr5N  40908  lhpmcvr6N  40909  lhpm0atN  40910  lhpmat  40911  lhpmatb  40912  lhp2at0  40913  lhpelim  40918  lhpmod2i2  40919  lhpmod6i1  40920  cdlemb2  40922  lhpat  40924  lhpat3  40927  4atexlemwb  40940  ltrnatb  41018  ltrnel  41020  ltrncnvel  41023  trlval2  41044  trlcl  41045  trljat1  41047  trljat2  41048  trlle  41065  trlval3  41068  cdlemc1  41072  cdlemc2  41073  cdlemc4  41075  cdlemc5  41076  cdlemc6  41077  cdlemd2  41080  cdleme0aa  41091  cdleme0b  41093  cdleme0c  41094  cdleme0cp  41095  cdleme0cq  41096  cdleme0e  41098  cdleme0fN  41099  cdlemeulpq  41101  cdleme01N  41102  cdleme0ex1N  41104  cdleme1b  41107  cdleme1  41108  cdleme2  41109  cdleme3b  41110  cdleme3c  41111  cdleme3g  41115  cdleme3h  41116  cdleme3  41118  cdleme4  41119  cdleme4a  41120  cdleme5  41121  cdleme7aa  41123  cdleme7c  41126  cdleme7d  41127  cdleme7e  41128  cdleme7ga  41129  cdleme7  41130  cdleme8  41131  cdleme9b  41133  cdleme9  41134  cdleme10  41135  cdleme11fN  41145  cdleme11g  41146  cdleme11k  41149  cdleme13  41153  cdleme15b  41156  cdleme15d  41158  cdleme15  41159  cdleme16e  41163  cdleme16f  41164  cdleme22gb  41175  cdlemedb  41178  cdlemednpq  41180  cdleme19b  41185  cdleme19c  41186  cdleme20aN  41190  cdleme20c  41192  cdleme20d  41193  cdleme20e  41194  cdleme20j  41199  cdleme21c  41208  cdleme21ct  41210  cdleme22aa  41220  cdleme22cN  41223  cdleme22d  41224  cdleme22e  41225  cdleme22eALTN  41226  cdleme22f  41227  cdleme22g  41229  cdleme23a  41230  cdleme23b  41231  cdleme23c  41232  cdleme28a  41251  cdleme28b  41252  cdleme29ex  41255  cdleme30a  41259  cdlemefr29exN  41283  cdleme32b  41323  cdleme32c  41324  cdleme32e  41326  cdleme35b  41331  cdleme35c  41332  cdleme35d  41333  cdleme35e  41334  cdleme35f  41335  cdleme42a  41352  cdleme42c  41353  cdleme42h  41363  cdleme42i  41364  cdleme48bw  41383  cdlemeg46frv  41406  cdlemeg46vrg  41408  cdlemeg46rgv  41409  cdlemeg46req  41410  cdlemf1  41442  cdlemf2  41443  trlord  41450  cdlemg2fv2  41481  cdlemg2m  41485  cdlemg7fvbwN  41488  cdlemg4  41498  cdlemg6c  41501  cdlemg10bALTN  41517  cdlemg10c  41520  cdlemg10  41522  cdlemg11b  41523  cdlemg12f  41529  cdlemg17a  41542  cdlemg17dALTN  41545  cdlemg19a  41564  cdlemg35  41594  trlcoabs2N  41603  trlcolem  41607  cdlemh2  41697  cdlemi1  41699  cdlemk3  41714  cdlemk4  41715  cdlemk9  41720  cdlemk9bN  41721  cdlemk10  41724  cdlemk39  41797  dia0eldmN  41921  dia1eldmN  41922  dia0  41933  dia1N  41934  diaglbN  41936  diaintclN  41939  dia2dimlem1  41945  dia2dimlem2  41946  dia2dimlem3  41947  dia2dimlem10  41954  dia2dimlem12  41956  cdlemm10N  41999  docaclN  42005  doca2N  42007  djajN  42018  dib0  42045  dibglbN  42047  dibintclN  42048  cdlemn2  42076  cdlemn10  42087  dihjustlem  42097  dihord1  42099  dihord2a  42100  dihord2b  42101  dihord2cN  42102  dihord11b  42103  dihord11c  42105  dihord2pre  42106  dihord2pre2  42107  dihlsscpre  42115  dib2dim  42124  dih2dimb  42125  dih2dimbALTN  42126  dihvalcq2  42128  dihopelvalcpre  42129  dihord6apre  42137  dihord5b  42140  dihord6b  42141  dihord5apre  42143  dih0  42161  dih1  42167  dihwN  42170  dihmeetlem1N  42171  dihglblem5apreN  42172  dihglblem5aN  42173  dihglblem2aN  42174  dihglblem2N  42175  dihglblem3N  42176  dihmeetlem2N  42180  dihglbcpreN  42181  dihmeetbclemN  42185  dihmeetlem3N  42186  dihmeetlem4preN  42187  dihmeetlem6  42190  dihjatc1  42192  dihmeetlem18N  42205  dih1dimatlem  42210  dihjatcclem1  42299  dihjatcclem2  42300  dihjatcclem4  42302