Metamath Proof Explorer

Theorem cdleme40n

Description: Part of proof of Lemma E in Crawley p. 113. Show that f(x) is one-to-one on P .\/ Q line. TODO: FIX COMMENT. TODO get rid of '.<' class? (Contributed by NM, 18-Mar-2013)

Ref Expression
Hypotheses cdleme40.b 
|- B = ( Base ` K )
cdleme40.l 
|- .<_ = ( le ` K )
cdleme40.j 
|- .\/ = ( join ` K )
cdleme40.m 
|- ./\ = ( meet ` K )
cdleme40.a 
|- A = ( Atoms ` K )
cdleme40.h 
|- H = ( LHyp ` K )
cdleme40.u 
|- U = ( ( P .\/ Q ) ./\ W )
cdleme40.e 
|- E = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
cdleme40.g 
|- G = ( ( P .\/ Q ) ./\ ( E .\/ ( ( s .\/ t ) ./\ W ) ) )
cdleme40.i 
|- I = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) )
cdleme40.n 
|- N = if ( s .<_ ( P .\/ Q ) , I , D )
cdleme40a1.y 
|- Y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( R .\/ t ) ./\ W ) ) )
cdleme40a1.c 
|- C = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = Y ) )
cdleme40.t 
|- T = ( ( v .\/ U ) ./\ ( Q .\/ ( ( P .\/ v ) ./\ W ) ) )
cdleme40.f 
|- F = ( ( P .\/ Q ) ./\ ( T .\/ ( ( S .\/ v ) ./\ W ) ) )
cdleme40a1.x 
|- X = ( ( P .\/ Q ) ./\ ( T .\/ ( ( u .\/ v ) ./\ W ) ) )
cdleme40.o 
|- O = ( iota_ z e. B A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = X ) )
cdleme40.v 
|- V = if ( u .<_ ( P .\/ Q ) , O , .< )
cdleme40a1.z 
|- Z = ( iota_ z e. B A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = F ) )
Assertion cdleme40n 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> [_ R / s ]_ N =/= [_ S / u ]_ V )

Proof

Step Hyp Ref Expression
1 cdleme40.b 
 |-  B = ( Base ` K )
2 cdleme40.l 
 |-  .<_ = ( le ` K )
3 cdleme40.j 
 |-  .\/ = ( join ` K )
4 cdleme40.m 
 |-  ./\ = ( meet ` K )
5 cdleme40.a 
 |-  A = ( Atoms ` K )
6 cdleme40.h 
 |-  H = ( LHyp ` K )
7 cdleme40.u 
 |-  U = ( ( P .\/ Q ) ./\ W )
8 cdleme40.e 
 |-  E = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
9 cdleme40.g 
 |-  G = ( ( P .\/ Q ) ./\ ( E .\/ ( ( s .\/ t ) ./\ W ) ) )
10 cdleme40.i 
 |-  I = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) )
11 cdleme40.n 
 |-  N = if ( s .<_ ( P .\/ Q ) , I , D )
12 cdleme40a1.y 
 |-  Y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( R .\/ t ) ./\ W ) ) )
13 cdleme40a1.c 
 |-  C = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = Y ) )
14 cdleme40.t 
 |-  T = ( ( v .\/ U ) ./\ ( Q .\/ ( ( P .\/ v ) ./\ W ) ) )
15 cdleme40.f 
 |-  F = ( ( P .\/ Q ) ./\ ( T .\/ ( ( S .\/ v ) ./\ W ) ) )
16 cdleme40a1.x 
 |-  X = ( ( P .\/ Q ) ./\ ( T .\/ ( ( u .\/ v ) ./\ W ) ) )
17 cdleme40.o 
 |-  O = ( iota_ z e. B A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = X ) )
18 cdleme40.v 
 |-  V = if ( u .<_ ( P .\/ Q ) , O , .< )
19 cdleme40a1.z 
 |-  Z = ( iota_ z e. B A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = F ) )
20 1 fvexi 
 |-  B e. _V
21 nfv 
 |-  F/ v ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) )
22 nfcv 
 |-  F/_ v [_ R / s ]_ N
23 nfra1 
 |-  F/ v A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = F )
24 nfcv 
 |-  F/_ v B
25 23 24 nfriota 
 |-  F/_ v ( iota_ z e. B A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = F ) )
26 19 25 nfcxfr 
 |-  F/_ v Z
27 22 26 nfne 
 |-  F/ v [_ R / s ]_ N =/= Z
28 27 a1i 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> F/ v [_ R / s ]_ N =/= Z )
29 19 a1i 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> Z = ( iota_ z e. B A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = F ) ) )
30 neeq2 
 |-  ( F = Z -> ( [_ R / s ]_ N =/= F <-> [_ R / s ]_ N =/= Z ) )
31 30 adantl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) /\ F = Z ) -> ( [_ R / s ]_ N =/= F <-> [_ R / s ]_ N =/= Z ) )
32 simpl11 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) /\ ( v e. A /\ ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) ) -> ( K e. HL /\ W e. H ) )
33 simpl12 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) /\ ( v e. A /\ ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) ) -> ( P e. A /\ -. P .<_ W ) )
34 simpl13 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) /\ ( v e. A /\ ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
35 simpl21 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) /\ ( v e. A /\ ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) ) -> P =/= Q )
36 simpl22 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) /\ ( v e. A /\ ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) ) -> ( R e. A /\ -. R .<_ W ) )
37 simpl23 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) /\ ( v e. A /\ ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) ) -> ( S e. A /\ -. S .<_ W ) )
38 simpl3 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) /\ ( v e. A /\ ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) ) -> ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) )
39 simprl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) /\ ( v e. A /\ ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) ) -> v e. A )
40 simprrl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) /\ ( v e. A /\ ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) ) -> -. v .<_ W )
41 simprrr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) /\ ( v e. A /\ ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) ) -> -. v .<_ ( P .\/ Q ) )
42 39 40 41 3jca 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) /\ ( v e. A /\ ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) ) -> ( v e. A /\ -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) )
43 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 cdleme40m 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) /\ ( v e. A /\ -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) ) -> [_ R / s ]_ N =/= F )
44 32 33 34 35 36 37 38 42 43 syl332anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) /\ ( v e. A /\ ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) ) -> [_ R / s ]_ N =/= F )
45 44 ex 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> ( ( v e. A /\ ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) ) -> [_ R / s ]_ N =/= F ) )
46 simp1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) )
47 simp23l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> S e. A )
48 simp23r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> -. S .<_ W )
49 simp21 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> P =/= Q )
50 simp32 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> S .<_ ( P .\/ Q ) )
51 1 2 3 4 5 6 7 14 15 19 cdleme25cl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ -. S .<_ W ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> Z e. B )
52 46 47 48 49 50 51 syl122anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> Z e. B )
53 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> ( K e. HL /\ W e. H ) )
54 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> ( P e. A /\ -. P .<_ W ) )
55 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> ( Q e. A /\ -. Q .<_ W ) )
56 2 3 5 6 cdlemb2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> E. v e. A ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) )
57 53 54 55 49 56 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> E. v e. A ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) )
58 21 28 29 31 45 52 57 riotasv3d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) /\ B e. _V ) -> [_ R / s ]_ N =/= Z )
59 20 58 mpan2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> [_ R / s ]_ N =/= Z )
60 16 17 18 15 19 cdleme31sn1c 
 |-  ( ( S e. A /\ S .<_ ( P .\/ Q ) ) -> [_ S / u ]_ V = Z )
61 47 50 60 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> [_ S / u ]_ V = Z )
62 59 61 neeqtrrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ S .<_ ( P .\/ Q ) /\ R =/= S ) ) -> [_ R / s ]_ N =/= [_ S / u ]_ V )