Metamath Proof Explorer

Theorem pocl

Description: Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997)

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 id 
 |-  ( x = B -> x = B )
2 1 1 breq12d 
 |-  ( x = B -> ( x R x <-> B R B ) )
3 2 notbid 
 |-  ( x = B -> ( -. x R x <-> -. B R B ) )
4 breq1 
 |-  ( x = B -> ( x R y <-> B R y ) )
5 4 anbi1d 
 |-  ( x = B -> ( ( x R y /\ y R z ) <-> ( B R y /\ y R z ) ) )
6 breq1 
 |-  ( x = B -> ( x R z <-> B R z ) )
7 5 6 imbi12d 
 |-  ( x = B -> ( ( ( x R y /\ y R z ) -> x R z ) <-> ( ( B R y /\ y R z ) -> B R z ) ) )
8 3 7 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 ) ) ) )
9 8 imbi2d 
 |-  ( x = B -> ( ( R Po A -> ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) <-> ( R Po A -> ( -. B R B /\ ( ( B R y /\ y R z ) -> B R z ) ) ) ) )
10 breq2 
 |-  ( y = C -> ( B R y <-> B R C ) )
11 breq1 
 |-  ( y = C -> ( y R z <-> C R z ) )
12 10 11 anbi12d 
 |-  ( y = C -> ( ( B R y /\ y R z ) <-> ( B R C /\ C R z ) ) )
13 12 imbi1d 
 |-  ( y = C -> ( ( ( B R y /\ y R z ) -> B R z ) <-> ( ( B R C /\ C R z ) -> B R z ) ) )
14 13 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 ) ) ) )
15 14 imbi2d 
 |-  ( y = C -> ( ( R Po A -> ( -. B R B /\ ( ( B R y /\ y R z ) -> B R z ) ) ) <-> ( R Po A -> ( -. 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 20 imbi2d 
 |-  ( z = D -> ( ( R Po A -> ( -. B R B /\ ( ( B R C /\ C R z ) -> B R z ) ) ) <-> ( R Po A -> ( -. B R B /\ ( ( B R C /\ C R D ) -> B R D ) ) ) ) )
22 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 ) ) )
23 r3al 
 |-  ( A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. x A. y A. z ( ( x e. A /\ y e. A /\ z e. A ) -> ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
24 22 23 sylbb 
 |-  ( R Po A -> A. x A. y A. z ( ( x e. A /\ y e. A /\ z e. A ) -> ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
25 24 19.21bbi 
 |-  ( R Po A -> A. z ( ( x e. A /\ y e. A /\ z e. A ) -> ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
26 25 19.21bi 
 |-  ( R Po A -> ( ( x e. A /\ y e. A /\ z e. A ) -> ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
27 26 com12 
 |-  ( ( x e. A /\ y e. A /\ z e. A ) -> ( R Po A -> ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
28 9 15 21 27 vtocl3ga 
 |-  ( ( B e. A /\ C e. A /\ D e. A ) -> ( R Po A -> ( -. B R B /\ ( ( B R C /\ C R D ) -> B R D ) ) ) )
29 28 com12 
 |-  ( R Po A -> ( ( B e. A /\ C e. A /\ D e. A ) -> ( -. B R B /\ ( ( B R C /\ C R D ) -> B R D ) ) ) )