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 ⊆ ℝ
ltord.5 ⊢ φ ∧ x ∈ S → A ∈ ℝ
ltord2.6 ⊢ φ ∧ x ∈ S ∧ y ∈ S → x < y → B < A
Assertion eqord2 ⊢ φ ∧ C ∈ S ∧ D ∈ 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 ⊆ ℝ
5 ltord.5 ⊢ φ ∧ x ∈ S → A ∈ ℝ
6 ltord2.6 ⊢ φ ∧ x ∈ S ∧ y ∈ S → x < y → B < A
7 1 negeqd ⊢ x = y → − A = − B
8 2 negeqd ⊢ x = C → − A = − M
9 3 negeqd ⊢ x = D → − A = − N
10 5 renegcld ⊢ φ ∧ x ∈ S → − A ∈ ℝ
11 5 ralrimiva ⊢ φ → ∀ x ∈ S A ∈ ℝ
12 1 eleq1d ⊢ x = y → A ∈ ℝ ↔ B ∈ ℝ
13 12 rspccva ⊢ ∀ x ∈ S A ∈ ℝ ∧ y ∈ S → B ∈ ℝ
14 11 13 sylan ⊢ φ ∧ y ∈ S → B ∈ ℝ
15 14 adantrl ⊢ φ ∧ x ∈ S ∧ y ∈ S → B ∈ ℝ
16 5 adantrr ⊢ φ ∧ x ∈ S ∧ y ∈ S → A ∈ ℝ
17 ltneg ⊢ B ∈ ℝ ∧ A ∈ ℝ → B < A ↔ − A < − B
18 15 16 17 syl2anc ⊢ φ ∧ x ∈ S ∧ y ∈ S → B < A ↔ − A < − B
19 6 18 sylibd ⊢ φ ∧ x ∈ S ∧ y ∈ S → x < y → − A < − B
20 7 8 9 4 10 19 eqord1 ⊢ φ ∧ C ∈ S ∧ D ∈ S → C = D ↔ − M = − N
21 2 eleq1d ⊢ x = C → A ∈ ℝ ↔ M ∈ ℝ
22 21 rspccva ⊢ ∀ x ∈ S A ∈ ℝ ∧ C ∈ S → M ∈ ℝ
23 11 22 sylan ⊢ φ ∧ C ∈ S → M ∈ ℝ
24 23 adantrr ⊢ φ ∧ C ∈ S ∧ D ∈ S → M ∈ ℝ
25 24 recnd ⊢ φ ∧ C ∈ S ∧ D ∈ S → M ∈ ℂ
26 3 eleq1d ⊢ x = D → A ∈ ℝ ↔ N ∈ ℝ
27 26 rspccva ⊢ ∀ x ∈ S A ∈ ℝ ∧ D ∈ S → N ∈ ℝ
28 11 27 sylan ⊢ φ ∧ D ∈ S → N ∈ ℝ
29 28 adantrl ⊢ φ ∧ C ∈ S ∧ D ∈ S → N ∈ ℝ
30 29 recnd ⊢ φ ∧ C ∈ S ∧ D ∈ S → N ∈ ℂ
31 25 30 neg11ad ⊢ φ ∧ C ∈ S ∧ D ∈ S → − M = − N ↔ M = N
32 20 31 bitrd ⊢ φ ∧ C ∈ S ∧ D ∈ S → C = D ↔ M = N