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