Metamath Proof Explorer


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 ) )