Theorem paddasslem3

Description: Lemma for paddass . Restate projective space axiom ps-2 . (Contributed by NM, 8-Jan-2012)

	Ref	Expression
Hypotheses	paddasslem.l	|- .<_ = ( le ` K )
	paddasslem.j	|- .\/ = ( join ` K )
	paddasslem.a	|- A = ( Atoms ` K )
Assertion	paddasslem3	|- ( ( K e. HL /\ ( x e. A /\ r e. A /\ y e. A ) /\ ( p e. A /\ z e. A ) ) -> ( ( ( -. x .<_ ( r .\/ y ) /\ p =/= z ) /\ ( p .<_ ( x .\/ r ) /\ z .<_ ( r .\/ y ) ) ) -> E. s e. A ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		paddasslem.l	|- .<_ = ( le ` K )
2		paddasslem.j	|- .\/ = ( join ` K )
3		paddasslem.a	|- A = ( Atoms ` K )
4	1 2 3	ps-2	|- ( ( ( K e. HL /\ ( x e. A /\ r e. A /\ y e. A ) /\ ( p e. A /\ z e. A ) ) /\ ( ( -. x .<_ ( r .\/ y ) /\ p =/= z ) /\ ( p .<_ ( x .\/ r ) /\ z .<_ ( r .\/ y ) ) ) ) -> E. s e. A ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) )
5	4	ex	|- ( ( K e. HL /\ ( x e. A /\ r e. A /\ y e. A ) /\ ( p e. A /\ z e. A ) ) -> ( ( ( -. x .<_ ( r .\/ y ) /\ p =/= z ) /\ ( p .<_ ( x .\/ r ) /\ z .<_ ( r .\/ y ) ) ) -> E. s e. A ( s .<_ ( x .\/ y ) /\ s .<_ ( p .\/ z ) ) ) )