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 
|- ( R Po A -> ( ( B e. A /\ C e. A /\ D e. A ) -> ( -. B R B /\ ( ( B R C /\ C R D ) -> B R D ) ) ) )

Proof

Step Hyp Ref Expression
1 df-po 
 |-  ( R Po A <-> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )
2 1 biimpi 
 |-  ( R Po A -> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )
3 id 
 |-  ( x = B -> x = B )
4 3 3 breq12d 
 |-  ( x = B -> ( x R x <-> B R B ) )
5 4 notbid 
 |-  ( x = B -> ( -. x R x <-> -. B R B ) )
6 breq1 
 |-  ( x = B -> ( x R y <-> B R y ) )
7 6 anbi1d 
 |-  ( x = B -> ( ( x R y /\ y R z ) <-> ( B R y /\ y R z ) ) )
8 breq1 
 |-  ( x = B -> ( x R z <-> B R z ) )
9 7 8 imbi12d 
 |-  ( x = B -> ( ( ( x R y /\ y R z ) -> x R z ) <-> ( ( B R y /\ y R z ) -> B R z ) ) )
10 5 9 anbi12d 
 |-  ( x = B -> ( ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> ( -. B R B /\ ( ( B R y /\ y R z ) -> B R z ) ) ) )
11 breq2 
 |-  ( y = C -> ( B R y <-> B R C ) )
12 breq1 
 |-  ( y = C -> ( y R z <-> C R z ) )
13 11 12 anbi12d 
 |-  ( y = C -> ( ( B R y /\ y R z ) <-> ( B R C /\ C R z ) ) )
14 13 imbi1d 
 |-  ( y = C -> ( ( ( B R y /\ y R z ) -> B R z ) <-> ( ( B R C /\ C R z ) -> B R z ) ) )
15 14 anbi2d 
 |-  ( y = C -> ( ( -. B R B /\ ( ( B R y /\ y R z ) -> B R z ) ) <-> ( -. B R B /\ ( ( B R C /\ C R z ) -> B R z ) ) ) )
16 breq2 
 |-  ( z = D -> ( C R z <-> C R D ) )
17 16 anbi2d 
 |-  ( z = D -> ( ( B R C /\ C R z ) <-> ( B R C /\ C R D ) ) )
18 breq2 
 |-  ( z = D -> ( B R z <-> B R D ) )
19 17 18 imbi12d 
 |-  ( z = D -> ( ( ( B R C /\ C R z ) -> B R z ) <-> ( ( B R C /\ C R D ) -> B R D ) ) )
20 19 anbi2d 
 |-  ( z = D -> ( ( -. B R B /\ ( ( B R C /\ C R z ) -> B R z ) ) <-> ( -. B R B /\ ( ( B R C /\ C R D ) -> B R D ) ) ) )
21 10 15 20 rspc3v 
 |-  ( ( B e. A /\ C e. A /\ D e. A ) -> ( A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) -> ( -. B R B /\ ( ( B R C /\ C R D ) -> B R D ) ) ) )
22 2 21 syl5com 
 |-  ( R Po A -> ( ( B e. A /\ C e. A /\ D e. A ) -> ( -. B R B /\ ( ( B R C /\ C R D ) -> B R D ) ) ) )