Description: Characteristic properties of a partial order in class notation. (Contributed by NM, 27-Mar-1997) Reduce axiom usage and shorten proof. (Revised by Gino Giotto, 3-Oct-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | pocl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-po | |
|
2 | 1 | biimpi | |
3 | id | |
|
4 | 3 3 | breq12d | |
5 | 4 | notbid | |
6 | breq1 | |
|
7 | 6 | anbi1d | |
8 | breq1 | |
|
9 | 7 8 | imbi12d | |
10 | 5 9 | anbi12d | |
11 | breq2 | |
|
12 | breq1 | |
|
13 | 11 12 | anbi12d | |
14 | 13 | imbi1d | |
15 | 14 | anbi2d | |
16 | breq2 | |
|
17 | 16 | anbi2d | |
18 | breq2 | |
|
19 | 17 18 | imbi12d | |
20 | 19 | anbi2d | |
21 | 10 15 20 | rspc3v | |
22 | 2 21 | syl5com | |