Metamath Proof Explorer

Theorem dfpo2

Description: Quantifier-free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion dfpo2 
|- ( R Po A <-> ( ( R i^i ( _I |` A ) ) = (/) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R ) )

Proof

Step Hyp Ref Expression
1 po0 
 |-  R Po (/)
2 res0 
 |-  ( _I |` (/) ) = (/)
3 2 ineq2i 
 |-  ( R i^i ( _I |` (/) ) ) = ( R i^i (/) )
4 in0 
 |-  ( R i^i (/) ) = (/)
5 3 4 eqtri 
 |-  ( R i^i ( _I |` (/) ) ) = (/)
6 xp0 
 |-  ( A X. (/) ) = (/)
7 6 ineq2i 
 |-  ( R i^i ( A X. (/) ) ) = ( R i^i (/) )
8 7 4 eqtri 
 |-  ( R i^i ( A X. (/) ) ) = (/)
9 8 coeq2i 
 |-  ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. (/) ) ) ) = ( ( R i^i ( A X. A ) ) o. (/) )
10 co02 
 |-  ( ( R i^i ( A X. A ) ) o. (/) ) = (/)
11 9 10 eqtri 
 |-  ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. (/) ) ) ) = (/)
12 0ss 
 |-  (/) C_ R
13 11 12 eqsstri 
 |-  ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. (/) ) ) ) C_ R
14 5 13 pm3.2i 
 |-  ( ( R i^i ( _I |` (/) ) ) = (/) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. (/) ) ) ) C_ R )
15 1 14 2th 
 |-  ( R Po (/) <-> ( ( R i^i ( _I |` (/) ) ) = (/) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. (/) ) ) ) C_ R ) )
16 poeq2 
 |-  ( A = (/) -> ( R Po A <-> R Po (/) ) )
17 reseq2 
 |-  ( A = (/) -> ( _I |` A ) = ( _I |` (/) ) )
18 17 ineq2d 
 |-  ( A = (/) -> ( R i^i ( _I |` A ) ) = ( R i^i ( _I |` (/) ) ) )
19 18 eqeq1d 
 |-  ( A = (/) -> ( ( R i^i ( _I |` A ) ) = (/) <-> ( R i^i ( _I |` (/) ) ) = (/) ) )
20 xpeq2 
 |-  ( A = (/) -> ( A X. A ) = ( A X. (/) ) )
21 20 ineq2d 
 |-  ( A = (/) -> ( R i^i ( A X. A ) ) = ( R i^i ( A X. (/) ) ) )
22 21 coeq2d 
 |-  ( A = (/) -> ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) = ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. (/) ) ) ) )
23 22 sseq1d 
 |-  ( A = (/) -> ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R <-> ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. (/) ) ) ) C_ R ) )
24 19 23 anbi12d 
 |-  ( A = (/) -> ( ( ( R i^i ( _I |` A ) ) = (/) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R ) <-> ( ( R i^i ( _I |` (/) ) ) = (/) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. (/) ) ) ) C_ R ) ) )
25 16 24 bibi12d 
 |-  ( A = (/) -> ( ( R Po A <-> ( ( R i^i ( _I |` A ) ) = (/) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R ) ) <-> ( R Po (/) <-> ( ( R i^i ( _I |` (/) ) ) = (/) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. (/) ) ) ) C_ R ) ) ) )
26 15 25 mpbiri 
 |-  ( A = (/) -> ( R Po A <-> ( ( R i^i ( _I |` A ) ) = (/) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R ) ) )
27 r19.28zv 
 |-  ( A =/= (/) -> ( A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> ( -. x R x /\ A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) ) )
28 27 ralbidv 
 |-  ( 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 ( -. x R x /\ A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) ) )
29 r19.28zv 
 |-  ( A =/= (/) -> ( A. y e. A ( -. x R x /\ A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) <-> ( -. x R x /\ A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) ) )
30 28 29 bitrd 
 |-  ( A =/= (/) -> ( A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> ( -. x R x /\ A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) ) )
31 30 ralbidv 
 |-  ( 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 ) ) <-> A. x e. A ( -. x R x /\ A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) ) )
32 r19.26 
 |-  ( A. x e. A ( -. x R x /\ A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) <-> ( A. x e. A -. x R x /\ A. x e. A A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) )
33 31 32 bitrdi 
 |-  ( 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 ) ) <-> ( A. x e. A -. x R x /\ A. x e. A A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) ) )
34 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 ) ) )
35 disj 
 |-  ( ( R i^i ( _I |` A ) ) = (/) <-> A. w e. R -. w e. ( _I |` A ) )
36 df-ral 
 |-  ( A. w e. R -. w e. ( _I |` A ) <-> A. w ( w e. R -> -. w e. ( _I |` A ) ) )
37 opex 
 |-  <. x , x >. e. _V
38 eleq1 
 |-  ( w = <. x , x >. -> ( w e. R <-> <. x , x >. e. R ) )
39 df-br 
 |-  ( x R x <-> <. x , x >. e. R )
40 38 39 bitr4di 
 |-  ( w = <. x , x >. -> ( w e. R <-> x R x ) )
41 eleq1 
 |-  ( w = <. x , x >. -> ( w e. ( _I |` A ) <-> <. x , x >. e. ( _I |` A ) ) )
42 opelidres 
 |-  ( x e. _V -> ( <. x , x >. e. ( _I |` A ) <-> x e. A ) )
43 42 elv 
 |-  ( <. x , x >. e. ( _I |` A ) <-> x e. A )
44 41 43 bitrdi 
 |-  ( w = <. x , x >. -> ( w e. ( _I |` A ) <-> x e. A ) )
45 44 notbid 
 |-  ( w = <. x , x >. -> ( -. w e. ( _I |` A ) <-> -. x e. A ) )
46 40 45 imbi12d 
 |-  ( w = <. x , x >. -> ( ( w e. R -> -. w e. ( _I |` A ) ) <-> ( x R x -> -. x e. A ) ) )
47 37 46 spcv 
 |-  ( A. w ( w e. R -> -. w e. ( _I |` A ) ) -> ( x R x -> -. x e. A ) )
48 47 con2d 
 |-  ( A. w ( w e. R -> -. w e. ( _I |` A ) ) -> ( x e. A -> -. x R x ) )
49 48 alrimiv 
 |-  ( A. w ( w e. R -> -. w e. ( _I |` A ) ) -> A. x ( x e. A -> -. x R x ) )
50 relres 
 |-  Rel ( _I |` A )
51 elrel 
 |-  ( ( Rel ( _I |` A ) /\ w e. ( _I |` A ) ) -> E. y E. z w = <. y , z >. )
52 50 51 mpan 
 |-  ( w e. ( _I |` A ) -> E. y E. z w = <. y , z >. )
53 52 ancri 
 |-  ( w e. ( _I |` A ) -> ( E. y E. z w = <. y , z >. /\ w e. ( _I |` A ) ) )
54 eleq1 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
55 breq12 
 |-  ( ( x = y /\ x = y ) -> ( x R x <-> y R y ) )
56 55 anidms 
 |-  ( x = y -> ( x R x <-> y R y ) )
57 56 notbid 
 |-  ( x = y -> ( -. x R x <-> -. y R y ) )
58 54 57 imbi12d 
 |-  ( x = y -> ( ( x e. A -> -. x R x ) <-> ( y e. A -> -. y R y ) ) )
59 58 spvv 
 |-  ( A. x ( x e. A -> -. x R x ) -> ( y e. A -> -. y R y ) )
60 breq2 
 |-  ( y = z -> ( y R y <-> y R z ) )
61 60 notbid 
 |-  ( y = z -> ( -. y R y <-> -. y R z ) )
62 61 imbi2d 
 |-  ( y = z -> ( ( y e. A -> -. y R y ) <-> ( y e. A -> -. y R z ) ) )
63 62 biimpcd 
 |-  ( ( y e. A -> -. y R y ) -> ( y = z -> ( y e. A -> -. y R z ) ) )
64 63 impcomd 
 |-  ( ( y e. A -> -. y R y ) -> ( ( y e. A /\ y = z ) -> -. y R z ) )
65 59 64 syl 
 |-  ( A. x ( x e. A -> -. x R x ) -> ( ( y e. A /\ y = z ) -> -. y R z ) )
66 eleq1 
 |-  ( w = <. y , z >. -> ( w e. ( _I |` A ) <-> <. y , z >. e. ( _I |` A ) ) )
67 vex 
 |-  z e. _V
68 67 brresi 
 |-  ( y ( _I |` A ) z <-> ( y e. A /\ y _I z ) )
69 df-br 
 |-  ( y ( _I |` A ) z <-> <. y , z >. e. ( _I |` A ) )
70 67 ideq 
 |-  ( y _I z <-> y = z )
71 70 anbi2i 
 |-  ( ( y e. A /\ y _I z ) <-> ( y e. A /\ y = z ) )
72 68 69 71 3bitr3ri 
 |-  ( ( y e. A /\ y = z ) <-> <. y , z >. e. ( _I |` A ) )
73 66 72 bitr4di 
 |-  ( w = <. y , z >. -> ( w e. ( _I |` A ) <-> ( y e. A /\ y = z ) ) )
74 eleq1 
 |-  ( w = <. y , z >. -> ( w e. R <-> <. y , z >. e. R ) )
75 df-br 
 |-  ( y R z <-> <. y , z >. e. R )
76 74 75 bitr4di 
 |-  ( w = <. y , z >. -> ( w e. R <-> y R z ) )
77 76 notbid 
 |-  ( w = <. y , z >. -> ( -. w e. R <-> -. y R z ) )
78 73 77 imbi12d 
 |-  ( w = <. y , z >. -> ( ( w e. ( _I |` A ) -> -. w e. R ) <-> ( ( y e. A /\ y = z ) -> -. y R z ) ) )
79 65 78 syl5ibrcom 
 |-  ( A. x ( x e. A -> -. x R x ) -> ( w = <. y , z >. -> ( w e. ( _I |` A ) -> -. w e. R ) ) )
80 79 exlimdvv 
 |-  ( A. x ( x e. A -> -. x R x ) -> ( E. y E. z w = <. y , z >. -> ( w e. ( _I |` A ) -> -. w e. R ) ) )
81 80 impd 
 |-  ( A. x ( x e. A -> -. x R x ) -> ( ( E. y E. z w = <. y , z >. /\ w e. ( _I |` A ) ) -> -. w e. R ) )
82 53 81 syl5 
 |-  ( A. x ( x e. A -> -. x R x ) -> ( w e. ( _I |` A ) -> -. w e. R ) )
83 82 con2d 
 |-  ( A. x ( x e. A -> -. x R x ) -> ( w e. R -> -. w e. ( _I |` A ) ) )
84 83 alrimiv 
 |-  ( A. x ( x e. A -> -. x R x ) -> A. w ( w e. R -> -. w e. ( _I |` A ) ) )
85 49 84 impbii 
 |-  ( A. w ( w e. R -> -. w e. ( _I |` A ) ) <-> A. x ( x e. A -> -. x R x ) )
86 df-ral 
 |-  ( A. x e. A -. x R x <-> A. x ( x e. A -> -. x R x ) )
87 85 86 bitr4i 
 |-  ( A. w ( w e. R -> -. w e. ( _I |` A ) ) <-> A. x e. A -. x R x )
88 35 36 87 3bitri 
 |-  ( ( R i^i ( _I |` A ) ) = (/) <-> A. x e. A -. x R x )
89 ralcom 
 |-  ( A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) <-> A. z e. A A. y e. A ( ( x R y /\ y R z ) -> x R z ) )
90 r19.23v 
 |-  ( A. y e. A ( ( x R y /\ y R z ) -> x R z ) <-> ( E. y e. A ( x R y /\ y R z ) -> x R z ) )
91 90 ralbii 
 |-  ( A. z e. A A. y e. A ( ( x R y /\ y R z ) -> x R z ) <-> A. z e. A ( E. y e. A ( x R y /\ y R z ) -> x R z ) )
92 89 91 bitri 
 |-  ( A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) <-> A. z e. A ( E. y e. A ( x R y /\ y R z ) -> x R z ) )
93 92 ralbii 
 |-  ( A. x e. A A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) <-> A. x e. A A. z e. A ( E. y e. A ( x R y /\ y R z ) -> x R z ) )
94 brin 
 |-  ( x ( R i^i ( A X. A ) ) y <-> ( x R y /\ x ( A X. A ) y ) )
95 brin 
 |-  ( y ( R i^i ( A X. A ) ) z <-> ( y R z /\ y ( A X. A ) z ) )
96 94 95 anbi12i 
 |-  ( ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) z ) <-> ( ( x R y /\ x ( A X. A ) y ) /\ ( y R z /\ y ( A X. A ) z ) ) )
97 an4 
 |-  ( ( ( x R y /\ x ( A X. A ) y ) /\ ( y R z /\ y ( A X. A ) z ) ) <-> ( ( x R y /\ y R z ) /\ ( x ( A X. A ) y /\ y ( A X. A ) z ) ) )
98 ancom 
 |-  ( ( ( x R y /\ y R z ) /\ ( x ( A X. A ) y /\ y ( A X. A ) z ) ) <-> ( ( x ( A X. A ) y /\ y ( A X. A ) z ) /\ ( x R y /\ y R z ) ) )
99 ancom 
 |-  ( ( x e. A /\ y e. A ) <-> ( y e. A /\ x e. A ) )
100 99 anbi1i 
 |-  ( ( ( x e. A /\ y e. A ) /\ ( y e. A /\ z e. A ) ) <-> ( ( y e. A /\ x e. A ) /\ ( y e. A /\ z e. A ) ) )
101 brxp 
 |-  ( x ( A X. A ) y <-> ( x e. A /\ y e. A ) )
102 brxp 
 |-  ( y ( A X. A ) z <-> ( y e. A /\ z e. A ) )
103 101 102 anbi12i 
 |-  ( ( x ( A X. A ) y /\ y ( A X. A ) z ) <-> ( ( x e. A /\ y e. A ) /\ ( y e. A /\ z e. A ) ) )
104 anandi 
 |-  ( ( y e. A /\ ( x e. A /\ z e. A ) ) <-> ( ( y e. A /\ x e. A ) /\ ( y e. A /\ z e. A ) ) )
105 100 103 104 3bitr4i 
 |-  ( ( x ( A X. A ) y /\ y ( A X. A ) z ) <-> ( y e. A /\ ( x e. A /\ z e. A ) ) )
106 105 anbi1i 
 |-  ( ( ( x ( A X. A ) y /\ y ( A X. A ) z ) /\ ( x R y /\ y R z ) ) <-> ( ( y e. A /\ ( x e. A /\ z e. A ) ) /\ ( x R y /\ y R z ) ) )
107 97 98 106 3bitri 
 |-  ( ( ( x R y /\ x ( A X. A ) y ) /\ ( y R z /\ y ( A X. A ) z ) ) <-> ( ( y e. A /\ ( x e. A /\ z e. A ) ) /\ ( x R y /\ y R z ) ) )
108 anass 
 |-  ( ( ( y e. A /\ ( x e. A /\ z e. A ) ) /\ ( x R y /\ y R z ) ) <-> ( y e. A /\ ( ( x e. A /\ z e. A ) /\ ( x R y /\ y R z ) ) ) )
109 96 107 108 3bitri 
 |-  ( ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) z ) <-> ( y e. A /\ ( ( x e. A /\ z e. A ) /\ ( x R y /\ y R z ) ) ) )
110 109 exbii 
 |-  ( E. y ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) z ) <-> E. y ( y e. A /\ ( ( x e. A /\ z e. A ) /\ ( x R y /\ y R z ) ) ) )
111 vex 
 |-  x e. _V
112 111 67 brco 
 |-  ( x ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) z <-> E. y ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) z ) )
113 df-br 
 |-  ( x ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) z <-> <. x , z >. e. ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) )
114 112 113 bitr3i 
 |-  ( E. y ( x ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) z ) <-> <. x , z >. e. ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) )
115 df-rex 
 |-  ( E. y e. A ( ( x e. A /\ z e. A ) /\ ( x R y /\ y R z ) ) <-> E. y ( y e. A /\ ( ( x e. A /\ z e. A ) /\ ( x R y /\ y R z ) ) ) )
116 r19.42v 
 |-  ( E. y e. A ( ( x e. A /\ z e. A ) /\ ( x R y /\ y R z ) ) <-> ( ( x e. A /\ z e. A ) /\ E. y e. A ( x R y /\ y R z ) ) )
117 115 116 bitr3i 
 |-  ( E. y ( y e. A /\ ( ( x e. A /\ z e. A ) /\ ( x R y /\ y R z ) ) ) <-> ( ( x e. A /\ z e. A ) /\ E. y e. A ( x R y /\ y R z ) ) )
118 110 114 117 3bitr3ri 
 |-  ( ( ( x e. A /\ z e. A ) /\ E. y e. A ( x R y /\ y R z ) ) <-> <. x , z >. e. ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) )
119 df-br 
 |-  ( x R z <-> <. x , z >. e. R )
120 118 119 imbi12i 
 |-  ( ( ( ( x e. A /\ z e. A ) /\ E. y e. A ( x R y /\ y R z ) ) -> x R z ) <-> ( <. x , z >. e. ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) -> <. x , z >. e. R ) )
121 120 2albii 
 |-  ( A. x A. z ( ( ( x e. A /\ z e. A ) /\ E. y e. A ( x R y /\ y R z ) ) -> x R z ) <-> A. x A. z ( <. x , z >. e. ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) -> <. x , z >. e. R ) )
122 r2al 
 |-  ( A. x e. A A. z e. A ( E. y e. A ( x R y /\ y R z ) -> x R z ) <-> A. x A. z ( ( x e. A /\ z e. A ) -> ( E. y e. A ( x R y /\ y R z ) -> x R z ) ) )
123 impexp 
 |-  ( ( ( ( x e. A /\ z e. A ) /\ E. y e. A ( x R y /\ y R z ) ) -> x R z ) <-> ( ( x e. A /\ z e. A ) -> ( E. y e. A ( x R y /\ y R z ) -> x R z ) ) )
124 123 2albii 
 |-  ( A. x A. z ( ( ( x e. A /\ z e. A ) /\ E. y e. A ( x R y /\ y R z ) ) -> x R z ) <-> A. x A. z ( ( x e. A /\ z e. A ) -> ( E. y e. A ( x R y /\ y R z ) -> x R z ) ) )
125 122 124 bitr4i 
 |-  ( A. x e. A A. z e. A ( E. y e. A ( x R y /\ y R z ) -> x R z ) <-> A. x A. z ( ( ( x e. A /\ z e. A ) /\ E. y e. A ( x R y /\ y R z ) ) -> x R z ) )
126 relco 
 |-  Rel ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) )
127 ssrel 
 |-  ( Rel ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) -> ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R <-> A. x A. z ( <. x , z >. e. ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) -> <. x , z >. e. R ) ) )
128 126 127 ax-mp 
 |-  ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R <-> A. x A. z ( <. x , z >. e. ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) -> <. x , z >. e. R ) )
129 121 125 128 3bitr4i 
 |-  ( A. x e. A A. z e. A ( E. y e. A ( x R y /\ y R z ) -> x R z ) <-> ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R )
130 93 129 bitr2i 
 |-  ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R <-> A. x e. A A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) )
131 88 130 anbi12i 
 |-  ( ( ( R i^i ( _I |` A ) ) = (/) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R ) <-> ( A. x e. A -. x R x /\ A. x e. A A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) )
132 33 34 131 3bitr4g 
 |-  ( A =/= (/) -> ( R Po A <-> ( ( R i^i ( _I |` A ) ) = (/) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R ) ) )
133 26 132 pm2.61ine 
 |-  ( R Po A <-> ( ( R i^i ( _I |` A ) ) = (/) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R ) )