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

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 ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
ltord.2 ⊢ ( 𝑥 = 𝐶 → 𝐴 = 𝑀 )
ltord.3 ⊢ ( 𝑥 = 𝐷 → 𝐴 = 𝑁 )
ltord.4 ⊢ 𝑆 ⊆ ℝ
ltord.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
ltord.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 < 𝑦 → 𝐴 < 𝐵 ) )
Assertion leord1 ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 ≤ 𝐷 ↔ 𝑀 ≤ 𝑁 ) )

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 3 2 4 5 6 ltord1 ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ) → ( 𝐷 < 𝐶 ↔ 𝑁 < 𝑀 ) )
8 7 ancom2s ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐷 < 𝐶 ↔ 𝑁 < 𝑀 ) )
9 8 notbid ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ¬ 𝐷 < 𝐶 ↔ ¬ 𝑁 < 𝑀 ) )
10 4 sseli ⊢ ( 𝐶 ∈ 𝑆 → 𝐶 ∈ ℝ )
11 4 sseli ⊢ ( 𝐷 ∈ 𝑆 → 𝐷 ∈ ℝ )
12 lenlt ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐶 ≤ 𝐷 ↔ ¬ 𝐷 < 𝐶 ) )
13 10 11 12 syl2an ⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) → ( 𝐶 ≤ 𝐷 ↔ ¬ 𝐷 < 𝐶 ) )
14 13 adantl ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 ≤ 𝐷 ↔ ¬ 𝐷 < 𝐶 ) )
15 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ )
16 2 eleq1d ⊢ ( 𝑥 = 𝐶 → ( 𝐴 ∈ ℝ ↔ 𝑀 ∈ ℝ ) )
17 16 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ ∧ 𝐶 ∈ 𝑆 ) → 𝑀 ∈ ℝ )
18 15 17 sylan ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑆 ) → 𝑀 ∈ ℝ )
19 18 adantrr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → 𝑀 ∈ ℝ )
20 3 eleq1d ⊢ ( 𝑥 = 𝐷 → ( 𝐴 ∈ ℝ ↔ 𝑁 ∈ ℝ ) )
21 20 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ ∧ 𝐷 ∈ 𝑆 ) → 𝑁 ∈ ℝ )
22 15 21 sylan ⊢ ( ( 𝜑 ∧ 𝐷 ∈ 𝑆 ) → 𝑁 ∈ ℝ )
23 22 adantrl ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → 𝑁 ∈ ℝ )
24 19 23 lenltd ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) )
25 9 14 24 3bitr4d ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 ≤ 𝐷 ↔ 𝑀 ≤ 𝑁 ) )