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 = y -> A = B )
ltord.2
|- ( x = C -> A = M )
ltord.3
|- ( x = D -> A = N )
ltord.4
|- S C_ RR
ltord.5
|- ( ( ph /\ x e. S ) -> A e. RR )
ltord.6
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x < y -> A < B ) )
Assertion leord1
|- ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C <_ D <-> M <_ N ) )

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 C_ RR
5 ltord.5
 |-  ( ( ph /\ x e. S ) -> A e. RR )
6 ltord.6
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x < y -> A < B ) )
7 1 3 2 4 5 6 ltord1
 |-  ( ( ph /\ ( D e. S /\ C e. S ) ) -> ( D < C <-> N < M ) )
8 7 ancom2s
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( D < C <-> N < M ) )
9 8 notbid
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( -. D < C <-> -. N < M ) )
10 4 sseli
 |-  ( C e. S -> C e. RR )
11 4 sseli
 |-  ( D e. S -> D e. RR )
12 lenlt
 |-  ( ( C e. RR /\ D e. RR ) -> ( C <_ D <-> -. D < C ) )
13 10 11 12 syl2an
 |-  ( ( C e. S /\ D e. S ) -> ( C <_ D <-> -. D < C ) )
14 13 adantl
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C <_ D <-> -. D < C ) )
15 5 ralrimiva
 |-  ( ph -> A. x e. S A e. RR )
16 2 eleq1d
 |-  ( x = C -> ( A e. RR <-> M e. RR ) )
17 16 rspccva
 |-  ( ( A. x e. S A e. RR /\ C e. S ) -> M e. RR )
18 15 17 sylan
 |-  ( ( ph /\ C e. S ) -> M e. RR )
19 18 adantrr
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> M e. RR )
20 3 eleq1d
 |-  ( x = D -> ( A e. RR <-> N e. RR ) )
21 20 rspccva
 |-  ( ( A. x e. S A e. RR /\ D e. S ) -> N e. RR )
22 15 21 sylan
 |-  ( ( ph /\ D e. S ) -> N e. RR )
23 22 adantrl
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> N e. RR )
24 19 23 lenltd
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( M <_ N <-> -. N < M ) )
25 9 14 24 3bitr4d
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C <_ D <-> M <_ N ) )