Theorem ltordlem

Description: Lemma for ltord1 . (Contributed by Mario Carneiro, 14-Jun-2014)

	Ref	Expression
Hypotheses	ltord.1	|- ( x = y -> A = B )
	ltord.2	|- ( x = C -> A = M )
	ltord.3	|- ( x = D -> A = N )
	ltord.4	|- S C_ RR
	ltord.5	|- ( ( ph /\ x e. S ) -> A e. RR )
	ltord.6	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x < y -> A < B ) )
Assertion	ltordlem	|- ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C < D -> M < N ) )

Proof

Step	Hyp	Ref	Expression
1		ltord.1	|- ( x = y -> A = B )
2		ltord.2	|- ( x = C -> A = M )
3		ltord.3	|- ( x = D -> A = N )
4		ltord.4	|- S C_ RR
5		ltord.5	|- ( ( ph /\ x e. S ) -> A e. RR )
6		ltord.6	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x < y -> A < B ) )
7	6	ralrimivva	|- ( ph -> A. x e. S A. y e. S ( x < y -> A < B ) )
8		breq1	|- ( x = C -> ( x < y <-> C < y ) )
9	2	breq1d	|- ( x = C -> ( A < B <-> M < B ) )
10	8 9	imbi12d	|- ( x = C -> ( ( x < y -> A < B ) <-> ( C < y -> M < B ) ) )
11		breq2	|- ( y = D -> ( C < y <-> C < D ) )
12		eqeq1	|- ( x = y -> ( x = D <-> y = D ) )
13	1	eqeq1d	|- ( x = y -> ( A = N <-> B = N ) )
14	12 13	imbi12d	|- ( x = y -> ( ( x = D -> A = N ) <-> ( y = D -> B = N ) ) )
15	14 3	chvarvv	|- ( y = D -> B = N )
16	15	breq2d	|- ( y = D -> ( M < B <-> M < N ) )
17	11 16	imbi12d	|- ( y = D -> ( ( C < y -> M < B ) <-> ( C < D -> M < N ) ) )
18	10 17	rspc2v	|- ( ( C e. S /\ D e. S ) -> ( A. x e. S A. y e. S ( x < y -> A < B ) -> ( C < D -> M < N ) ) )
19	7 18	mpan9	|- ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C < D -> M < N ) )