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

Theorem dfpo2 27570
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 4661 . . . 4  |-  R  Po  (/)
2 res0 5120 . . . . . . 7  |-  (  _I  |`  (/) )  =  (/)
32ineq2i 3554 . . . . . 6  |-  ( R  i^i  (  _I  |`  (/) ) )  =  ( R  i^i  (/) )
4 in0 3668 . . . . . 6  |-  ( R  i^i  (/) )  =  (/)
53, 4eqtri 2463 . . . . 5  |-  ( R  i^i  (  _I  |`  (/) ) )  =  (/)
6 xp0 5261 . . . . . . . . . 10  |-  ( A  X.  (/) )  =  (/)
76ineq2i 3554 . . . . . . . . 9  |-  ( R  i^i  ( A  X.  (/) ) )  =  ( R  i^i  (/) )
87, 4eqtri 2463 . . . . . . . 8  |-  ( R  i^i  ( A  X.  (/) ) )  =  (/)
98coeq2i 5005 . . . . . . 7  |-  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  =  ( ( R  i^i  ( A  X.  A ) )  o.  (/) )
10 co02 5356 . . . . . . 7  |-  ( ( R  i^i  ( A  X.  A ) )  o.  (/) )  =  (/)
119, 10eqtri 2463 . . . . . 6  |-  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  =  (/)
12 0ss 3671 . . . . . 6  |-  (/)  C_  R
1311, 12eqsstri 3391 . . . . 5  |-  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  C_  R
145, 13pm3.2i 455 . . . 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 4650 . . . 4  |-  ( A  =  (/)  ->  ( R  Po  A  <->  R  Po  (/) ) )
17 reseq2 5110 . . . . . . 7  |-  ( A  =  (/)  ->  (  _I  |`  A )  =  (  _I  |`  (/) ) )
1817ineq2d 3557 . . . . . 6  |-  ( A  =  (/)  ->  ( R  i^i  (  _I  |`  A ) )  =  ( R  i^i  (  _I  |`  (/) ) ) )
1918eqeq1d 2451 . . . . 5  |-  ( A  =  (/)  ->  ( ( R  i^i  (  _I  |`  A ) )  =  (/) 
<->  ( R  i^i  (  _I  |`  (/) ) )  =  (/) ) )
20 xpeq2 4860 . . . . . . . 8  |-  ( A  =  (/)  ->  ( A  X.  A )  =  ( A  X.  (/) ) )
2120ineq2d 3557 . . . . . . 7  |-  ( A  =  (/)  ->  ( R  i^i  ( A  X.  A ) )  =  ( R  i^i  ( A  X.  (/) ) ) )
2221coeq2d 5007 . . . . . 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 3388 . . . . 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 710 . . . 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 321 . . 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 3780 . . . . . . 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 2740 . . . . . 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 3780 . . . . . 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 2740 . . . 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 2854 . . . 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 4646 . . 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 3724 . . . . 5  |-  ( ( R  i^i  (  _I  |`  A ) )  =  (/) 
<-> 
A. w  e.  R  -.  w  e.  (  _I  |`  A ) )
36 df-ral 2725 . . . . 5  |-  ( A. w  e.  R  -.  w  e.  (  _I  |`  A )  <->  A. w
( w  e.  R  ->  -.  w  e.  (  _I  |`  A )
) )
37 opex 4561 . . . . . . . . . 10  |-  <. x ,  x >.  e.  _V
38 eleq1 2503 . . . . . . . . . . . 12  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  R  <->  <. x ,  x >.  e.  R ) )
39 df-br 4298 . . . . . . . . . . . 12  |-  ( x R x  <->  <. x ,  x >.  e.  R
)
4038, 39syl6bbr 263 . . . . . . . . . . 11  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  R  <->  x R x ) )
41 eleq1 2503 . . . . . . . . . . . . 13  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  (  _I  |`  A )  <->  <. x ,  x >.  e.  (  _I  |`  A ) ) )
42 vex 2980 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
43 ididg 4998 . . . . . . . . . . . . . . . 16  |-  ( x  e.  _V  ->  x  _I  x )
4442, 43ax-mp 5 . . . . . . . . . . . . . . 15  |-  x  _I  x
4542brres 5122 . . . . . . . . . . . . . . 15  |-  ( x (  _I  |`  A ) x  <->  ( x  _I  x  /\  x  e.  A ) )
4644, 45mpbiran 909 . . . . . . . . . . . . . 14  |-  ( x (  _I  |`  A ) x  <->  x  e.  A
)
47 df-br 4298 . . . . . . . . . . . . . 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 294 . . . . . . . . . . 11  |-  ( w  =  <. x ,  x >.  ->  ( -.  w  e.  (  _I  |`  A )  <->  -.  x  e.  A
) )
5140, 50imbi12d 320 . . . . . . . . . 10  |-  ( w  =  <. x ,  x >.  ->  ( ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  <->  ( x R x  ->  -.  x  e.  A ) ) )
5237, 51spcv 3068 . . . . . . . . 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 1685 . . . . . . 7  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  ->  A. x
( x  e.  A  ->  -.  x R x ) )
55 relres 5143 . . . . . . . . . . . 12  |-  Rel  (  _I  |`  A )
56 elrel 4947 . . . . . . . . . . . 12  |-  ( ( Rel  (  _I  |`  A )  /\  w  e.  (  _I  |`  A )
)  ->  E. y E. z  w  =  <. y ,  z >.
)
5755, 56mpan 670 . . . . . . . . . . 11  |-  ( w  e.  (  _I  |`  A )  ->  E. y E. z  w  =  <. y ,  z >. )
5857ancri 552 . . . . . . . . . 10  |-  ( w  e.  (  _I  |`  A )  ->  ( E. y E. z  w  =  <. y ,  z >.  /\  w  e.  (  _I  |`  A ) ) )
59 eleq1 2503 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )
60 breq12 4302 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  =  y  /\  x  =  y )  ->  ( x R x  <-> 
y R y ) )
6160anidms 645 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
x R x  <->  y R
y ) )
6261notbid 294 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  ( -.  x R x  <->  -.  y R y ) )
6359, 62imbi12d 320 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
( x  e.  A  ->  -.  x R x )  <->  ( y  e.  A  ->  -.  y R y ) ) )
6463spv 1955 . . . . . . . . . . . . . 14  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( y  e.  A  ->  -.  y R y ) )
65 breq2 4301 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  z  ->  (
y R y  <->  y R
z ) )
6665notbid 294 . . . . . . . . . . . . . . . . 17  |-  ( y  =  z  ->  ( -.  y R y  <->  -.  y R z ) )
6766imbi2d 316 . . . . . . . . . . . . . . . 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 431 . . . . . . . . . . . . . 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 2503 . . . . . . . . . . . . . . 15  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  (  _I  |`  A )  <->  <. y ,  z >.  e.  (  _I  |`  A ) ) )
72 vex 2980 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
7372brres 5122 . . . . . . . . . . . . . . . 16  |-  ( y (  _I  |`  A ) z  <->  ( y  _I  z  /\  y  e.  A ) )
74 df-br 4298 . . . . . . . . . . . . . . . 16  |-  ( y (  _I  |`  A ) z  <->  <. y ,  z
>.  e.  (  _I  |`  A ) )
7572ideq 4997 . . . . . . . . . . . . . . . . 17  |-  ( y  _I  z  <->  y  =  z )
7675anbi1i 695 . . . . . . . . . . . . . . . 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 2503 . . . . . . . . . . . . . . . 16  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  R  <->  <. y ,  z
>.  e.  R ) )
80 df-br 4298 . . . . . . . . . . . . . . . 16  |-  ( y R z  <->  <. y ,  z >.  e.  R
)
8179, 80syl6bbr 263 . . . . . . . . . . . . . . 15  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  R  <->  y R z ) )
8281notbid 294 . . . . . . . . . . . . . 14  |-  ( w  =  <. y ,  z
>.  ->  ( -.  w  e.  R  <->  -.  y R
z ) )
8378, 82imbi12d 320 . . . . . . . . . . . . 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 1691 . . . . . . . . . . 11  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( E. y E. z  w  =  <. y ,  z >.  ->  (
w  e.  (  _I  |`  A )  ->  -.  w  e.  R )
) )
8685impd 431 . . . . . . . . . 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 1685 . . . . . . 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 2725 . . . . . 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 2886 . . . . . . 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 2838 . . . . . . . 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 2744 . . . . . . 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 2744 . . . . 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 4346 . . . . . . . . . . . 12  |-  ( x ( R  i^i  ( A  X.  A ) ) y  <->  ( x R y  /\  x ( A  X.  A ) y ) )
100 brin 4346 . . . . . . . . . . . 12  |-  ( y ( R  i^i  ( A  X.  A ) ) z  <->  ( y R z  /\  y ( A  X.  A ) z ) )
10199, 100anbi12i 697 . . . . . . . . . . 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 820 . . . . . . . . . . . 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 450 . . . . . . . . . . . 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 450 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  A  /\  y  e.  A )  <->  ( y  e.  A  /\  x  e.  A )
)
105104anbi1i 695 . . . . . . . . . . . . . 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 4875 . . . . . . . . . . . . . . 15  |-  ( x ( A  X.  A
) y  <->  ( x  e.  A  /\  y  e.  A ) )
107 brxp 4875 . . . . . . . . . . . . . . 15  |-  ( y ( A  X.  A
) z  <->  ( y  e.  A  /\  z  e.  A ) )
108106, 107anbi12i 697 . . . . . . . . . . . . . 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 824 . . . . . . . . . . . . . 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 695 . . . . . . . . . . . 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 649 . . . . . . . . . . 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 1634 . . . . . . . . 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 5015 . . . . . . . . . 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 4298 . . . . . . . . . 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 2726 . . . . . . . . . 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 2880 . . . . . . . . . 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 4298 . . . . . . . 8  |-  ( x R z  <->  <. x ,  z >.  e.  R
)
124122, 123imbi12i 326 . . . . . . 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 1611 . . . . . 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 2757 . . . . . . 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 446 . . . . . . . 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 1611 . . . . . . 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 5341 . . . . . . 7  |-  Rel  (
( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  A
) ) )
131 ssrel 4933 . . . . . . 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 697 . . 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 2692 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 369   A.wal 1367    = wceq 1369   E.wex 1586    e. wcel 1756    =/= wne 2611   A.wral 2720   E.wrex 2721   _Vcvv 2977    i^i cin 3332    C_ wss 3333   (/)c0 3642   <.cop 3888   class class class wbr 4297    _I cid 4636    Po wpo 4644    X. cxp 4843    |` cres 4847    o. ccom 4849   Rel wrel 4850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pr 4536
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-br 4298  df-opab 4356  df-id 4641  df-po 4646  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-res 4857
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator