This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqord2

Description: A strictly decreasing real function on a subset of RR is one-to-one. (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 )
ltord2.6 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x < y -> B < A ) )
Assertion eqord2 
|- ( ( 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 ltord2.6 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x < y -> B < A ) )
7 1 negeqd 
 |-  ( x = y -> -u A = -u B )
8 2 negeqd 
 |-  ( x = C -> -u A = -u M )
9 3 negeqd 
 |-  ( x = D -> -u A = -u N )
10 5 renegcld 
 |-  ( ( ph /\ x e. S ) -> -u A e. RR )
11 5 ralrimiva 
 |-  ( ph -> A. x e. S A e. RR )
12 1 eleq1d 
 |-  ( x = y -> ( A e. RR <-> B e. RR ) )
13 12 rspccva 
 |-  ( ( A. x e. S A e. RR /\ y e. S ) -> B e. RR )
14 11 13 sylan 
 |-  ( ( ph /\ y e. S ) -> B e. RR )
15 14 adantrl 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> B e. RR )
16 5 adantrr 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> A e. RR )
17 ltneg 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B < A <-> -u A < -u B ) )
18 15 16 17 syl2anc 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( B < A <-> -u A < -u B ) )
19 6 18 sylibd 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x < y -> -u A < -u B ) )
20 7 8 9 4 10 19 eqord1 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C = D <-> -u M = -u N ) )
21 2 eleq1d 
 |-  ( x = C -> ( A e. RR <-> M e. RR ) )
22 21 rspccva 
 |-  ( ( A. x e. S A e. RR /\ C e. S ) -> M e. RR )
23 11 22 sylan 
 |-  ( ( ph /\ C e. S ) -> M e. RR )
24 23 adantrr 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> M e. RR )
25 24 recnd 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> M e. CC )
26 3 eleq1d 
 |-  ( x = D -> ( A e. RR <-> N e. RR ) )
27 26 rspccva 
 |-  ( ( A. x e. S A e. RR /\ D e. S ) -> N e. RR )
28 11 27 sylan 
 |-  ( ( ph /\ D e. S ) -> N e. RR )
29 28 adantrl 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> N e. RR )
30 29 recnd 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> N e. CC )
31 25 30 neg11ad 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( -u M = -u N <-> M = N ) )
32 20 31 bitrd 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C = D <-> M = N ) )