Metamath Proof Explorer

Theorem leord1

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