| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Define the strict complete (linear) order predicate. |
| Ref | Expression |
|---|---|
| df-so |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA |
. . 3
| |
| 2 | cR |
. . 3
| |
| 3 | 1, 2 | wor 3751 |
. 2
|
| 4 | 1, 2 | wpo 3750 |
. . 3
|
| 5 | vx |
. . . . . . . 8
| |
| 6 | 5 | cv 1585 |
. . . . . . 7
|
| 7 | vy |
. . . . . . . 8
| |
| 8 | 7 | cv 1585 |
. . . . . . 7
|
| 9 | 6, 8, 2 | wbr 3507 |
. . . . . 6
|
| 10 | 6, 8 | wceq 1586 |
. . . . . 6
|
| 11 | 8, 6, 2 | wbr 3507 |
. . . . . 6
|
| 12 | 9, 10, 11 | w3o 1101 |
. . . . 5
|
| 13 | 12, 7, 1 | wral 2355 |
. . . 4
|
| 14 | 13, 5, 1 | wral 2355 |
. . 3
|
| 15 | 4, 14 | wa 337 |
. 2
|
| 16 | 3, 15 | wb 219 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: sopo 3765 soss 3766 soeq1 3767 solin 3771 itlso 3777 so0 3779 dfwe2 4007 cnvso 4532 soxp 5213 zorn2lem6 6366 zorn 6370 dfso2 14464 soxpOLD 14603 soseq 14608 |