Metamath Proof Explorer

Theorem eqord1

Description: A strictly increasing 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 )
ltord.6 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x < y -> A < B ) )
Assertion eqord1 
|- ( ( 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 leord1 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C <_ D <-> M <_ N ) )
8 1 3 2 4 5 6 leord1 
 |-  ( ( ph /\ ( D e. S /\ C e. S ) ) -> ( D <_ C <-> N <_ M ) )
9 8 ancom2s 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( D <_ C <-> N <_ M ) )
10 7 9 anbi12d 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( ( C <_ D /\ D <_ C ) <-> ( M <_ N /\ N <_ M ) ) )
11 4 sseli 
 |-  ( C e. S -> C e. RR )
12 4 sseli 
 |-  ( D e. S -> D e. RR )
13 letri3 
 |-  ( ( C e. RR /\ D e. RR ) -> ( C = D <-> ( C <_ D /\ D <_ C ) ) )
14 11 12 13 syl2an 
 |-  ( ( C e. S /\ D e. S ) -> ( C = D <-> ( C <_ D /\ D <_ C ) ) )
15 14 adantl 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C = D <-> ( C <_ D /\ D <_ C ) ) )
16 5 ralrimiva 
 |-  ( ph -> A. x e. S A e. RR )
17 2 eleq1d 
 |-  ( x = C -> ( A e. RR <-> M e. RR ) )
18 17 rspccva 
 |-  ( ( A. x e. S A e. RR /\ C e. S ) -> M e. RR )
19 16 18 sylan 
 |-  ( ( ph /\ C e. S ) -> M e. RR )
20 19 adantrr 
 |-  ( ( ph /\ ( C e. S /\ D 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 16 22 sylan 
 |-  ( ( ph /\ D e. S ) -> N e. RR )
24 23 adantrl 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> N e. RR )
25 20 24 letri3d 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( M = N <-> ( M <_ N /\ N <_ M ) ) )
26 10 15 25 3bitr4d 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C = D <-> M = N ) )