Description: Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | swopolem.1 | |
|
Assertion | swopolem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | swopolem.1 | |
|
2 | 1 | ralrimivvva | |
3 | breq1 | |
|
4 | breq1 | |
|
5 | 4 | orbi1d | |
6 | 3 5 | imbi12d | |
7 | breq2 | |
|
8 | breq2 | |
|
9 | 8 | orbi2d | |
10 | 7 9 | imbi12d | |
11 | breq2 | |
|
12 | breq1 | |
|
13 | 11 12 | orbi12d | |
14 | 13 | imbi2d | |
15 | 6 10 14 | rspc3v | |
16 | 2 15 | mpan9 | |