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∈SA∈ℝ
17 2 eleq1d ⊢x=C→A∈ℝ↔M∈ℝ
18 17 rspccva ⊢∀x∈SA∈ℝ∧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∈SA∈ℝ∧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