Metamath Proof Explorer

Theorem leord2

Description: Infer an ordering relation from a proof in only one direction. (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 ∈ ℝ
ltord2.6 ⊢ φ ∧ x ∈ S ∧ y ∈ S → x < y → B < A
Assertion leord2 ⊢ φ ∧ C ∈ S ∧ D ∈ S → C ≤ D ↔ N ≤ M

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 ltord2.6 ⊢ φ ∧ x ∈ S ∧ y ∈ S → x < y → B < A
7 1 negeqd ⊢ x = y → − A = − B
8 2 negeqd ⊢ x = C → − A = − M
9 3 negeqd ⊢ x = D → − A = − N
10 5 renegcld ⊢ φ ∧ x ∈ S → − A ∈ ℝ
11 5 ralrimiva ⊢ φ → ∀ x ∈ S A ∈ ℝ
12 1 eleq1d ⊢ x = y → A ∈ ℝ ↔ B ∈ ℝ
13 12 rspccva ⊢ ∀ x ∈ S A ∈ ℝ ∧ y ∈ S → B ∈ ℝ
14 11 13 sylan ⊢ φ ∧ y ∈ S → B ∈ ℝ
15 14 adantrl ⊢ φ ∧ x ∈ S ∧ y ∈ S → B ∈ ℝ
16 5 adantrr ⊢ φ ∧ x ∈ S ∧ y ∈ S → A ∈ ℝ
17 ltneg ⊢ B ∈ ℝ ∧ A ∈ ℝ → B < A ↔ − A < − B
18 15 16 17 syl2anc ⊢ φ ∧ x ∈ S ∧ y ∈ S → B < A ↔ − A < − B
19 6 18 sylibd ⊢ φ ∧ x ∈ S ∧ y ∈ S → x < y → − A < − B
20 7 8 9 4 10 19 leord1 ⊢ φ ∧ C ∈ S ∧ D ∈ S → C ≤ D ↔ − M ≤ − N
21 3 eleq1d ⊢ x = D → A ∈ ℝ ↔ N ∈ ℝ
22 21 rspccva ⊢ ∀ x ∈ S A ∈ ℝ ∧ D ∈ S → N ∈ ℝ
23 11 22 sylan ⊢ φ ∧ D ∈ S → N ∈ ℝ
24 23 adantrl ⊢ φ ∧ C ∈ S ∧ D ∈ S → N ∈ ℝ
25 2 eleq1d ⊢ x = C → A ∈ ℝ ↔ M ∈ ℝ
26 25 rspccva ⊢ ∀ x ∈ S A ∈ ℝ ∧ C ∈ S → M ∈ ℝ
27 11 26 sylan ⊢ φ ∧ C ∈ S → M ∈ ℝ
28 27 adantrr ⊢ φ ∧ C ∈ S ∧ D ∈ S → M ∈ ℝ
29 leneg ⊢ N ∈ ℝ ∧ M ∈ ℝ → N ≤ M ↔ − M ≤ − N
30 24 28 29 syl2anc ⊢ φ ∧ C ∈ S ∧ D ∈ S → N ≤ M ↔ − M ≤ − N
31 20 30 bitr4d ⊢ φ ∧ C ∈ S ∧ D ∈ S → C ≤ D ↔ N ≤ M