Theorem lhpbase 40000

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3480  ∅c0 4333   class class class wbr 5143  ‘cfv 6561  Basecbs 17247  1.cp1 18469   ⋖ ccvr 39263  LHypclh 39986

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-lhyp 39990

This theorem is referenced by:  lhplt  40002  lhp2lt  40003  lhpexlt  40004  lhp0lt  40005  lhpexle  40007  lhpexnle  40008  lhpexle1  40010  lhpexle2lem  40011  lhpexle3lem  40013  lhpocnle  40018  lhpocat  40019  lhpjat1  40022  lhpjat2  40023  lhpj1  40024  lhpmcvr  40025  lhpmcvr2  40026  lhpmcvr3  40027  lhpmcvr4N  40028  lhpmcvr5N  40029  lhpmcvr6N  40030  lhpm0atN  40031  lhpmat  40032  lhpmatb  40033  lhp2at0  40034  lhpelim  40039  lhpmod2i2  40040  lhpmod6i1  40041  cdlemb2  40043  lhpat  40045  lhpat3  40048  4atexlemwb  40061  ltrnatb  40139  ltrnel  40141  ltrncnvel  40144  trlval2  40165  trlcl  40166  trljat1  40168  trljat2  40169  trlle  40186  trlval3  40189  cdlemc1  40193  cdlemc2  40194  cdlemc4  40196  cdlemc5  40197  cdlemc6  40198  cdlemd2  40201  cdleme0aa  40212  cdleme0b  40214  cdleme0c  40215  cdleme0cp  40216  cdleme0cq  40217  cdleme0e  40219  cdleme0fN  40220  cdlemeulpq  40222  cdleme01N  40223  cdleme0ex1N  40225  cdleme1b  40228  cdleme1  40229  cdleme2  40230  cdleme3b  40231  cdleme3c  40232  cdleme3g  40236  cdleme3h  40237  cdleme3  40239  cdleme4  40240  cdleme4a  40241  cdleme5  40242  cdleme7aa  40244  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme7  40251  cdleme8  40252  cdleme9b  40254  cdleme9  40255  cdleme10  40256  cdleme11fN  40266  cdleme11g  40267  cdleme11k  40270  cdleme13  40274  cdleme15b  40277  cdleme15d  40279  cdleme15  40280  cdleme16e  40284  cdleme16f  40285  cdleme22gb  40296  cdlemedb  40299  cdlemednpq  40301  cdleme19b  40306  cdleme19c  40307  cdleme20aN  40311  cdleme20c  40313  cdleme20d  40314  cdleme20e  40315  cdleme20j  40320  cdleme21c  40329  cdleme21ct  40331  cdleme22aa  40341  cdleme22cN  40344  cdleme22d  40345  cdleme22e  40346  cdleme22eALTN  40347  cdleme22f  40348  cdleme22g  40350  cdleme23a  40351  cdleme23b  40352  cdleme23c  40353  cdleme28a  40372  cdleme28b  40373  cdleme29ex  40376  cdleme30a  40380  cdlemefr29exN  40404  cdleme32b  40444  cdleme32c  40445  cdleme32e  40447  cdleme35b  40452  cdleme35c  40453  cdleme35d  40454  cdleme35e  40455  cdleme35f  40456  cdleme42a  40473  cdleme42c  40474  cdleme42h  40484  cdleme42i  40485  cdleme48bw  40504  cdlemeg46frv  40527  cdlemeg46vrg  40529  cdlemeg46rgv  40530  cdlemeg46req  40531  cdlemf1  40563  cdlemf2  40564  trlord  40571  cdlemg2fv2  40602  cdlemg2m  40606  cdlemg7fvbwN  40609  cdlemg4  40619  cdlemg6c  40622  cdlemg10bALTN  40638  cdlemg10c  40641  cdlemg10  40643  cdlemg11b  40644  cdlemg12f  40650  cdlemg17a  40663  cdlemg17dALTN  40666  cdlemg19a  40685  cdlemg35  40715  trlcoabs2N  40724  trlcolem  40728  cdlemh2  40818  cdlemi1  40820  cdlemk3  40835  cdlemk4  40836  cdlemk9  40841  cdlemk9bN  40842  cdlemk10  40845  cdlemk39  40918  dia0eldmN  41042  dia1eldmN  41043  dia0  41054  dia1N  41055  diaglbN  41057  diaintclN  41060  dia2dimlem1  41066  dia2dimlem2  41067  dia2dimlem3  41068  dia2dimlem10  41075  dia2dimlem12  41077  cdlemm10N  41120  docaclN  41126  doca2N  41128  djajN  41139  dib0  41166  dibglbN  41168  dibintclN  41169  cdlemn2  41197  cdlemn10  41208  dihjustlem  41218  dihord1  41220  dihord2a  41221  dihord2b  41222  dihord2cN  41223  dihord11b  41224  dihord11c  41226  dihord2pre  41227  dihord2pre2  41228  dihlsscpre  41236  dib2dim  41245  dih2dimb  41246  dih2dimbALTN  41247  dihvalcq2  41249  dihopelvalcpre  41250  dihord6apre  41258  dihord5b  41261  dihord6b  41262  dihord5apre  41264  dih0  41282  dih1  41288  dihwN  41291  dihmeetlem1N  41292  dihglblem5apreN  41293  dihglblem5aN  41294  dihglblem2aN  41295  dihglblem2N  41296  dihglblem3N  41297  dihmeetlem2N  41301  dihglbcpreN  41302  dihmeetbclemN  41306  dihmeetlem3N  41307  dihmeetlem4preN  41308  dihmeetlem6  41311  dihjatc1  41313  dihmeetlem18N  41326  dih1dimatlem  41331  dihjatcclem1  41420  dihjatcclem2  41421  dihjatcclem4  41423