Metamath Proof Explorer

Theorem cdleme27a

Description: Part of proof of Lemma E in Crawley p. 113. cdleme26f with s and t swapped (this case is not mentioned by them). If s <_ t \/ v, then f(s) <_ f_s(t) \/ v. TODO: FIX COMMENT. (Contributed by NM, 3-Feb-2013)

Ref Expression
Hypotheses cdleme26.b 
|- B = ( Base ` K )
cdleme26.l 
|- .<_ = ( le ` K )
cdleme26.j 
|- .\/ = ( join ` K )
cdleme26.m 
|- ./\ = ( meet ` K )
cdleme26.a 
|- A = ( Atoms ` K )
cdleme26.h 
|- H = ( LHyp ` K )
cdleme27.u 
|- U = ( ( P .\/ Q ) ./\ W )
cdleme27.f 
|- F = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
cdleme27.z 
|- Z = ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) )
cdleme27.n 
|- N = ( ( P .\/ Q ) ./\ ( Z .\/ ( ( s .\/ z ) ./\ W ) ) )
cdleme27.d 
|- D = ( iota_ u e. B A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = N ) )
cdleme27.c 
|- C = if ( s .<_ ( P .\/ Q ) , D , F )
cdleme27.g 
|- G = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
cdleme27.o 
|- O = ( ( P .\/ Q ) ./\ ( Z .\/ ( ( t .\/ z ) ./\ W ) ) )
cdleme27.e 
|- E = ( iota_ u e. B A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = O ) )
cdleme27.y 
|- Y = if ( t .<_ ( P .\/ Q ) , E , G )
Assertion cdleme27a 
|- ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> C .<_ ( Y .\/ V ) )

Proof

Step Hyp Ref Expression
1 cdleme26.b 
 |-  B = ( Base ` K )
2 cdleme26.l 
 |-  .<_ = ( le ` K )
3 cdleme26.j 
 |-  .\/ = ( join ` K )
4 cdleme26.m 
 |-  ./\ = ( meet ` K )
5 cdleme26.a 
 |-  A = ( Atoms ` K )
6 cdleme26.h 
 |-  H = ( LHyp ` K )
7 cdleme27.u 
 |-  U = ( ( P .\/ Q ) ./\ W )
8 cdleme27.f 
 |-  F = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
9 cdleme27.z 
 |-  Z = ( ( z .\/ U ) ./\ ( Q .\/ ( ( P .\/ z ) ./\ W ) ) )
10 cdleme27.n 
 |-  N = ( ( P .\/ Q ) ./\ ( Z .\/ ( ( s .\/ z ) ./\ W ) ) )
11 cdleme27.d 
 |-  D = ( iota_ u e. B A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = N ) )
12 cdleme27.c 
 |-  C = if ( s .<_ ( P .\/ Q ) , D , F )
13 cdleme27.g 
 |-  G = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
14 cdleme27.o 
 |-  O = ( ( P .\/ Q ) ./\ ( Z .\/ ( ( t .\/ z ) ./\ W ) ) )
15 cdleme27.e 
 |-  E = ( iota_ u e. B A. z e. A ( ( -. z .<_ W /\ -. z .<_ ( P .\/ Q ) ) -> u = O ) )
16 cdleme27.y 
 |-  Y = if ( t .<_ ( P .\/ Q ) , E , G )
17 simp211 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( K e. HL /\ W e. H ) )
18 simp221 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( P e. A /\ -. P .<_ W ) )
19 simp222 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( Q e. A /\ -. Q .<_ W ) )
20 simp213 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( s e. A /\ -. s .<_ W ) )
21 simp223 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( t e. A /\ -. t .<_ W ) )
22 simp23r 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( V e. A /\ V .<_ W ) )
23 simp212 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> P =/= Q )
24 simp1l 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> s .<_ ( P .\/ Q ) )
25 simp1r 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> t .<_ ( P .\/ Q ) )
26 23 24 25 3jca 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( P =/= Q /\ s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) )
27 simp3 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> ( t .\/ V ) = ( P .\/ Q ) )
28 1 2 3 4 5 6 7 9 10 14 11 15 cdleme26ee 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( s e. A /\ -. s .<_ W ) /\ ( t e. A /\ -. t .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ ( ( P =/= Q /\ s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) ) -> D .<_ ( E .\/ V ) )
29 17 18 19 20 21 22 26 27 28 syl332anc 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) = ( P .\/ Q ) ) -> D .<_ ( E .\/ V ) )
30 29 3expia 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( ( t .\/ V ) = ( P .\/ Q ) -> D .<_ ( E .\/ V ) ) )
31 simp1r 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> t .<_ ( P .\/ Q ) )
32 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> K e. HL )
33 32 3ad2ant2 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> K e. HL )
34 simp13l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> s e. A )
35 34 3ad2ant2 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> s e. A )
36 simp23l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> t e. A )
37 36 3ad2ant2 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> t e. A )
38 simp3ll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> s =/= t )
39 38 3ad2ant2 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> s =/= t )
40 35 37 39 3jca 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> ( s e. A /\ t e. A /\ s =/= t ) )
41 simp21l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> P e. A )
42 41 3ad2ant2 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> P e. A )
43 simp22l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> Q e. A )
44 43 3ad2ant2 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> Q e. A )
45 simp212 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> P =/= Q )
46 simp3rl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> V e. A )
47 46 3ad2ant2 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> V e. A )
48 simp3 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> ( t .\/ V ) =/= ( P .\/ Q ) )
49 simp3lr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> s .<_ ( t .\/ V ) )
50 49 3ad2ant2 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> s .<_ ( t .\/ V ) )
51 simp1l 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> s .<_ ( P .\/ Q ) )
52 48 50 51 3jca 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> ( ( t .\/ V ) =/= ( P .\/ Q ) /\ s .<_ ( t .\/ V ) /\ s .<_ ( P .\/ Q ) ) )
53 2 3 4 5 6 cdleme22b 
 |-  ( ( ( K e. HL /\ ( s e. A /\ t e. A /\ s =/= t ) ) /\ ( P e. A /\ Q e. A /\ P =/= Q ) /\ ( V e. A /\ ( ( t .\/ V ) =/= ( P .\/ Q ) /\ s .<_ ( t .\/ V ) /\ s .<_ ( P .\/ Q ) ) ) ) -> -. t .<_ ( P .\/ Q ) )
54 33 40 42 44 45 47 52 53 syl232anc 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> -. t .<_ ( P .\/ Q ) )
55 31 54 pm2.21dd 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) /\ ( t .\/ V ) =/= ( P .\/ Q ) ) -> D .<_ ( E .\/ V ) )
56 55 3expia 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( ( t .\/ V ) =/= ( P .\/ Q ) -> D .<_ ( E .\/ V ) ) )
57 30 56 pm2.61dne 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> D .<_ ( E .\/ V ) )
58 iftrue 
 |-  ( s .<_ ( P .\/ Q ) -> if ( s .<_ ( P .\/ Q ) , D , F ) = D )
59 12 58 syl5eq 
 |-  ( s .<_ ( P .\/ Q ) -> C = D )
60 59 ad2antrr 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C = D )
61 iftrue 
 |-  ( t .<_ ( P .\/ Q ) -> if ( t .<_ ( P .\/ Q ) , E , G ) = E )
62 16 61 syl5eq 
 |-  ( t .<_ ( P .\/ Q ) -> Y = E )
63 62 oveq1d 
 |-  ( t .<_ ( P .\/ Q ) -> ( Y .\/ V ) = ( E .\/ V ) )
64 63 ad2antlr 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( Y .\/ V ) = ( E .\/ V ) )
65 57 60 64 3brtr4d 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C .<_ ( Y .\/ V ) )
66 65 ex 
 |-  ( ( s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) -> ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> C .<_ ( Y .\/ V ) ) )
67 simpr11 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( K e. HL /\ W e. H ) )
68 simpr12 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> P =/= Q )
69 simpll 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> s .<_ ( P .\/ Q ) )
70 68 69 jca 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( P =/= Q /\ s .<_ ( P .\/ Q ) ) )
71 simpr23 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( t e. A /\ -. t .<_ W ) )
72 simpr21 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( P e. A /\ -. P .<_ W ) )
73 simpr22 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
74 simpr13 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( s e. A /\ -. s .<_ W ) )
75 simplr 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> -. t .<_ ( P .\/ Q ) )
76 simpr3l 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( s =/= t /\ s .<_ ( t .\/ V ) ) )
77 simpr3r 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( V e. A /\ V .<_ W ) )
78 eqid 
 |-  ( ( P .\/ Q ) ./\ ( G .\/ ( ( s .\/ t ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( G .\/ ( ( s .\/ t ) ./\ W ) ) )
79 eqid 
 |-  ( iota_ u e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( G .\/ ( ( s .\/ t ) ./\ W ) ) ) ) ) = ( iota_ u e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( G .\/ ( ( s .\/ t ) ./\ W ) ) ) ) )
80 9 10 13 78 11 79 cdleme25cv 
 |-  D = ( iota_ u e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( G .\/ ( ( s .\/ t ) ./\ W ) ) ) ) )
81 1 2 3 4 5 6 7 13 78 80 cdleme26f 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ s .<_ ( P .\/ Q ) ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( s e. A /\ -. s .<_ W ) ) /\ ( -. t .<_ ( P .\/ Q ) /\ ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> D .<_ ( G .\/ V ) )
82 67 70 71 72 73 74 75 76 77 81 syl333anc 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> D .<_ ( G .\/ V ) )
83 59 ad2antrr 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C = D )
84 iffalse 
 |-  ( -. t .<_ ( P .\/ Q ) -> if ( t .<_ ( P .\/ Q ) , E , G ) = G )
85 16 84 syl5eq 
 |-  ( -. t .<_ ( P .\/ Q ) -> Y = G )
86 85 oveq1d 
 |-  ( -. t .<_ ( P .\/ Q ) -> ( Y .\/ V ) = ( G .\/ V ) )
87 86 ad2antlr 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( Y .\/ V ) = ( G .\/ V ) )
88 82 83 87 3brtr4d 
 |-  ( ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C .<_ ( Y .\/ V ) )
89 88 ex 
 |-  ( ( s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) -> ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> C .<_ ( Y .\/ V ) ) )
90 simpr11 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( K e. HL /\ W e. H ) )
91 simpr12 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> P =/= Q )
92 simplr 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> t .<_ ( P .\/ Q ) )
93 91 92 jca 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( P =/= Q /\ t .<_ ( P .\/ Q ) ) )
94 simpr13 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( s e. A /\ -. s .<_ W ) )
95 simpr21 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( P e. A /\ -. P .<_ W ) )
96 simpr22 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
97 simpr23 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( t e. A /\ -. t .<_ W ) )
98 simpll 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> -. s .<_ ( P .\/ Q ) )
99 simpr3l 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( s =/= t /\ s .<_ ( t .\/ V ) ) )
100 simpr3r 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( V e. A /\ V .<_ W ) )
101 eqid 
 |-  ( ( P .\/ Q ) ./\ ( F .\/ ( ( t .\/ s ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( F .\/ ( ( t .\/ s ) ./\ W ) ) )
102 eqid 
 |-  ( iota_ u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( F .\/ ( ( t .\/ s ) ./\ W ) ) ) ) ) = ( iota_ u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( F .\/ ( ( t .\/ s ) ./\ W ) ) ) ) )
103 9 14 8 101 15 102 cdleme25cv 
 |-  E = ( iota_ u e. B A. s e. A ( ( -. s .<_ W /\ -. s .<_ ( P .\/ Q ) ) -> u = ( ( P .\/ Q ) ./\ ( F .\/ ( ( t .\/ s ) ./\ W ) ) ) ) )
104 1 2 3 4 5 6 7 8 101 103 cdleme26f2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P =/= Q /\ t .<_ ( P .\/ Q ) ) /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( -. s .<_ ( P .\/ Q ) /\ ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> F .<_ ( E .\/ V ) )
105 90 93 94 95 96 97 98 99 100 104 syl333anc 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> F .<_ ( E .\/ V ) )
106 iffalse 
 |-  ( -. s .<_ ( P .\/ Q ) -> if ( s .<_ ( P .\/ Q ) , D , F ) = F )
107 12 106 syl5eq 
 |-  ( -. s .<_ ( P .\/ Q ) -> C = F )
108 107 ad2antrr 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C = F )
109 63 ad2antlr 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( Y .\/ V ) = ( E .\/ V ) )
110 105 108 109 3brtr4d 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C .<_ ( Y .\/ V ) )
111 110 ex 
 |-  ( ( -. s .<_ ( P .\/ Q ) /\ t .<_ ( P .\/ Q ) ) -> ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> C .<_ ( Y .\/ V ) ) )
112 simpr11 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( K e. HL /\ W e. H ) )
113 simpr23 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( t e. A /\ -. t .<_ W ) )
114 simplr 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> -. t .<_ ( P .\/ Q ) )
115 simpll 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> -. s .<_ ( P .\/ Q ) )
116 simpr12 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> P =/= Q )
117 114 115 116 3jca 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( -. t .<_ ( P .\/ Q ) /\ -. s .<_ ( P .\/ Q ) /\ P =/= Q ) )
118 simpr21 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( P e. A /\ -. P .<_ W ) )
119 simpr22 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
120 simpr13 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( s e. A /\ -. s .<_ W ) )
121 simpr3l 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( s =/= t /\ s .<_ ( t .\/ V ) ) )
122 simpr3r 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( V e. A /\ V .<_ W ) )
123 2 3 4 5 6 7 8 13 cdleme22g 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( t e. A /\ -. t .<_ W ) /\ ( -. t .<_ ( P .\/ Q ) /\ -. s .<_ ( P .\/ Q ) /\ P =/= Q ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( s e. A /\ -. s .<_ W ) /\ ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> F .<_ ( G .\/ V ) )
124 112 113 117 118 119 120 121 122 123 syl323anc 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> F .<_ ( G .\/ V ) )
125 107 ad2antrr 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C = F )
126 86 ad2antlr 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> ( Y .\/ V ) = ( G .\/ V ) )
127 124 125 126 3brtr4d 
 |-  ( ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) /\ ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) ) -> C .<_ ( Y .\/ V ) )
128 127 ex 
 |-  ( ( -. s .<_ ( P .\/ Q ) /\ -. t .<_ ( P .\/ Q ) ) -> ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> C .<_ ( Y .\/ V ) ) )
129 66 89 111 128 4cases 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ P =/= Q /\ ( s e. A /\ -. s .<_ W ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( t e. A /\ -. t .<_ W ) ) /\ ( ( s =/= t /\ s .<_ ( t .\/ V ) ) /\ ( V e. A /\ V .<_ W ) ) ) -> C .<_ ( Y .\/ V ) )