Metamath Proof Explorer


Theorem pocl

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 RPoABACADA¬BRBBRCCRDBRD

Proof

Step Hyp Ref Expression
1 df-po RPoAxAyAzA¬xRxxRyyRzxRz
2 1 biimpi RPoAxAyAzA¬xRxxRyyRzxRz
3 id x=Bx=B
4 3 3 breq12d x=BxRxBRB
5 4 notbid x=B¬xRx¬BRB
6 breq1 x=BxRyBRy
7 6 anbi1d x=BxRyyRzBRyyRz
8 breq1 x=BxRzBRz
9 7 8 imbi12d x=BxRyyRzxRzBRyyRzBRz
10 5 9 anbi12d x=B¬xRxxRyyRzxRz¬BRBBRyyRzBRz
11 breq2 y=CBRyBRC
12 breq1 y=CyRzCRz
13 11 12 anbi12d y=CBRyyRzBRCCRz
14 13 imbi1d y=CBRyyRzBRzBRCCRzBRz
15 14 anbi2d y=C¬BRBBRyyRzBRz¬BRBBRCCRzBRz
16 breq2 z=DCRzCRD
17 16 anbi2d z=DBRCCRzBRCCRD
18 breq2 z=DBRzBRD
19 17 18 imbi12d z=DBRCCRzBRzBRCCRDBRD
20 19 anbi2d z=D¬BRBBRCCRzBRz¬BRBBRCCRDBRD
21 10 15 20 rspc3v BACADAxAyAzA¬xRxxRyyRzxRz¬BRBBRCCRDBRD
22 2 21 syl5com RPoABACADA¬BRBBRCCRDBRD