Metamath Proof Explorer

Theorem ltord1

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

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 2 3 4 5 6 ltordlem ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 < 𝐷 → 𝑀 < 𝑁 ) )
8 eqeq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 = 𝐷 ↔ 𝐶 = 𝐷 ) )
9 2 eqeq1d ⊢ ( 𝑥 = 𝐶 → ( 𝐴 = 𝑁 ↔ 𝑀 = 𝑁 ) )
10 8 9 imbi12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝑥 = 𝐷 → 𝐴 = 𝑁 ) ↔ ( 𝐶 = 𝐷 → 𝑀 = 𝑁 ) ) )
11 10 3 vtoclg ⊢ ( 𝐶 ∈ 𝑆 → ( 𝐶 = 𝐷 → 𝑀 = 𝑁 ) )
12 11 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 = 𝐷 → 𝑀 = 𝑁 ) )
13 1 3 2 4 5 6 ltordlem ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ) → ( 𝐷 < 𝐶 → 𝑁 < 𝑀 ) )
14 13 ancom2s ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐷 < 𝐶 → 𝑁 < 𝑀 ) )
15 12 14 orim12d ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ( 𝐶 = 𝐷 ∨ 𝐷 < 𝐶 ) → ( 𝑀 = 𝑁 ∨ 𝑁 < 𝑀 ) ) )
16 15 con3d ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( ¬ ( 𝑀 = 𝑁 ∨ 𝑁 < 𝑀 ) → ¬ ( 𝐶 = 𝐷 ∨ 𝐷 < 𝐶 ) ) )
17 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ )
18 2 eleq1d ⊢ ( 𝑥 = 𝐶 → ( 𝐴 ∈ ℝ ↔ 𝑀 ∈ ℝ ) )
19 18 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ ∧ 𝐶 ∈ 𝑆 ) → 𝑀 ∈ ℝ )
20 17 19 sylan ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑆 ) → 𝑀 ∈ ℝ )
21 3 eleq1d ⊢ ( 𝑥 = 𝐷 → ( 𝐴 ∈ ℝ ↔ 𝑁 ∈ ℝ ) )
22 21 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ ∧ 𝐷 ∈ 𝑆 ) → 𝑁 ∈ ℝ )
23 17 22 sylan ⊢ ( ( 𝜑 ∧ 𝐷 ∈ 𝑆 ) → 𝑁 ∈ ℝ )
24 20 23 anim12dan ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
25 axlttri ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 < 𝑁 ↔ ¬ ( 𝑀 = 𝑁 ∨ 𝑁 < 𝑀 ) ) )
26 24 25 syl ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝑀 < 𝑁 ↔ ¬ ( 𝑀 = 𝑁 ∨ 𝑁 < 𝑀 ) ) )
27 4 sseli ⊢ ( 𝐶 ∈ 𝑆 → 𝐶 ∈ ℝ )
28 4 sseli ⊢ ( 𝐷 ∈ 𝑆 → 𝐷 ∈ ℝ )
29 axlttri ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐶 < 𝐷 ↔ ¬ ( 𝐶 = 𝐷 ∨ 𝐷 < 𝐶 ) ) )
30 27 28 29 syl2an ⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) → ( 𝐶 < 𝐷 ↔ ¬ ( 𝐶 = 𝐷 ∨ 𝐷 < 𝐶 ) ) )
31 30 adantl ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 < 𝐷 ↔ ¬ ( 𝐶 = 𝐷 ∨ 𝐷 < 𝐶 ) ) )
32 16 26 31 3imtr4d ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝑀 < 𝑁 → 𝐶 < 𝐷 ) )
33 7 32 impbid ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆 ) ) → ( 𝐶 < 𝐷 ↔ 𝑀 < 𝑁 ) )