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 \to A = B$
	ltord.2	$⊢ x = C \to A = M$
	ltord.3	$⊢ x = D \to A = N$
	ltord.4	$⊢ S \subseteq ℝ$
	ltord.5	$⊢ (φ \land x \in S) \to A \in ℝ$
	ltord2.6	$⊢ (φ \land (x \in S \land y \in S)) \to (x < y \to B < A)$
Assertion	eqord2	$⊢ (φ \land (C \in S \land D \in S)) \to (C = D \leftrightarrow M = N)$

Proof

Step	Hyp	Ref	Expression
1		ltord.1	$⊢ x = y \to A = B$
2		ltord.2	$⊢ x = C \to A = M$
3		ltord.3	$⊢ x = D \to A = N$
4		ltord.4	$⊢ S \subseteq ℝ$
5		ltord.5	$⊢ (φ \land x \in S) \to A \in ℝ$
6		ltord2.6	$⊢ (φ \land (x \in S \land y \in S)) \to (x < y \to B < A)$
7	1	negeqd	$⊢ x = y \to - A = - B$
8	2	negeqd	$⊢ x = C \to - A = - M$
9	3	negeqd	$⊢ x = D \to - A = - N$
10	5	renegcld	$⊢ (φ \land x \in S) \to - A \in ℝ$
11	5	ralrimiva	$⊢ φ \to \forall x \in S A \in ℝ$
12	1	eleq1d	$⊢ x = y \to (A \in ℝ \leftrightarrow B \in ℝ)$
13	12	rspccva	$⊢ (\forall x \in S A \in ℝ \land y \in S) \to B \in ℝ$
14	11 13	sylan	$⊢ (φ \land y \in S) \to B \in ℝ$
15	14	adantrl	$⊢ (φ \land (x \in S \land y \in S)) \to B \in ℝ$
16	5	adantrr	$⊢ (φ \land (x \in S \land y \in S)) \to A \in ℝ$
17		ltneg	$⊢ (B \in ℝ \land A \in ℝ) \to (B < A \leftrightarrow - A < - B)$
18	15 16 17	syl2anc	$⊢ (φ \land (x \in S \land y \in S)) \to (B < A \leftrightarrow - A < - B)$
19	6 18	sylibd	$⊢ (φ \land (x \in S \land y \in S)) \to (x < y \to - A < - B)$
20	7 8 9 4 10 19	eqord1	$⊢ (φ \land (C \in S \land D \in S)) \to (C = D \leftrightarrow - M = - N)$
21	2	eleq1d	$⊢ x = C \to (A \in ℝ \leftrightarrow M \in ℝ)$
22	21	rspccva	$⊢ (\forall x \in S A \in ℝ \land C \in S) \to M \in ℝ$
23	11 22	sylan	$⊢ (φ \land C \in S) \to M \in ℝ$
24	23	adantrr	$⊢ (φ \land (C \in S \land D \in S)) \to M \in ℝ$
25	24	recnd	$⊢ (φ \land (C \in S \land D \in S)) \to M \in ℂ$
26	3	eleq1d	$⊢ x = D \to (A \in ℝ \leftrightarrow N \in ℝ)$
27	26	rspccva	$⊢ (\forall x \in S A \in ℝ \land D \in S) \to N \in ℝ$
28	11 27	sylan	$⊢ (φ \land D \in S) \to N \in ℝ$
29	28	adantrl	$⊢ (φ \land (C \in S \land D \in S)) \to N \in ℝ$
30	29	recnd	$⊢ (φ \land (C \in S \land D \in S)) \to N \in ℂ$
31	25 30	neg11ad	$⊢ (φ \land (C \in S \land D \in S)) \to (- M = - N \leftrightarrow M = N)$
32	20 31	bitrd	$⊢ (φ \land (C \in S \land D \in S)) \to (C = D \leftrightarrow M = N)$

Metamath Proof Explorer

Theorem eqord2

Proof