ltordlem

	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	ltordlem	$⊢ (φ \land (C \in S \land D \in S)) \to (C < D \to M < N)$

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	6	ralrimivva	$⊢ φ \to \forall x \in S \forall y \in S (x < y \to A < B)$
8		breq1	$⊢ x = C \to (x < y \leftrightarrow C < y)$
9	2	breq1d	$⊢ x = C \to (A < B \leftrightarrow M < B)$
10	8 9	imbi12d	$⊢ x = C \to ((x < y \to A < B) \leftrightarrow (C < y \to M < B))$
11		breq2	$⊢ y = D \to (C < y \leftrightarrow C < D)$
12		eqeq1	$⊢ x = y \to (x = D \leftrightarrow y = D)$
13	1	eqeq1d	$⊢ x = y \to (A = N \leftrightarrow B = N)$
14	12 13	imbi12d	$⊢ x = y \to ((x = D \to A = N) \leftrightarrow (y = D \to B = N))$
15	14 3	chvarvv	$⊢ y = D \to B = N$
16	15	breq2d	$⊢ y = D \to (M < B \leftrightarrow M < N)$
17	11 16	imbi12d	$⊢ y = D \to ((C < y \to M < B) \leftrightarrow (C < D \to M < N))$
18	10 17	rspc2v	$⊢ (C \in S \land D \in S) \to (\forall x \in S \forall y \in S (x < y \to A < B) \to (C < D \to M < N))$
19	7 18	mpan9	$⊢ (φ \land (C \in S \land D \in S)) \to (C < D \to M < N)$

Metamath Proof Explorer