Theorem lhpbase 40753

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 4294	. . . 4 ⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅)
2		lhpbase.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3	2	eqeq1i 2768	. . . 4 ⊢ (𝐻 = ∅ ↔ (LHyp‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅)
5		fvprc 6875	. . 3 ⊢ (¬ 𝐾 ∈ V → (LHyp‘𝐾) = ∅)
6	4, 5	nsyl2 142	. 2 ⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V)
7		lhpbase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2763	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
9		eqid 2763	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	islhp 40751	. . 3 ⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾))))
11	10	simprbda 503	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵)
12	6, 11	mpancom 700	1 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  Vcvv 3455  ∅c0 4287   class class class wbr 5110  ‘cfv 6538  Basecbs 17270  1.cp1 18479   ⋖ ccvr 40017  LHypclh 40739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546  df-lhyp 40743

This theorem is referenced by:  lhplt  40755  lhp2lt  40756  lhpexlt  40757  lhp0lt  40758  lhpexle  40760  lhpexnle  40761  lhpexle1  40763  lhpexle2lem  40764  lhpexle3lem  40766  lhpocnle  40771  lhpocat  40772  lhpjat1  40775  lhpjat2  40776  lhpj1  40777  lhpmcvr  40778  lhpmcvr2  40779  lhpmcvr3  40780  lhpmcvr4N  40781  lhpmcvr5N  40782  lhpmcvr6N  40783  lhpm0atN  40784  lhpmat  40785  lhpmatb  40786  lhp2at0  40787  lhpelim  40792  lhpmod2i2  40793  lhpmod6i1  40794  cdlemb2  40796  lhpat  40798  lhpat3  40801  4atexlemwb  40814  ltrnatb  40892  ltrnel  40894  ltrncnvel  40897  trlval2  40918  trlcl  40919  trljat1  40921  trljat2  40922  trlle  40939  trlval3  40942  cdlemc1  40946  cdlemc2  40947  cdlemc4  40949  cdlemc5  40950  cdlemc6  40951  cdlemd2  40954  cdleme0aa  40965  cdleme0b  40967  cdleme0c  40968  cdleme0cp  40969  cdleme0cq  40970  cdleme0e  40972  cdleme0fN  40973  cdlemeulpq  40975  cdleme01N  40976  cdleme0ex1N  40978  cdleme1b  40981  cdleme1  40982  cdleme2  40983  cdleme3b  40984  cdleme3c  40985  cdleme3g  40989  cdleme3h  40990  cdleme3  40992  cdleme4  40993  cdleme4a  40994  cdleme5  40995  cdleme7aa  40997  cdleme7c  41000  cdleme7d  41001  cdleme7e  41002  cdleme7ga  41003  cdleme7  41004  cdleme8  41005  cdleme9b  41007  cdleme9  41008  cdleme10  41009  cdleme11fN  41019  cdleme11g  41020  cdleme11k  41023  cdleme13  41027  cdleme15b  41030  cdleme15d  41032  cdleme15  41033  cdleme16e  41037  cdleme16f  41038  cdleme22gb  41049  cdlemedb  41052  cdlemednpq  41054  cdleme19b  41059  cdleme19c  41060  cdleme20aN  41064  cdleme20c  41066  cdleme20d  41067  cdleme20e  41068  cdleme20j  41073  cdleme21c  41082  cdleme21ct  41084  cdleme22aa  41094  cdleme22cN  41097  cdleme22d  41098  cdleme22e  41099  cdleme22eALTN  41100  cdleme22f  41101  cdleme22g  41103  cdleme23a  41104  cdleme23b  41105  cdleme23c  41106  cdleme28a  41125  cdleme28b  41126  cdleme29ex  41129  cdleme30a  41133  cdlemefr29exN  41157  cdleme32b  41197  cdleme32c  41198  cdleme32e  41200  cdleme35b  41205  cdleme35c  41206  cdleme35d  41207  cdleme35e  41208  cdleme35f  41209  cdleme42a  41226  cdleme42c  41227  cdleme42h  41237  cdleme42i  41238  cdleme48bw  41257  cdlemeg46frv  41280  cdlemeg46vrg  41282  cdlemeg46rgv  41283  cdlemeg46req  41284  cdlemf1  41316  cdlemf2  41317  trlord  41324  cdlemg2fv2  41355  cdlemg2m  41359  cdlemg7fvbwN  41362  cdlemg4  41372  cdlemg6c  41375  cdlemg10bALTN  41391  cdlemg10c  41394  cdlemg10  41396  cdlemg11b  41397  cdlemg12f  41403  cdlemg17a  41416  cdlemg17dALTN  41419  cdlemg19a  41438  cdlemg35  41468  trlcoabs2N  41477  trlcolem  41481  cdlemh2  41571  cdlemi1  41573  cdlemk3  41588  cdlemk4  41589  cdlemk9  41594  cdlemk9bN  41595  cdlemk10  41598  cdlemk39  41671  dia0eldmN  41795  dia1eldmN  41796  dia0  41807  dia1N  41808  diaglbN  41810  diaintclN  41813  dia2dimlem1  41819  dia2dimlem2  41820  dia2dimlem3  41821  dia2dimlem10  41828  dia2dimlem12  41830  cdlemm10N  41873  docaclN  41879  doca2N  41881  djajN  41892  dib0  41919  dibglbN  41921  dibintclN  41922  cdlemn2  41950  cdlemn10  41961  dihjustlem  41971  dihord1  41973  dihord2a  41974  dihord2b  41975  dihord2cN  41976  dihord11b  41977  dihord11c  41979  dihord2pre  41980  dihord2pre2  41981  dihlsscpre  41989  dib2dim  41998  dih2dimb  41999  dih2dimbALTN  42000  dihvalcq2  42002  dihopelvalcpre  42003  dihord6apre  42011  dihord5b  42014  dihord6b  42015  dihord5apre  42017  dih0  42035  dih1  42041  dihwN  42044  dihmeetlem1N  42045  dihglblem5apreN  42046  dihglblem5aN  42047  dihglblem2aN  42048  dihglblem2N  42049  dihglblem3N  42050  dihmeetlem2N  42054  dihglbcpreN  42055  dihmeetbclemN  42059  dihmeetlem3N  42060  dihmeetlem4preN  42061  dihmeetlem6  42064  dihjatc1  42066  dihmeetlem18N  42079  dih1dimatlem  42084  dihjatcclem1  42173  dihjatcclem2  42174  dihjatcclem4  42176