Theorem ltordlem

Description: Lemma for ltord1 . (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	$$⊢\left(\phi \wedge x\in S\right)\to A\in ℝ$$
	ltord.6	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to \left(x<y\to A<B\right)$$
Assertion	ltordlem	$$⊢\left(\phi \wedge \left(C\in S\wedge D\in S\right)\right)\to \left(C<D\to M<N\right)$$

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