Theorem lhpbase

Description: A co-atom is a member of the lattice base set (i.e., a lattice element). (Contributed by NM, 18-May-2012)

	Ref	Expression
Hypotheses	lhpbase.b	|- B = ( Base ` K )
	lhpbase.h	|- H = ( LHyp ` K )
Assertion	lhpbase	|- ( W e. H -> W e. B )

Proof

Step	Hyp	Ref	Expression
1		lhpbase.b	|- B = ( Base ` K )
2		lhpbase.h	|- H = ( LHyp ` K )
3		n0i	|- ( W e. H -> -. H = (/) )
4	2	eqeq1i	|- ( H = (/) <-> ( LHyp ` K ) = (/) )
5	3 4	sylnib	|- ( W e. H -> -. ( LHyp ` K ) = (/) )
6		fvprc	|- ( -. K e. _V -> ( LHyp ` K ) = (/) )
7	5 6	nsyl2	|- ( W e. H -> K e. _V )
8		eqid	|- ( 1. ` K ) = ( 1. ` K )
9		eqid	|- (
10	1 8 9 2	islhp	|- ( K e. _V -> ( W e. H <-> ( W e. B /\ W (
11	10	simprbda	|- ( ( K e. _V /\ W e. H ) -> W e. B )
12	7 11	mpancom	|- ( W e. H -> W e. B )