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

Proof

Step	Hyp	Ref	Expression
1		ltord.1	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
2		ltord.2	⊢ ( 𝑥 = 𝐶 → 𝐴 = 𝑀 )
3		ltord.3	⊢ ( 𝑥 = 𝐷 → 𝐴 = 𝑁 )
4		ltord.4	⊢ 𝑆 ⊆ ℝ
5		ltord.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
6		ltord.6	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 < 𝑦 → 𝐴 < 𝐵 ) )
7	1 2 3 4 5 6	leord1	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 ≤ 𝐷 ↔ 𝑀 ≤ 𝑁 ) )
8	1 3 2 4 5 6	leord1	⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ) → ( 𝐷 ≤ 𝐶 ↔ 𝑁 ≤ 𝑀 ) )
9	8	ancom2s	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐷 ≤ 𝐶 ↔ 𝑁 ≤ 𝑀 ) )
10	7 9	anbi12d	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ( 𝐶 ≤ 𝐷 ∧ 𝐷 ≤ 𝐶 ) ↔ ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) )
11	4	sseli	⊢ ( 𝐶 ∈ 𝑆 → 𝐶 ∈ ℝ )
12	4	sseli	⊢ ( 𝐷 ∈ 𝑆 → 𝐷 ∈ ℝ )
13		letri3	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐶 = 𝐷 ↔ ( 𝐶 ≤ 𝐷 ∧ 𝐷 ≤ 𝐶 ) ) )
14	11 12 13	syl2an	⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) → ( 𝐶 = 𝐷 ↔ ( 𝐶 ≤ 𝐷 ∧ 𝐷 ≤ 𝐶 ) ) )
15	14	adantl	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 = 𝐷 ↔ ( 𝐶 ≤ 𝐷 ∧ 𝐷 ≤ 𝐶 ) ) )
16	5	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ )
17	2	eleq1d	⊢ ( 𝑥 = 𝐶 → ( 𝐴 ∈ ℝ ↔ 𝑀 ∈ ℝ ) )
18	17	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ ∧ 𝐶 ∈ 𝑆 ) → 𝑀 ∈ ℝ )
19	16 18	sylan	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑆 ) → 𝑀 ∈ ℝ )
20	19	adantrr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → 𝑀 ∈ ℝ )
21	3	eleq1d	⊢ ( 𝑥 = 𝐷 → ( 𝐴 ∈ ℝ ↔ 𝑁 ∈ ℝ ) )
22	21	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ ∧ 𝐷 ∈ 𝑆 ) → 𝑁 ∈ ℝ )
23	16 22	sylan	⊢ ( ( 𝜑 ∧ 𝐷 ∈ 𝑆 ) → 𝑁 ∈ ℝ )
24	23	adantrl	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → 𝑁 ∈ ℝ )
25	20 24	letri3d	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝑀 = 𝑁 ↔ ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) )
26	10 15 25	3bitr4d	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 = 𝐷 ↔ 𝑀 = 𝑁 ) )