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	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
	ltord.2	⊢ ( 𝑥 = 𝐶 → 𝐴 = 𝑀 )
	ltord.3	⊢ ( 𝑥 = 𝐷 → 𝐴 = 𝑁 )
	ltord.4	⊢ 𝑆 ⊆ ℝ
	ltord.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
	ltord2.6	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 < 𝑦 → 𝐵 < 𝐴 ) )
Assertion	eqord2	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 = 𝐷 ↔ 𝑀 = 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		ltord.1	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
2		ltord.2	⊢ ( 𝑥 = 𝐶 → 𝐴 = 𝑀 )
3		ltord.3	⊢ ( 𝑥 = 𝐷 → 𝐴 = 𝑁 )
4		ltord.4	⊢ 𝑆 ⊆ ℝ
5		ltord.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
6		ltord2.6	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 < 𝑦 → 𝐵 < 𝐴 ) )
7	1	negeqd	⊢ ( 𝑥 = 𝑦 → - 𝐴 = - 𝐵 )
8	2	negeqd	⊢ ( 𝑥 = 𝐶 → - 𝐴 = - 𝑀 )
9	3	negeqd	⊢ ( 𝑥 = 𝐷 → - 𝐴 = - 𝑁 )
10	5	renegcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → - 𝐴 ∈ ℝ )
11	5	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ )
12	1	eleq1d	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ ℝ ↔ 𝐵 ∈ ℝ ) )
13	12	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ ∧ 𝑦 ∈ 𝑆 ) → 𝐵 ∈ ℝ )
14	11 13	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝐵 ∈ ℝ )
15	14	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝐵 ∈ ℝ )
16	5	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝐴 ∈ ℝ )
17		ltneg	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ - 𝐴 < - 𝐵 ) )
18	15 16 17	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝐵 < 𝐴 ↔ - 𝐴 < - 𝐵 ) )
19	6 18	sylibd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 < 𝑦 → - 𝐴 < - 𝐵 ) )
20	7 8 9 4 10 19	eqord1	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 = 𝐷 ↔ - 𝑀 = - 𝑁 ) )
21	2	eleq1d	⊢ ( 𝑥 = 𝐶 → ( 𝐴 ∈ ℝ ↔ 𝑀 ∈ ℝ ) )
22	21	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ ∧ 𝐶 ∈ 𝑆 ) → 𝑀 ∈ ℝ )
23	11 22	sylan	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑆 ) → 𝑀 ∈ ℝ )
24	23	adantrr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → 𝑀 ∈ ℝ )
25	24	recnd	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → 𝑀 ∈ ℂ )
26	3	eleq1d	⊢ ( 𝑥 = 𝐷 → ( 𝐴 ∈ ℝ ↔ 𝑁 ∈ ℝ ) )
27	26	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ ∧ 𝐷 ∈ 𝑆 ) → 𝑁 ∈ ℝ )
28	11 27	sylan	⊢ ( ( 𝜑 ∧ 𝐷 ∈ 𝑆 ) → 𝑁 ∈ ℝ )
29	28	adantrl	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → 𝑁 ∈ ℝ )
30	29	recnd	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → 𝑁 ∈ ℂ )
31	25 30	neg11ad	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( - 𝑀 = - 𝑁 ↔ 𝑀 = 𝑁 ) )
32	20 31	bitrd	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 = 𝐷 ↔ 𝑀 = 𝑁 ) )