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	$⊢ x = y \to A = B$
	ltord.2	$⊢ x = C \to A = M$
	ltord.3	$⊢ x = D \to A = N$
	ltord.4	$⊢ S \subseteq ℝ$
	ltord.5	$⊢ (φ \land x \in S) \to A \in ℝ$
	ltord.6	$⊢ (φ \land (x \in S \land y \in S)) \to (x < y \to A < B)$
Assertion	ltord1	$⊢ (φ \land (C \in S \land D \in S)) \to (C < D \leftrightarrow M < N)$

Proof

Step	Hyp	Ref	Expression
1		ltord.1	$⊢ x = y \to A = B$
2		ltord.2	$⊢ x = C \to A = M$
3		ltord.3	$⊢ x = D \to A = N$
4		ltord.4	$⊢ S \subseteq ℝ$
5		ltord.5	$⊢ (φ \land x \in S) \to A \in ℝ$
6		ltord.6	$⊢ (φ \land (x \in S \land y \in S)) \to (x < y \to A < B)$
7	1 2 3 4 5 6	ltordlem	$⊢ (φ \land (C \in S \land D \in S)) \to (C < D \to M < N)$
8		eqeq1	$⊢ x = C \to (x = D \leftrightarrow C = D)$
9	2	eqeq1d	$⊢ x = C \to (A = N \leftrightarrow M = N)$
10	8 9	imbi12d	$⊢ x = C \to ((x = D \to A = N) \leftrightarrow (C = D \to M = N))$
11	10 3	vtoclg	$⊢ C \in S \to (C = D \to M = N)$
12	11	ad2antrl	$⊢ (φ \land (C \in S \land D \in S)) \to (C = D \to M = N)$
13	1 3 2 4 5 6	ltordlem	$⊢ (φ \land (D \in S \land C \in S)) \to (D < C \to N < M)$
14	13	ancom2s	$⊢ (φ \land (C \in S \land D \in S)) \to (D < C \to N < M)$
15	12 14	orim12d	$⊢ (φ \land (C \in S \land D \in S)) \to ((C = D \lor D < C) \to (M = N \lor N < M))$
16	15	con3d	$⊢ (φ \land (C \in S \land D \in S)) \to (\neg (M = N \lor N < M) \to \neg (C = D \lor D < C))$
17	5	ralrimiva	$⊢ φ \to \forall x \in S A \in ℝ$
18	2	eleq1d	$⊢ x = C \to (A \in ℝ \leftrightarrow M \in ℝ)$
19	18	rspccva	$⊢ (\forall x \in S A \in ℝ \land C \in S) \to M \in ℝ$
20	17 19	sylan	$⊢ (φ \land C \in S) \to M \in ℝ$
21	3	eleq1d	$⊢ x = D \to (A \in ℝ \leftrightarrow N \in ℝ)$
22	21	rspccva	$⊢ (\forall x \in S A \in ℝ \land D \in S) \to N \in ℝ$
23	17 22	sylan	$⊢ (φ \land D \in S) \to N \in ℝ$
24	20 23	anim12dan	$⊢ (φ \land (C \in S \land D \in S)) \to (M \in ℝ \land N \in ℝ)$
25		axlttri	$⊢ (M \in ℝ \land N \in ℝ) \to (M < N \leftrightarrow \neg (M = N \lor N < M))$
26	24 25	syl	$⊢ (φ \land (C \in S \land D \in S)) \to (M < N \leftrightarrow \neg (M = N \lor N < M))$
27	4	sseli	$⊢ C \in S \to C \in ℝ$
28	4	sseli	$⊢ D \in S \to D \in ℝ$
29		axlttri	$⊢ (C \in ℝ \land D \in ℝ) \to (C < D \leftrightarrow \neg (C = D \lor D < C))$
30	27 28 29	syl2an	$⊢ (C \in S \land D \in S) \to (C < D \leftrightarrow \neg (C = D \lor D < C))$
31	30	adantl	$⊢ (φ \land (C \in S \land D \in S)) \to (C < D \leftrightarrow \neg (C = D \lor D < C))$
32	16 26 31	3imtr4d	$⊢ (φ \land (C \in S \land D \in S)) \to (M < N \to C < D)$
33	7 32	impbid	$⊢ (φ \land (C \in S \land D \in S)) \to (C < D \leftrightarrow M < N)$

Metamath Proof Explorer

Theorem ltord1

Proof