Theorem cdlemesner

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012)

	Ref	Expression
Hypotheses	cdlemesner.l	|- .<_ = ( le ` K )
	cdlemesner.j	|- .\/ = ( join ` K )
	cdlemesner.a	|- A = ( Atoms ` K )
	cdlemesner.h	|- H = ( LHyp ` K )
Assertion	cdlemesner	|- ( ( K e. HL /\ ( R e. A /\ S e. A ) /\ ( R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> S =/= R )

Proof

Step	Hyp	Ref	Expression
1		cdlemesner.l	|- .<_ = ( le ` K )
2		cdlemesner.j	|- .\/ = ( join ` K )
3		cdlemesner.a	|- A = ( Atoms ` K )
4		cdlemesner.h	|- H = ( LHyp ` K )
5		nbrne2	|- ( ( R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) -> R =/= S )
6	5	3ad2ant3	|- ( ( K e. HL /\ ( R e. A /\ S e. A ) /\ ( R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> R =/= S )
7	6	necomd	|- ( ( K e. HL /\ ( R e. A /\ S e. A ) /\ ( R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> S =/= R )