![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-po | Structured version Visualization version Unicode version |
Description: Define the strict partial
order predicate. Definition of [Enderton]
p. 168. The expression ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-po |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cR |
. . 3
![]() ![]() | |
3 | 1, 2 | wpo 5033 |
. 2
![]() ![]() ![]() ![]() |
4 | vx |
. . . . . . . . 9
![]() ![]() | |
5 | 4 | cv 1482 |
. . . . . . . 8
![]() ![]() |
6 | 5, 5, 2 | wbr 4653 |
. . . . . . 7
![]() ![]() ![]() ![]() |
7 | 6 | wn 3 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() |
8 | vy |
. . . . . . . . . 10
![]() ![]() | |
9 | 8 | cv 1482 |
. . . . . . . . 9
![]() ![]() |
10 | 5, 9, 2 | wbr 4653 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
11 | vz |
. . . . . . . . . 10
![]() ![]() | |
12 | 11 | cv 1482 |
. . . . . . . . 9
![]() ![]() |
13 | 9, 12, 2 | wbr 4653 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
14 | 10, 13 | wa 384 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 5, 12, 2 | wbr 4653 |
. . . . . . 7
![]() ![]() ![]() ![]() |
16 | 14, 15 | wi 4 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 7, 16 | wa 384 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 17, 11, 1 | wral 2912 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 18, 8, 1 | wral 2912 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | 19, 4, 1 | wral 2912 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
21 | 3, 20 | wb 196 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: poss 5037 poeq1 5038 nfpo 5040 pocl 5042 ispod 5043 po0 5050 poinxp 5182 posn 5187 cnvpo 5673 isopolem 6595 porpss 6941 dfwe2 6981 poxp 7289 dfso3 31601 dfpo2 31645 elpotr 31686 poseq 31750 |
Copyright terms: Public domain | W3C validator |