This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem latnlej

Description: An idiom to express that a lattice element differs from two others. (Contributed by NM, 28-May-2012)

Ref Expression
Hypotheses latlej.b 
|- B = ( Base ` K )
latlej.l 
|- .<_ = ( le ` K )
latlej.j 
|- .\/ = ( join ` K )
Assertion latnlej 
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ -. X .<_ ( Y .\/ Z ) ) -> ( X =/= Y /\ X =/= Z ) )

Proof

Step Hyp Ref Expression
1 latlej.b 
 |-  B = ( Base ` K )
2 latlej.l 
 |-  .<_ = ( le ` K )
3 latlej.j 
 |-  .\/ = ( join ` K )
4 1 2 3 latlej1 
 |-  ( ( K e. Lat /\ Y e. B /\ Z e. B ) -> Y .<_ ( Y .\/ Z ) )
5 4 3adant3r1 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y .<_ ( Y .\/ Z ) )
6 breq1 
 |-  ( X = Y -> ( X .<_ ( Y .\/ Z ) <-> Y .<_ ( Y .\/ Z ) ) )
7 5 6 syl5ibrcom 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X = Y -> X .<_ ( Y .\/ Z ) ) )
8 7 necon3bd 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( -. X .<_ ( Y .\/ Z ) -> X =/= Y ) )
9 1 2 3 latlej2 
 |-  ( ( K e. Lat /\ Y e. B /\ Z e. B ) -> Z .<_ ( Y .\/ Z ) )
10 9 3adant3r1 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z .<_ ( Y .\/ Z ) )
11 breq1 
 |-  ( X = Z -> ( X .<_ ( Y .\/ Z ) <-> Z .<_ ( Y .\/ Z ) ) )
12 10 11 syl5ibrcom 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X = Z -> X .<_ ( Y .\/ Z ) ) )
13 12 necon3bd 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( -. X .<_ ( Y .\/ Z ) -> X =/= Z ) )
14 8 13 jcad 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( -. X .<_ ( Y .\/ Z ) -> ( X =/= Y /\ X =/= Z ) ) )
15 14 3impia 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ -. X .<_ ( Y .\/ Z ) ) -> ( X =/= Y /\ X =/= Z ) )