Metamath Proof Explorer

Theorem cdleme21at

Description: Part of proof of Lemma E in Crawley p. 115. (Contributed by NM, 29-Nov-2012)

		Ref	Expression
	Hypotheses	cdleme21.l	\|- .<_ = ( le ` K )
		cdleme21.j	\|- .\/ = ( join ` K )
		cdleme21.m	\|- ./\ = ( meet ` K )
		cdleme21.a	\|- A = ( Atoms ` K )
		cdleme21.h	\|- H = ( LHyp ` K )
		cdleme21.u	\|- U = ( ( P .\/ Q ) ./\ W )
	Assertion	cdleme21at	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ U .<_ ( S .\/ T ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> T =/= z )

Proof

Step	Hyp	Ref	Expression
1		cdleme21.l	\|- .<_ = ( le ` K )
2		cdleme21.j	\|- .\/ = ( join ` K )
3		cdleme21.m	\|- ./\ = ( meet ` K )
4		cdleme21.a	\|- A = ( Atoms ` K )
5		cdleme21.h	\|- H = ( LHyp ` K )
6		cdleme21.u	\|- U = ( ( P .\/ Q ) ./\ W )
7	1 2 3 4 5 6	cdleme21c	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> -. U .<_ ( S .\/ z ) )
8	7	3adant2r	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ U .<_ ( S .\/ T ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> -. U .<_ ( S .\/ z ) )
9		simp2r	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ U .<_ ( S .\/ T ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> U .<_ ( S .\/ T ) )
10		oveq2	\|- ( T = z -> ( S .\/ T ) = ( S .\/ z ) )
11	10	breq2d	\|- ( T = z -> ( U .<_ ( S .\/ T ) <-> U .<_ ( S .\/ z ) ) )
12	9 11	syl5ibcom	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ U .<_ ( S .\/ T ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> ( T = z -> U .<_ ( S .\/ z ) ) )
13	12	necon3bd	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ U .<_ ( S .\/ T ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> ( -. U .<_ ( S .\/ z ) -> T =/= z ) )
14	8 13	mpd	\|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( S e. A /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) /\ U .<_ ( S .\/ T ) ) /\ ( z e. A /\ ( P .\/ z ) = ( S .\/ z ) ) ) -> T =/= z )