Metamath Proof Explorer


Theorem leord1

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
ltord.6 φxSySx<yA<B
Assertion leord1 φCSDSCDMN

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 ltord.6 φxSySx<yA<B
7 1 3 2 4 5 6 ltord1 φDSCSD<CN<M
8 7 ancom2s φCSDSD<CN<M
9 8 notbid φCSDS¬D<C¬N<M
10 4 sseli CSC
11 4 sseli DSD
12 lenlt CDCD¬D<C
13 10 11 12 syl2an CSDSCD¬D<C
14 13 adantl φCSDSCD¬D<C
15 5 ralrimiva φxSA
16 2 eleq1d x=CAM
17 16 rspccva xSACSM
18 15 17 sylan φCSM
19 18 adantrr φCSDSM
20 3 eleq1d x=DAN
21 20 rspccva xSADSN
22 15 21 sylan φDSN
23 22 adantrl φCSDSN
24 19 23 lenltd φCSDSMN¬N<M
25 9 14 24 3bitr4d φCSDSCDMN