Metamath Proof Explorer


Theorem leord2

Description: Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Hypotheses ltord.1 x=yA=B
ltord.2 x=CA=M
ltord.3 x=DA=N
ltord.4 S
ltord.5 φxSA
ltord2.6 φxSySx<yB<A
Assertion leord2 φCSDSCDNM

Proof

Step Hyp Ref Expression
1 ltord.1 x=yA=B
2 ltord.2 x=CA=M
3 ltord.3 x=DA=N
4 ltord.4 S
5 ltord.5 φxSA
6 ltord2.6 φxSySx<yB<A
7 1 negeqd x=yA=B
8 2 negeqd x=CA=M
9 3 negeqd x=DA=N
10 5 renegcld φxSA
11 5 ralrimiva φxSA
12 1 eleq1d x=yAB
13 12 rspccva xSAySB
14 11 13 sylan φySB
15 14 adantrl φxSySB
16 5 adantrr φxSySA
17 ltneg BAB<AA<B
18 15 16 17 syl2anc φxSySB<AA<B
19 6 18 sylibd φxSySx<yA<B
20 7 8 9 4 10 19 leord1 φCSDSCDMN
21 3 eleq1d x=DAN
22 21 rspccva xSADSN
23 11 22 sylan φDSN
24 23 adantrl φCSDSN
25 2 eleq1d x=CAM
26 25 rspccva xSACSM
27 11 26 sylan φCSM
28 27 adantrr φCSDSM
29 leneg NMNMMN
30 24 28 29 syl2anc φCSDSNMMN
31 20 30 bitr4d φCSDSCDNM