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 = y A = B
ltord.2 x = C A = M
ltord.3 x = D A = N
ltord.4 S
ltord.5 φ x S A
ltord2.6 φ x S y S x < y B < A
Assertion leord2 φ C S D S C D N M

Proof

Step Hyp Ref Expression
1 ltord.1 x = y A = B
2 ltord.2 x = C A = M
3 ltord.3 x = D A = N
4 ltord.4 S
5 ltord.5 φ x S A
6 ltord2.6 φ x S y S x < y B < A
7 1 negeqd x = y A = B
8 2 negeqd x = C A = M
9 3 negeqd x = D A = N
10 5 renegcld φ x S A
11 5 ralrimiva φ x S A
12 1 eleq1d x = y A B
13 12 rspccva x S A y S B
14 11 13 sylan φ y S B
15 14 adantrl φ x S y S B
16 5 adantrr φ x S y S A
17 ltneg B A B < A A < B
18 15 16 17 syl2anc φ x S y S B < A A < B
19 6 18 sylibd φ x S y S x < y A < B
20 7 8 9 4 10 19 leord1 φ C S D S C D M N
21 3 eleq1d x = D A N
22 21 rspccva x S A D S N
23 11 22 sylan φ D S N
24 23 adantrl φ C S D S N
25 2 eleq1d x = C A M
26 25 rspccva x S A C S M
27 11 26 sylan φ C S M
28 27 adantrr φ C S D S M
29 leneg N M N M M N
30 24 28 29 syl2anc φ C S D S N M M N
31 20 30 bitr4d φ C S D S C D N M