This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
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 ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 = 𝐷 ↔ 𝑀 = 𝑁 ) )