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 ) )