Theorem lhpocnel2

Description: The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 20-Feb-2014)

	Ref	Expression
Hypotheses	lhpocnel2.l	|- .<_ = ( le ` K )
	lhpocnel2.a	|- A = ( Atoms ` K )
	lhpocnel2.h	|- H = ( LHyp ` K )
	lhpocnel2.p	|- P = ( ( oc ` K ) ` W )
Assertion	lhpocnel2	|- ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) )

Proof

Step	Hyp	Ref	Expression
1		lhpocnel2.l	|- .<_ = ( le ` K )
2		lhpocnel2.a	|- A = ( Atoms ` K )
3		lhpocnel2.h	|- H = ( LHyp ` K )
4		lhpocnel2.p	|- P = ( ( oc ` K ) ` W )
5		eqid	|- ( oc ` K ) = ( oc ` K )
6	1 5 2 3	lhpocnel	|- ( ( K e. HL /\ W e. H ) -> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) .<_ W ) )
7	4	eleq1i	|- ( P e. A <-> ( ( oc ` K ) ` W ) e. A )
8	4	breq1i	|- ( P .<_ W <-> ( ( oc ` K ) ` W ) .<_ W )
9	8	notbii	|- ( -. P .<_ W <-> -. ( ( oc ` K ) ` W ) .<_ W )
10	7 9	anbi12i	|- ( ( P e. A /\ -. P .<_ W ) <-> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) .<_ W ) )
11	6 10	sylibr	|- ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) )