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 ( ( 𝜑 ∧ ( 𝐶𝑆𝐷𝑆 ) ) → ( 𝐶𝐷𝑀𝑁 ) )