Metamath Proof Explorer

Theorem ltord1

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 ltord1 
|- ( ( 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 2 3 4 5 6 ltordlem 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C < D -> M < N ) )
8 eqeq1 
 |-  ( x = C -> ( x = D <-> C = D ) )
9 2 eqeq1d 
 |-  ( x = C -> ( A = N <-> M = N ) )
10 8 9 imbi12d 
 |-  ( x = C -> ( ( x = D -> A = N ) <-> ( C = D -> M = N ) ) )
11 10 3 vtoclg 
 |-  ( C e. S -> ( C = D -> M = N ) )
12 11 ad2antrl 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C = D -> M = N ) )
13 1 3 2 4 5 6 ltordlem 
 |-  ( ( ph /\ ( D e. S /\ C e. S ) ) -> ( D < C -> N < M ) )
14 13 ancom2s 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( D < C -> N < M ) )
15 12 14 orim12d 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( ( C = D \/ D < C ) -> ( M = N \/ N < M ) ) )
16 15 con3d 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( -. ( M = N \/ N < M ) -> -. ( C = D \/ D < C ) ) )
17 5 ralrimiva 
 |-  ( ph -> A. x e. S A e. RR )
18 2 eleq1d 
 |-  ( x = C -> ( A e. RR <-> M e. RR ) )
19 18 rspccva 
 |-  ( ( A. x e. S A e. RR /\ C e. S ) -> M e. RR )
20 17 19 sylan 
 |-  ( ( ph /\ C e. S ) -> M e. RR )
21 3 eleq1d 
 |-  ( x = D -> ( A e. RR <-> N e. RR ) )
22 21 rspccva 
 |-  ( ( A. x e. S A e. RR /\ D e. S ) -> N e. RR )
23 17 22 sylan 
 |-  ( ( ph /\ D e. S ) -> N e. RR )
24 20 23 anim12dan 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( M e. RR /\ N e. RR ) )
25 axlttri 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M < N <-> -. ( M = N \/ N < M ) ) )
26 24 25 syl 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( M < N <-> -. ( M = N \/ N < M ) ) )
27 4 sseli 
 |-  ( C e. S -> C e. RR )
28 4 sseli 
 |-  ( D e. S -> D e. RR )
29 axlttri 
 |-  ( ( C e. RR /\ D e. RR ) -> ( C < D <-> -. ( C = D \/ D < C ) ) )
30 27 28 29 syl2an 
 |-  ( ( C e. S /\ D e. S ) -> ( C < D <-> -. ( C = D \/ D < C ) ) )
31 30 adantl 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C < D <-> -. ( C = D \/ D < C ) ) )
32 16 26 31 3imtr4d 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( M < N -> C < D ) )
33 7 32 impbid 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C < D <-> M < N ) )