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