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 ⊢ x = y → A = B
ltord.2 ⊢ x = C → A = M
ltord.3 ⊢ x = D → A = N
ltord.4 ⊢ S ⊆ ℝ
ltord.5 ⊢ φ ∧ x ∈ S → A ∈ ℝ
ltord.6 ⊢ φ ∧ x ∈ S ∧ y ∈ S → x < y → A < B
Assertion eqord1 ⊢ φ ∧ 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 ltord.6 ⊢ φ ∧ x ∈ S ∧ y ∈ S → x < y → A < B
7 1 2 3 4 5 6 leord1 ⊢ φ ∧ C ∈ S ∧ D ∈ S → C ≤ D ↔ M ≤ N
8 1 3 2 4 5 6 leord1 ⊢ φ ∧ D ∈ S ∧ C ∈ S → D ≤ C ↔ N ≤ M
9 8 ancom2s ⊢ φ ∧ C ∈ S ∧ D ∈ S → D ≤ C ↔ N ≤ M
10 7 9 anbi12d ⊢ φ ∧ C ∈ S ∧ D ∈ S → C ≤ D ∧ D ≤ C ↔ M ≤ N ∧ N ≤ M
11 4 sseli ⊢ C ∈ S → C ∈ ℝ
12 4 sseli ⊢ D ∈ S → D ∈ ℝ
13 letri3 ⊢ C ∈ ℝ ∧ D ∈ ℝ → C = D ↔ C ≤ D ∧ D ≤ C
14 11 12 13 syl2an ⊢ C ∈ S ∧ D ∈ S → C = D ↔ C ≤ D ∧ D ≤ C
15 14 adantl ⊢ φ ∧ C ∈ S ∧ D ∈ S → C = D ↔ C ≤ D ∧ D ≤ C
16 5 ralrimiva ⊢ φ → ∀ x ∈ S A ∈ ℝ
17 2 eleq1d ⊢ x = C → A ∈ ℝ ↔ M ∈ ℝ
18 17 rspccva ⊢ ∀ x ∈ S A ∈ ℝ ∧ C ∈ S → M ∈ ℝ
19 16 18 sylan ⊢ φ ∧ C ∈ S → M ∈ ℝ
20 19 adantrr ⊢ φ ∧ C ∈ S ∧ D ∈ S → M ∈ ℝ
21 3 eleq1d ⊢ x = D → A ∈ ℝ ↔ N ∈ ℝ
22 21 rspccva ⊢ ∀ x ∈ S A ∈ ℝ ∧ D ∈ S → N ∈ ℝ
23 16 22 sylan ⊢ φ ∧ D ∈ S → N ∈ ℝ
24 23 adantrl ⊢ φ ∧ C ∈ S ∧ D ∈ S → N ∈ ℝ
25 20 24 letri3d ⊢ φ ∧ C ∈ S ∧ D ∈ S → M = N ↔ M ≤ N ∧ N ≤ M
26 10 15 25 3bitr4d ⊢ φ ∧ C ∈ S ∧ D ∈ S → C = D ↔ M = N