# Metamath Proof Explorer

Description: Lemma for paddass . (Contributed by NM, 8-Jan-2012)

Ref Expression
`|- .<_ = ( le ` K )`
`|- .\/ = ( join ` K )`
`|- A = ( Atoms ` K )`
`|- ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> p .<_ ( s .\/ z ) )`

### Proof

Step Hyp Ref Expression
` |-  .<_ = ( le ` K )`
` |-  .\/ = ( join ` K )`
` |-  A = ( Atoms ` K )`
4 simpl1
` |-  ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> K e. HL )`
5 simpl2r
` |-  ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> s e. A )`
6 simpl2l
` |-  ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> p e. A )`
7 simpl3
` |-  ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> z e. A )`
8 5 6 7 3jca
` |-  ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> ( s e. A /\ p e. A /\ z e. A ) )`
9 simprl
` |-  ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> s =/= z )`
10 4 8 9 3jca
` |-  ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> ( K e. HL /\ ( s e. A /\ p e. A /\ z e. A ) /\ s =/= z ) )`
11 simprr
` |-  ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> s .<_ ( p .\/ z ) )`
12 1 2 3 hlatexch2
` |-  ( ( K e. HL /\ ( s e. A /\ p e. A /\ z e. A ) /\ s =/= z ) -> ( s .<_ ( p .\/ z ) -> p .<_ ( s .\/ z ) ) )`
13 10 11 12 sylc
` |-  ( ( ( K e. HL /\ ( p e. A /\ s e. A ) /\ z e. A ) /\ ( s =/= z /\ s .<_ ( p .\/ z ) ) ) -> p .<_ ( s .\/ z ) )`