Theorem islhp

Description: The predicate "is a co-atom (lattice hyperplane)". (Contributed by NM, 11-May-2012)

	Ref	Expression
Hypotheses	lhpset.b	|- B = ( Base ` K )
	lhpset.u	|- .1. = ( 1. ` K )
	lhpset.c	|- C = (
	lhpset.h	|- H = ( LHyp ` K )
Assertion	islhp	|- ( K e. A -> ( W e. H <-> ( W e. B /\ W C .1. ) ) )

Proof

Step	Hyp	Ref	Expression
1		lhpset.b	|- B = ( Base ` K )
2		lhpset.u	|- .1. = ( 1. ` K )
3		lhpset.c	|- C = (
4		lhpset.h	|- H = ( LHyp ` K )
5	1 2 3 4	lhpset	|- ( K e. A -> H = { w e. B | w C .1. } )
6	5	eleq2d	|- ( K e. A -> ( W e. H <-> W e. { w e. B | w C .1. } ) )
7		breq1	|- ( w = W -> ( w C .1. <-> W C .1. ) )
8	7	elrab	|- ( W e. { w e. B | w C .1. } <-> ( W e. B /\ W C .1. ) )
9	6 8	bitrdi	|- ( K e. A -> ( W e. H <-> ( W e. B /\ W C .1. ) ) )