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

Theorem dfpo2 25330
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 4482 . . . 4  |-  R  Po  (/)
2 res0 5113 . . . . . . 7  |-  (  _I  |`  (/) )  =  (/)
32ineq2i 3503 . . . . . 6  |-  ( R  i^i  (  _I  |`  (/) ) )  =  ( R  i^i  (/) )
4 in0 3617 . . . . . 6  |-  ( R  i^i  (/) )  =  (/)
53, 4eqtri 2428 . . . . 5  |-  ( R  i^i  (  _I  |`  (/) ) )  =  (/)
6 xp0 5254 . . . . . . . . . 10  |-  ( A  X.  (/) )  =  (/)
76ineq2i 3503 . . . . . . . . 9  |-  ( R  i^i  ( A  X.  (/) ) )  =  ( R  i^i  (/) )
87, 4eqtri 2428 . . . . . . . 8  |-  ( R  i^i  ( A  X.  (/) ) )  =  (/)
98coeq2i 4996 . . . . . . 7  |-  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  =  ( ( R  i^i  ( A  X.  A ) )  o.  (/) )
10 co02 5346 . . . . . . 7  |-  ( ( R  i^i  ( A  X.  A ) )  o.  (/) )  =  (/)
119, 10eqtri 2428 . . . . . 6  |-  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  =  (/)
12 0ss 3620 . . . . . 6  |-  (/)  C_  R
1311, 12eqsstri 3342 . . . . 5  |-  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  C_  R
145, 13pm3.2i 442 . . . 4  |-  ( ( R  i^i  (  _I  |`  (/) ) )  =  (/)  /\  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) ) 
C_  R )
151, 142th 231 . . 3  |-  ( R  Po  (/)  <->  ( ( R  i^i  (  _I  |`  (/) ) )  =  (/)  /\  (
( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  C_  R )
)
16 poeq2 4471 . . . 4  |-  ( A  =  (/)  ->  ( R  Po  A  <->  R  Po  (/) ) )
17 reseq2 5104 . . . . . . 7  |-  ( A  =  (/)  ->  (  _I  |`  A )  =  (  _I  |`  (/) ) )
1817ineq2d 3506 . . . . . 6  |-  ( A  =  (/)  ->  ( R  i^i  (  _I  |`  A ) )  =  ( R  i^i  (  _I  |`  (/) ) ) )
1918eqeq1d 2416 . . . . 5  |-  ( A  =  (/)  ->  ( ( R  i^i  (  _I  |`  A ) )  =  (/) 
<->  ( R  i^i  (  _I  |`  (/) ) )  =  (/) ) )
20 xpeq2 4856 . . . . . . . 8  |-  ( A  =  (/)  ->  ( A  X.  A )  =  ( A  X.  (/) ) )
2120ineq2d 3506 . . . . . . 7  |-  ( A  =  (/)  ->  ( R  i^i  ( A  X.  A ) )  =  ( R  i^i  ( A  X.  (/) ) ) )
2221coeq2d 4998 . . . . . 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 3339 . . . . 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 692 . . . 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 313 . . 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 225 . 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 3687 . . . . . . 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 2690 . . . . . 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 3687 . . . . . 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 245 . . . . 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 2690 . . . 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 2802 . . . 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 253 . . 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 4467 . . 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 3632 . . . . 5  |-  ( ( R  i^i  (  _I  |`  A ) )  =  (/) 
<-> 
A. w  e.  R  -.  w  e.  (  _I  |`  A ) )
36 df-ral 2675 . . . . 5  |-  ( A. w  e.  R  -.  w  e.  (  _I  |`  A )  <->  A. w
( w  e.  R  ->  -.  w  e.  (  _I  |`  A )
) )
37 opex 4391 . . . . . . . . . 10  |-  <. x ,  x >.  e.  _V
38 eleq1 2468 . . . . . . . . . . . 12  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  R  <->  <. x ,  x >.  e.  R ) )
39 df-br 4177 . . . . . . . . . . . 12  |-  ( x R x  <->  <. x ,  x >.  e.  R
)
4038, 39syl6bbr 255 . . . . . . . . . . 11  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  R  <->  x R x ) )
41 eleq1 2468 . . . . . . . . . . . . 13  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  (  _I  |`  A )  <->  <. x ,  x >.  e.  (  _I  |`  A ) ) )
42 vex 2923 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
43 ididg 4989 . . . . . . . . . . . . . . . 16  |-  ( x  e.  _V  ->  x  _I  x )
4442, 43ax-mp 8 . . . . . . . . . . . . . . 15  |-  x  _I  x
4542brres 5115 . . . . . . . . . . . . . . 15  |-  ( x (  _I  |`  A ) x  <->  ( x  _I  x  /\  x  e.  A ) )
4644, 45mpbiran 885 . . . . . . . . . . . . . 14  |-  ( x (  _I  |`  A ) x  <->  x  e.  A
)
47 df-br 4177 . . . . . . . . . . . . . 14  |-  ( x (  _I  |`  A ) x  <->  <. x ,  x >.  e.  (  _I  |`  A ) )
4846, 47bitr3i 243 . . . . . . . . . . . . 13  |-  ( x  e.  A  <->  <. x ,  x >.  e.  (  _I  |`  A ) )
4941, 48syl6bbr 255 . . . . . . . . . . . 12  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  (  _I  |`  A )  <-> 
x  e.  A ) )
5049notbid 286 . . . . . . . . . . 11  |-  ( w  =  <. x ,  x >.  ->  ( -.  w  e.  (  _I  |`  A )  <->  -.  x  e.  A
) )
5140, 50imbi12d 312 . . . . . . . . . 10  |-  ( w  =  <. x ,  x >.  ->  ( ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  <->  ( x R x  ->  -.  x  e.  A ) ) )
5237, 51spcv 3006 . . . . . . . . 9  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  ->  ( x R x  ->  -.  x  e.  A ) )
5352con2d 109 . . . . . . . 8  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  ->  ( x  e.  A  ->  -.  x R x ) )
5453alrimiv 1638 . . . . . . 7  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  ->  A. x
( x  e.  A  ->  -.  x R x ) )
55 relres 5137 . . . . . . . . . . . 12  |-  Rel  (  _I  |`  A )
56 elrel 4941 . . . . . . . . . . . 12  |-  ( ( Rel  (  _I  |`  A )  /\  w  e.  (  _I  |`  A )
)  ->  E. y E. z  w  =  <. y ,  z >.
)
5755, 56mpan 652 . . . . . . . . . . 11  |-  ( w  e.  (  _I  |`  A )  ->  E. y E. z  w  =  <. y ,  z >. )
5857ancri 536 . . . . . . . . . 10  |-  ( w  e.  (  _I  |`  A )  ->  ( E. y E. z  w  =  <. y ,  z >.  /\  w  e.  (  _I  |`  A ) ) )
59 eleq1 2468 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )
60 breq12 4181 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  =  y  /\  x  =  y )  ->  ( x R x  <-> 
y R y ) )
6160anidms 627 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
x R x  <->  y R
y ) )
6261notbid 286 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  ( -.  x R x  <->  -.  y R y ) )
6359, 62imbi12d 312 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
( x  e.  A  ->  -.  x R x )  <->  ( y  e.  A  ->  -.  y R y ) ) )
6463spv 1963 . . . . . . . . . . . . . 14  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( y  e.  A  ->  -.  y R y ) )
65 breq2 4180 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  z  ->  (
y R y  <->  y R
z ) )
6665notbid 286 . . . . . . . . . . . . . . . . 17  |-  ( y  =  z  ->  ( -.  y R y  <->  -.  y R z ) )
6766imbi2d 308 . . . . . . . . . . . . . . . 16  |-  ( y  =  z  ->  (
( y  e.  A  ->  -.  y R y )  <->  ( y  e.  A  ->  -.  y R z ) ) )
6867biimpcd 216 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  A  ->  -.  y R y )  ->  ( y  =  z  ->  ( y  e.  A  ->  -.  y R z ) ) )
6968imp3a 421 . . . . . . . . . . . . . 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 2468 . . . . . . . . . . . . . . 15  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  (  _I  |`  A )  <->  <. y ,  z >.  e.  (  _I  |`  A ) ) )
72 vex 2923 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
7372brres 5115 . . . . . . . . . . . . . . . 16  |-  ( y (  _I  |`  A ) z  <->  ( y  _I  z  /\  y  e.  A ) )
74 df-br 4177 . . . . . . . . . . . . . . . 16  |-  ( y (  _I  |`  A ) z  <->  <. y ,  z
>.  e.  (  _I  |`  A ) )
7572ideq 4988 . . . . . . . . . . . . . . . . 17  |-  ( y  _I  z  <->  y  =  z )
7675anbi1i 677 . . . . . . . . . . . . . . . 16  |-  ( ( y  _I  z  /\  y  e.  A )  <->  ( y  =  z  /\  y  e.  A )
)
7773, 74, 763bitr3ri 268 . . . . . . . . . . . . . . 15  |-  ( ( y  =  z  /\  y  e.  A )  <->  <.
y ,  z >.  e.  (  _I  |`  A ) )
7871, 77syl6bbr 255 . . . . . . . . . . . . . 14  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  (  _I  |`  A )  <-> 
( y  =  z  /\  y  e.  A
) ) )
79 eleq1 2468 . . . . . . . . . . . . . . . 16  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  R  <->  <. y ,  z
>.  e.  R ) )
80 df-br 4177 . . . . . . . . . . . . . . . 16  |-  ( y R z  <->  <. y ,  z >.  e.  R
)
8179, 80syl6bbr 255 . . . . . . . . . . . . . . 15  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  R  <->  y R z ) )
8281notbid 286 . . . . . . . . . . . . . 14  |-  ( w  =  <. y ,  z
>.  ->  ( -.  w  e.  R  <->  -.  y R
z ) )
8378, 82imbi12d 312 . . . . . . . . . . . . 13  |-  ( w  =  <. y ,  z
>.  ->  ( ( w  e.  (  _I  |`  A )  ->  -.  w  e.  R )  <->  ( (
y  =  z  /\  y  e.  A )  ->  -.  y R z ) ) )
8470, 83syl5ibrcom 214 . . . . . . . . . . . 12  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( w  =  <. y ,  z >.  ->  (
w  e.  (  _I  |`  A )  ->  -.  w  e.  R )
) )
8584exlimdvv 1644 . . . . . . . . . . 11  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( E. y E. z  w  =  <. y ,  z >.  ->  (
w  e.  (  _I  |`  A )  ->  -.  w  e.  R )
) )
8685imp3a 421 . . . . . . . . . 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 30 . . . . . . . . 9  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( w  e.  (  _I  |`  A )  ->  -.  w  e.  R
) )
8887con2d 109 . . . . . . . 8  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( w  e.  R  ->  -.  w  e.  (  _I  |`  A )
) )
8988alrimiv 1638 . . . . . . 7  |-  ( A. x ( x  e.  A  ->  -.  x R x )  ->  A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) ) )
9054, 89impbii 181 . . . . . 6  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  <->  A. x ( x  e.  A  ->  -.  x R x ) )
91 df-ral 2675 . . . . . 6  |-  ( A. x  e.  A  -.  x R x  <->  A. x
( x  e.  A  ->  -.  x R x ) )
9290, 91bitr4i 244 . . . . 5  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  <->  A. x  e.  A  -.  x R x )
9335, 36, 923bitri 263 . . . 4  |-  ( ( R  i^i  (  _I  |`  A ) )  =  (/) 
<-> 
A. x  e.  A  -.  x R x )
94 ralcom 2832 . . . . . . 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 2786 . . . . . . . 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 2694 . . . . . . 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 241 . . . . . 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 2694 . . . . 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 4223 . . . . . . . . . . . 12  |-  ( x ( R  i^i  ( A  X.  A ) ) y  <->  ( x R y  /\  x ( A  X.  A ) y ) )
100 brin 4223 . . . . . . . . . . . 12  |-  ( y ( R  i^i  ( A  X.  A ) ) z  <->  ( y R z  /\  y ( A  X.  A ) z ) )
10199, 100anbi12i 679 . . . . . . . . . . 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 798 . . . . . . . . . . . 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 438 . . . . . . . . . . . 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 438 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  A  /\  y  e.  A )  <->  ( y  e.  A  /\  x  e.  A )
)
105104anbi1i 677 . . . . . . . . . . . . . 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 4872 . . . . . . . . . . . . . . 15  |-  ( x ( A  X.  A
) y  <->  ( x  e.  A  /\  y  e.  A ) )
107 brxp 4872 . . . . . . . . . . . . . . 15  |-  ( y ( A  X.  A
) z  <->  ( y  e.  A  /\  z  e.  A ) )
108106, 107anbi12i 679 . . . . . . . . . . . . . 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 802 . . . . . . . . . . . . . 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 269 . . . . . . . . . . . . 13  |-  ( ( x ( A  X.  A ) y  /\  y ( A  X.  A ) z )  <-> 
( y  e.  A  /\  ( x  e.  A  /\  z  e.  A
) ) )
111110anbi1i 677 . . . . . . . . . . . 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 263 . . . . . . . . . . 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 631 . . . . . . . . . . 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 263 . . . . . . . . . 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 1589 . . . . . . . . 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 5006 . . . . . . . . . 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 4177 . . . . . . . . . 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 243 . . . . . . . . 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 2676 . . . . . . . . . 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 2826 . . . . . . . . . 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 243 . . . . . . . . 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 268 . . . . . . . 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 4177 . . . . . . . 8  |-  ( x R z  <->  <. x ,  z >.  e.  R
)
124122, 123imbi12i 317 . . . . . . 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 1573 . . . . . 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 2707 . . . . . . 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 434 . . . . . . . 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 1573 . . . . . . 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 244 . . . . . 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 5331 . . . . . . 7  |-  Rel  (
( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  A
) ) )
131 ssrel 4927 . . . . . . 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 8 . . . . . 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 269 . . . . 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 242 . . . 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 679 . . 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 280 . 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 2647 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 set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1546   E.wex 1547    = wceq 1649    e. wcel 1721    =/= wne 2571   A.wral 2670   E.wrex 2671   _Vcvv 2920    i^i cin 3283    C_ wss 3284   (/)c0 3592   <.cop 3781   class class class wbr 4176    _I cid 4457    Po wpo 4465    X. cxp 4839    |` cres 4843    o. ccom 4845   Rel wrel 4846
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-br 4177  df-opab 4231  df-id 4462  df-po 4467  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-res 4853
  Copyright terms: Public domain W3C validator