Metamath Proof Explorer

Theorem cnvpo

Description: The converse of a partial order is a partial order. (Contributed by NM, 15-Jun-2005)

Ref Expression
Assertion cnvpo 
|- ( R Po A <-> `' R Po A )

Proof

Step Hyp Ref Expression
1 r19.26 
 |-  ( A. z e. A ( -. z `' R z /\ ( ( z `' R y /\ y `' R x ) -> z `' R x ) ) <-> ( A. z e. A -. z `' R z /\ A. z e. A ( ( z `' R y /\ y `' R x ) -> z `' R x ) ) )
2 vex 
 |-  z e. _V
3 2 2 brcnv 
 |-  ( z `' R z <-> z R z )
4 id 
 |-  ( z = x -> z = x )
5 4 4 breq12d 
 |-  ( z = x -> ( z R z <-> x R x ) )
6 3 5 bitrid 
 |-  ( z = x -> ( z `' R z <-> x R x ) )
7 6 notbid 
 |-  ( z = x -> ( -. z `' R z <-> -. x R x ) )
8 7 cbvralvw 
 |-  ( A. z e. A -. z `' R z <-> A. x e. A -. x R x )
9 vex 
 |-  y e. _V
10 2 9 brcnv 
 |-  ( z `' R y <-> y R z )
11 vex 
 |-  x e. _V
12 9 11 brcnv 
 |-  ( y `' R x <-> x R y )
13 10 12 anbi12ci 
 |-  ( ( z `' R y /\ y `' R x ) <-> ( x R y /\ y R z ) )
14 2 11 brcnv 
 |-  ( z `' R x <-> x R z )
15 13 14 imbi12i 
 |-  ( ( ( z `' R y /\ y `' R x ) -> z `' R x ) <-> ( ( x R y /\ y R z ) -> x R z ) )
16 15 ralbii 
 |-  ( A. z e. A ( ( z `' R y /\ y `' R x ) -> z `' R x ) <-> A. z e. A ( ( x R y /\ y R z ) -> x R z ) )
17 8 16 anbi12i 
 |-  ( ( A. z e. A -. z `' R z /\ A. z e. A ( ( z `' R y /\ y `' R x ) -> z `' R x ) ) <-> ( A. x e. A -. x R x /\ A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) )
18 1 17 bitr2i 
 |-  ( ( A. x e. A -. x R x /\ A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) <-> A. z e. A ( -. z `' R z /\ ( ( z `' R y /\ y `' R x ) -> z `' R x ) ) )
19 18 ralbii 
 |-  ( A. x e. A ( A. x e. A -. x R x /\ A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) <-> A. x e. A A. z e. A ( -. z `' R z /\ ( ( z `' R y /\ y `' R x ) -> z `' R x ) ) )
20 r19.26 
 |-  ( A. x e. A ( A. z e. A -. x R x /\ A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) <-> ( A. x e. A A. z e. A -. x R x /\ A. x e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) )
21 ralidm 
 |-  ( A. x e. A A. x e. A -. x R x <-> A. x e. A -. x R x )
22 rzal 
 |-  ( A = (/) -> A. x e. A -. x R x )
23 rzal 
 |-  ( A = (/) -> A. x e. A A. z e. A -. x R x )
24 22 23 2thd 
 |-  ( A = (/) -> ( A. x e. A -. x R x <-> A. x e. A A. z e. A -. x R x ) )
25 r19.3rzv 
 |-  ( A =/= (/) -> ( -. x R x <-> A. z e. A -. x R x ) )
26 25 ralbidv 
 |-  ( A =/= (/) -> ( A. x e. A -. x R x <-> A. x e. A A. z e. A -. x R x ) )
27 24 26 pm2.61ine 
 |-  ( A. x e. A -. x R x <-> A. x e. A A. z e. A -. x R x )
28 21 27 bitr2i 
 |-  ( A. x e. A A. z e. A -. x R x <-> A. x e. A A. x e. A -. x R x )
29 28 anbi1i 
 |-  ( ( A. x e. A A. z e. A -. x R x /\ A. x e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) <-> ( A. x e. A A. x e. A -. x R x /\ A. x e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) )
30 20 29 bitri 
 |-  ( A. x e. A ( A. z e. A -. x R x /\ A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) <-> ( A. x e. A A. x e. A -. x R x /\ A. x e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) )
31 r19.26 
 |-  ( A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> ( A. z e. A -. x R x /\ A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) )
32 31 ralbii 
 |-  ( A. x e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. x e. A ( A. z e. A -. x R x /\ A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) )
33 r19.26 
 |-  ( A. x e. A ( A. x e. A -. x R x /\ A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) <-> ( A. x e. A A. x e. A -. x R x /\ A. x e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) )
34 30 32 33 3bitr4i 
 |-  ( A. x e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. x e. A ( A. x e. A -. x R x /\ A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) )
35 ralcom 
 |-  ( A. z e. A A. x e. A ( -. z `' R z /\ ( ( z `' R y /\ y `' R x ) -> z `' R x ) ) <-> A. x e. A A. z e. A ( -. z `' R z /\ ( ( z `' R y /\ y `' R x ) -> z `' R x ) ) )
36 19 34 35 3bitr4i 
 |-  ( A. x e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. z e. A A. x e. A ( -. z `' R z /\ ( ( z `' R y /\ y `' R x ) -> z `' R x ) ) )
37 36 ralbii 
 |-  ( A. y e. A A. x e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. y e. A A. z e. A A. x e. A ( -. z `' R z /\ ( ( z `' R y /\ y `' R x ) -> z `' R x ) ) )
38 ralcom 
 |-  ( 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. y e. A A. x e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )
39 ralcom 
 |-  ( A. z e. A A. y e. A A. x e. A ( -. z `' R z /\ ( ( z `' R y /\ y `' R x ) -> z `' R x ) ) <-> A. y e. A A. z e. A A. x e. A ( -. z `' R z /\ ( ( z `' R y /\ y `' R x ) -> z `' R x ) ) )
40 37 38 39 3bitr4i 
 |-  ( 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. z e. A A. y e. A A. x e. A ( -. z `' R z /\ ( ( z `' R y /\ y `' R x ) -> z `' R x ) ) )
41 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 ) ) )
42 df-po 
 |-  ( `' R Po A <-> A. z e. A A. y e. A A. x e. A ( -. z `' R z /\ ( ( z `' R y /\ y `' R x ) -> z `' R x ) ) )
43 40 41 42 3bitr4i 
 |-  ( R Po A <-> `' R Po A )