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