Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dfpo2 Structured version   Unicode version

Theorem dfpo2 29428
Description: Quantifier free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013.)
Assertion
Ref Expression
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 of Theorem dfpo2
Dummy variables  x  y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 po0 4804 . . . 4  |-  R  Po  (/)
2 res0 5266 . . . . . . 7  |-  (  _I  |`  (/) )  =  (/)
32ineq2i 3683 . . . . . 6  |-  ( R  i^i  (  _I  |`  (/) ) )  =  ( R  i^i  (/) )
4 in0 3810 . . . . . 6  |-  ( R  i^i  (/) )  =  (/)
53, 4eqtri 2483 . . . . 5  |-  ( R  i^i  (  _I  |`  (/) ) )  =  (/)
6 xp0 5410 . . . . . . . . . 10  |-  ( A  X.  (/) )  =  (/)
76ineq2i 3683 . . . . . . . . 9  |-  ( R  i^i  ( A  X.  (/) ) )  =  ( R  i^i  (/) )
87, 4eqtri 2483 . . . . . . . 8  |-  ( R  i^i  ( A  X.  (/) ) )  =  (/)
98coeq2i 5152 . . . . . . 7  |-  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  =  ( ( R  i^i  ( A  X.  A ) )  o.  (/) )
10 co02 5504 . . . . . . 7  |-  ( ( R  i^i  ( A  X.  A ) )  o.  (/) )  =  (/)
119, 10eqtri 2483 . . . . . 6  |-  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  =  (/)
12 0ss 3813 . . . . . 6  |-  (/)  C_  R
1311, 12eqsstri 3519 . . . . 5  |-  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  C_  R
145, 13pm3.2i 453 . . . 4  |-  ( ( R  i^i  (  _I  |`  (/) ) )  =  (/)  /\  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) ) 
C_  R )
151, 142th 239 . . 3  |-  ( R  Po  (/)  <->  ( ( R  i^i  (  _I  |`  (/) ) )  =  (/)  /\  (
( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  C_  R )
)
16 poeq2 4793 . . . 4  |-  ( A  =  (/)  ->  ( R  Po  A  <->  R  Po  (/) ) )
17 reseq2 5257 . . . . . . 7  |-  ( A  =  (/)  ->  (  _I  |`  A )  =  (  _I  |`  (/) ) )
1817ineq2d 3686 . . . . . 6  |-  ( A  =  (/)  ->  ( R  i^i  (  _I  |`  A ) )  =  ( R  i^i  (  _I  |`  (/) ) ) )
1918eqeq1d 2456 . . . . 5  |-  ( A  =  (/)  ->  ( ( R  i^i  (  _I  |`  A ) )  =  (/) 
<->  ( R  i^i  (  _I  |`  (/) ) )  =  (/) ) )
20 xpeq2 5003 . . . . . . . 8  |-  ( A  =  (/)  ->  ( A  X.  A )  =  ( A  X.  (/) ) )
2120ineq2d 3686 . . . . . . 7  |-  ( A  =  (/)  ->  ( R  i^i  ( A  X.  A ) )  =  ( R  i^i  ( A  X.  (/) ) ) )
2221coeq2d 5154 . . . . . 6  |-  ( 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.  (/) ) ) ) )
2322sseq1d 3516 . . . . 5  |-  ( 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 ) )
2419, 23anbi12d 708 . . . 4  |-  ( 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 )
) )
2516, 24bibi12d 319 . . 3  |-  ( 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 )
) ) )
2615, 25mpbiri 233 . 2  |-  ( 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 3912 . . . . . . 7  |-  ( 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 ) ) ) )
2827ralbidv 2893 . . . . . 6  |-  ( 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 3912 . . . . . 6  |-  ( 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 ) ) ) )
3028, 29bitrd 253 . . . . 5  |-  ( 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 ) ) ) )
3130ralbidv 2893 . . . 4  |-  ( 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 2981 . . . 4  |-  ( 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 ) ) )
3331, 32syl6bb 261 . . 3  |-  ( 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 4789 . . 3  |-  ( 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 3855 . . . . 5  |-  ( ( R  i^i  (  _I  |`  A ) )  =  (/) 
<-> 
A. w  e.  R  -.  w  e.  (  _I  |`  A ) )
36 df-ral 2809 . . . . 5  |-  ( A. w  e.  R  -.  w  e.  (  _I  |`  A )  <->  A. w
( w  e.  R  ->  -.  w  e.  (  _I  |`  A )
) )
37 opex 4701 . . . . . . . . . 10  |-  <. x ,  x >.  e.  _V
38 eleq1 2526 . . . . . . . . . . . 12  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  R  <->  <. x ,  x >.  e.  R ) )
39 df-br 4440 . . . . . . . . . . . 12  |-  ( x R x  <->  <. x ,  x >.  e.  R
)
4038, 39syl6bbr 263 . . . . . . . . . . 11  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  R  <->  x R x ) )
41 eleq1 2526 . . . . . . . . . . . . 13  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  (  _I  |`  A )  <->  <. x ,  x >.  e.  (  _I  |`  A ) ) )
42 vex 3109 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
43 ididg 5145 . . . . . . . . . . . . . . . 16  |-  ( x  e.  _V  ->  x  _I  x )
4442, 43ax-mp 5 . . . . . . . . . . . . . . 15  |-  x  _I  x
4542brres 5268 . . . . . . . . . . . . . . 15  |-  ( x (  _I  |`  A ) x  <->  ( x  _I  x  /\  x  e.  A ) )
4644, 45mpbiran 916 . . . . . . . . . . . . . 14  |-  ( x (  _I  |`  A ) x  <->  x  e.  A
)
47 df-br 4440 . . . . . . . . . . . . . 14  |-  ( x (  _I  |`  A ) x  <->  <. x ,  x >.  e.  (  _I  |`  A ) )
4846, 47bitr3i 251 . . . . . . . . . . . . 13  |-  ( x  e.  A  <->  <. x ,  x >.  e.  (  _I  |`  A ) )
4941, 48syl6bbr 263 . . . . . . . . . . . 12  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  (  _I  |`  A )  <-> 
x  e.  A ) )
5049notbid 292 . . . . . . . . . . 11  |-  ( w  =  <. x ,  x >.  ->  ( -.  w  e.  (  _I  |`  A )  <->  -.  x  e.  A
) )
5140, 50imbi12d 318 . . . . . . . . . 10  |-  ( w  =  <. x ,  x >.  ->  ( ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  <->  ( x R x  ->  -.  x  e.  A ) ) )
5237, 51spcv 3197 . . . . . . . . 9  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  ->  ( x R x  ->  -.  x  e.  A ) )
5352con2d 115 . . . . . . . 8  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  ->  ( x  e.  A  ->  -.  x R x ) )
5453alrimiv 1724 . . . . . . 7  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  ->  A. x
( x  e.  A  ->  -.  x R x ) )
55 relres 5289 . . . . . . . . . . . 12  |-  Rel  (  _I  |`  A )
56 elrel 5093 . . . . . . . . . . . 12  |-  ( ( Rel  (  _I  |`  A )  /\  w  e.  (  _I  |`  A )
)  ->  E. y E. z  w  =  <. y ,  z >.
)
5755, 56mpan 668 . . . . . . . . . . 11  |-  ( w  e.  (  _I  |`  A )  ->  E. y E. z  w  =  <. y ,  z >. )
5857ancri 550 . . . . . . . . . 10  |-  ( w  e.  (  _I  |`  A )  ->  ( E. y E. z  w  =  <. y ,  z >.  /\  w  e.  (  _I  |`  A ) ) )
59 eleq1 2526 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )
60 breq12 4444 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  =  y  /\  x  =  y )  ->  ( x R x  <-> 
y R y ) )
6160anidms 643 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
x R x  <->  y R
y ) )
6261notbid 292 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  ( -.  x R x  <->  -.  y R y ) )
6359, 62imbi12d 318 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
( x  e.  A  ->  -.  x R x )  <->  ( y  e.  A  ->  -.  y R y ) ) )
6463spv 2016 . . . . . . . . . . . . . 14  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( y  e.  A  ->  -.  y R y ) )
65 breq2 4443 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  z  ->  (
y R y  <->  y R
z ) )
6665notbid 292 . . . . . . . . . . . . . . . . 17  |-  ( y  =  z  ->  ( -.  y R y  <->  -.  y R z ) )
6766imbi2d 314 . . . . . . . . . . . . . . . 16  |-  ( y  =  z  ->  (
( y  e.  A  ->  -.  y R y )  <->  ( y  e.  A  ->  -.  y R z ) ) )
6867biimpcd 224 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  A  ->  -.  y R y )  ->  ( y  =  z  ->  ( y  e.  A  ->  -.  y R z ) ) )
6968impd 429 . . . . . . . . . . . . . 14  |-  ( ( y  e.  A  ->  -.  y R y )  ->  ( ( y  =  z  /\  y  e.  A )  ->  -.  y R z ) )
7064, 69syl 16 . . . . . . . . . . . . 13  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( ( y  =  z  /\  y  e.  A )  ->  -.  y R z ) )
71 eleq1 2526 . . . . . . . . . . . . . . 15  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  (  _I  |`  A )  <->  <. y ,  z >.  e.  (  _I  |`  A ) ) )
72 vex 3109 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
7372brres 5268 . . . . . . . . . . . . . . . 16  |-  ( y (  _I  |`  A ) z  <->  ( y  _I  z  /\  y  e.  A ) )
74 df-br 4440 . . . . . . . . . . . . . . . 16  |-  ( y (  _I  |`  A ) z  <->  <. y ,  z
>.  e.  (  _I  |`  A ) )
7572ideq 5144 . . . . . . . . . . . . . . . . 17  |-  ( y  _I  z  <->  y  =  z )
7675anbi1i 693 . . . . . . . . . . . . . . . 16  |-  ( ( y  _I  z  /\  y  e.  A )  <->  ( y  =  z  /\  y  e.  A )
)
7773, 74, 763bitr3ri 276 . . . . . . . . . . . . . . 15  |-  ( ( y  =  z  /\  y  e.  A )  <->  <.
y ,  z >.  e.  (  _I  |`  A ) )
7871, 77syl6bbr 263 . . . . . . . . . . . . . 14  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  (  _I  |`  A )  <-> 
( y  =  z  /\  y  e.  A
) ) )
79 eleq1 2526 . . . . . . . . . . . . . . . 16  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  R  <->  <. y ,  z
>.  e.  R ) )
80 df-br 4440 . . . . . . . . . . . . . . . 16  |-  ( y R z  <->  <. y ,  z >.  e.  R
)
8179, 80syl6bbr 263 . . . . . . . . . . . . . . 15  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  R  <->  y R z ) )
8281notbid 292 . . . . . . . . . . . . . 14  |-  ( w  =  <. y ,  z
>.  ->  ( -.  w  e.  R  <->  -.  y R
z ) )
8378, 82imbi12d 318 . . . . . . . . . . . . 13  |-  ( w  =  <. y ,  z
>.  ->  ( ( w  e.  (  _I  |`  A )  ->  -.  w  e.  R )  <->  ( (
y  =  z  /\  y  e.  A )  ->  -.  y R z ) ) )
8470, 83syl5ibrcom 222 . . . . . . . . . . . 12  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( w  =  <. y ,  z >.  ->  (
w  e.  (  _I  |`  A )  ->  -.  w  e.  R )
) )
8584exlimdvv 1730 . . . . . . . . . . 11  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( E. y E. z  w  =  <. y ,  z >.  ->  (
w  e.  (  _I  |`  A )  ->  -.  w  e.  R )
) )
8685impd 429 . . . . . . . . . 10  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( ( E. y E. z  w  =  <. y ,  z >.  /\  w  e.  (  _I  |`  A ) )  ->  -.  w  e.  R ) )
8758, 86syl5 32 . . . . . . . . 9  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( w  e.  (  _I  |`  A )  ->  -.  w  e.  R
) )
8887con2d 115 . . . . . . . 8  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( w  e.  R  ->  -.  w  e.  (  _I  |`  A )
) )
8988alrimiv 1724 . . . . . . 7  |-  ( A. x ( x  e.  A  ->  -.  x R x )  ->  A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) ) )
9054, 89impbii 188 . . . . . 6  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  <->  A. x ( x  e.  A  ->  -.  x R x ) )
91 df-ral 2809 . . . . . 6  |-  ( A. x  e.  A  -.  x R x  <->  A. x
( x  e.  A  ->  -.  x R x ) )
9290, 91bitr4i 252 . . . . 5  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  <->  A. x  e.  A  -.  x R x )
9335, 36, 923bitri 271 . . . 4  |-  ( ( R  i^i  (  _I  |`  A ) )  =  (/) 
<-> 
A. x  e.  A  -.  x R x )
94 ralcom 3015 . . . . . . 7  |-  ( 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 ) )
95 r19.23v 2934 . . . . . . . 8  |-  ( 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 ) )
9695ralbii 2885 . . . . . . 7  |-  ( 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 ) )
9794, 96bitri 249 . . . . . 6  |-  ( 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 ) )
9897ralbii 2885 . . . . 5  |-  ( 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 ) )
99 brin 4488 . . . . . . . . . . . 12  |-  ( x ( R  i^i  ( A  X.  A ) ) y  <->  ( x R y  /\  x ( A  X.  A ) y ) )
100 brin 4488 . . . . . . . . . . . 12  |-  ( y ( R  i^i  ( A  X.  A ) ) z  <->  ( y R z  /\  y ( A  X.  A ) z ) )
10199, 100anbi12i 695 . . . . . . . . . . 11  |-  ( ( 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 ) ) )
102 an4 822 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
103 ancom 448 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
104 ancom 448 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  A  /\  y  e.  A )  <->  ( y  e.  A  /\  x  e.  A )
)
105104anbi1i 693 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  A  /\  y  e.  A
)  /\  ( y  e.  A  /\  z  e.  A ) )  <->  ( (
y  e.  A  /\  x  e.  A )  /\  ( y  e.  A  /\  z  e.  A
) ) )
106 brxp 5019 . . . . . . . . . . . . . . 15  |-  ( x ( A  X.  A
) y  <->  ( x  e.  A  /\  y  e.  A ) )
107 brxp 5019 . . . . . . . . . . . . . . 15  |-  ( y ( A  X.  A
) z  <->  ( y  e.  A  /\  z  e.  A ) )
108106, 107anbi12i 695 . . . . . . . . . . . . . 14  |-  ( ( x ( A  X.  A ) y  /\  y ( A  X.  A ) z )  <-> 
( ( x  e.  A  /\  y  e.  A )  /\  (
y  e.  A  /\  z  e.  A )
) )
109 anandi 826 . . . . . . . . . . . . . 14  |-  ( ( y  e.  A  /\  ( x  e.  A  /\  z  e.  A
) )  <->  ( (
y  e.  A  /\  x  e.  A )  /\  ( y  e.  A  /\  z  e.  A
) ) )
110105, 108, 1093bitr4i 277 . . . . . . . . . . . . 13  |-  ( ( x ( A  X.  A ) y  /\  y ( A  X.  A ) z )  <-> 
( y  e.  A  /\  ( x  e.  A  /\  z  e.  A
) ) )
111110anbi1i 693 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
112102, 103, 1113bitri 271 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
113 anass 647 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) )
114101, 112, 1133bitri 271 . . . . . . . . . 10  |-  ( ( 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 ) ) ) )
115114exbii 1672 . . . . . . . . 9  |-  ( 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 ) ) ) )
11642, 72brco 5162 . . . . . . . . . 10  |-  ( 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 ) )
117 df-br 4440 . . . . . . . . . 10  |-  ( 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 ) ) ) )
118116, 117bitr3i 251 . . . . . . . . 9  |-  ( 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
) ) ) )
119 df-rex 2810 . . . . . . . . . 10  |-  ( 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 ) ) ) )
120 r19.42v 3009 . . . . . . . . . 10  |-  ( 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 ) ) )
121119, 120bitr3i 251 . . . . . . . . 9  |-  ( 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 ) ) )
122115, 118, 1213bitr3ri 276 . . . . . . . 8  |-  ( ( ( 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 ) ) ) )
123 df-br 4440 . . . . . . . 8  |-  ( x R z  <->  <. x ,  z >.  e.  R
)
124122, 123imbi12i 324 . . . . . . 7  |-  ( ( ( ( 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 ) )
1251242albii 1646 . . . . . 6  |-  ( 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
) )
126 r2al 2832 . . . . . . 7  |-  ( 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 ) ) )
127 impexp 444 . . . . . . . 8  |-  ( ( ( ( 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 ) ) )
1281272albii 1646 . . . . . . 7  |-  ( 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 ) ) )
129126, 128bitr4i 252 . . . . . 6  |-  ( 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 ) )
130 relco 5488 . . . . . . 7  |-  Rel  (
( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  A
) ) )
131 ssrel 5079 . . . . . . 7  |-  ( 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
) ) )
132130, 131ax-mp 5 . . . . . 6  |-  ( ( ( 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
) )
133125, 129, 1323bitr4i 277 . . . . 5  |-  ( 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 )
13498, 133bitr2i 250 . . . 4  |-  ( ( ( 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 ) )
13593, 134anbi12i 695 . . 3  |-  ( ( ( 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 ) ) )
13633, 34, 1353bitr4g 288 . 2  |-  ( A  =/=  (/)  ->  ( R  Po  A  <->  ( ( R  i^i  (  _I  |`  A ) )  =  (/)  /\  (
( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  A
) ) )  C_  R ) ) )
13726, 136pm2.61ine 2767 1  |-  ( R  Po  A  <->  ( ( R  i^i  (  _I  |`  A ) )  =  (/)  /\  (
( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  A
) ) )  C_  R ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 367   A.wal 1396    = wceq 1398   E.wex 1617    e. wcel 1823    =/= wne 2649   A.wral 2804   E.wrex 2805   _Vcvv 3106    i^i cin 3460    C_ wss 3461   (/)c0 3783   <.cop 4022   class class class wbr 4439    _I cid 4779    Po wpo 4787    X. cxp 4986    |` cres 4990    o. ccom 4992   Rel wrel 4993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-id 4784  df-po 4789  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-res 5000
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator