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 ) )