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

Theorem dfpo2 30443
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 4788 . . . 4  |-  R  Po  (/)
2 res0 5127 . . . . . . 7  |-  (  _I  |`  (/) )  =  (/)
32ineq2i 3642 . . . . . 6  |-  ( R  i^i  (  _I  |`  (/) ) )  =  ( R  i^i  (/) )
4 in0 3771 . . . . . 6  |-  ( R  i^i  (/) )  =  (/)
53, 4eqtri 2483 . . . . 5  |-  ( R  i^i  (  _I  |`  (/) ) )  =  (/)
6 xp0 5273 . . . . . . . . . 10  |-  ( A  X.  (/) )  =  (/)
76ineq2i 3642 . . . . . . . . 9  |-  ( R  i^i  ( A  X.  (/) ) )  =  ( R  i^i  (/) )
87, 4eqtri 2483 . . . . . . . 8  |-  ( R  i^i  ( A  X.  (/) ) )  =  (/)
98coeq2i 5013 . . . . . . 7  |-  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  =  ( ( R  i^i  ( A  X.  A ) )  o.  (/) )
10 co02 5367 . . . . . . 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 3774 . . . . . 6  |-  (/)  C_  R
1311, 12eqsstri 3473 . . . . 5  |-  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  C_  R
145, 13pm3.2i 461 . . . 4  |-  ( ( R  i^i  (  _I  |`  (/) ) )  =  (/)  /\  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) ) 
C_  R )
151, 142th 247 . . 3  |-  ( R  Po  (/)  <->  ( ( R  i^i  (  _I  |`  (/) ) )  =  (/)  /\  (
( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  C_  R )
)
16 poeq2 4777 . . . 4  |-  ( A  =  (/)  ->  ( R  Po  A  <->  R  Po  (/) ) )
17 reseq2 5118 . . . . . . 7  |-  ( A  =  (/)  ->  (  _I  |`  A )  =  (  _I  |`  (/) ) )
1817ineq2d 3645 . . . . . 6  |-  ( A  =  (/)  ->  ( R  i^i  (  _I  |`  A ) )  =  ( R  i^i  (  _I  |`  (/) ) ) )
1918eqeq1d 2463 . . . . 5  |-  ( A  =  (/)  ->  ( ( R  i^i  (  _I  |`  A ) )  =  (/) 
<->  ( R  i^i  (  _I  |`  (/) ) )  =  (/) ) )
20 xpeq2 4867 . . . . . . . 8  |-  ( A  =  (/)  ->  ( A  X.  A )  =  ( A  X.  (/) ) )
2120ineq2d 3645 . . . . . . 7  |-  ( A  =  (/)  ->  ( R  i^i  ( A  X.  A ) )  =  ( R  i^i  ( A  X.  (/) ) ) )
2221coeq2d 5015 . . . . . 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 3470 . . . . 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 722 . . . 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 327 . . 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 241 . 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 3875 . . . . . . 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 2838 . . . . . 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 3875 . . . . . 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 261 . . . . 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 2838 . . . 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 2928 . . . 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 269 . . 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 4773 . . 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 3816 . . . . 5  |-  ( ( R  i^i  (  _I  |`  A ) )  =  (/) 
<-> 
A. w  e.  R  -.  w  e.  (  _I  |`  A ) )
36 df-ral 2753 . . . . 5  |-  ( A. w  e.  R  -.  w  e.  (  _I  |`  A )  <->  A. w
( w  e.  R  ->  -.  w  e.  (  _I  |`  A )
) )
37 opex 4677 . . . . . . . . . 10  |-  <. x ,  x >.  e.  _V
38 eleq1 2527 . . . . . . . . . . . 12  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  R  <->  <. x ,  x >.  e.  R ) )
39 df-br 4416 . . . . . . . . . . . 12  |-  ( x R x  <->  <. x ,  x >.  e.  R
)
4038, 39syl6bbr 271 . . . . . . . . . . 11  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  R  <->  x R x ) )
41 eleq1 2527 . . . . . . . . . . . . 13  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  (  _I  |`  A )  <->  <. x ,  x >.  e.  (  _I  |`  A ) ) )
42 vex 3059 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
43 ididg 5006 . . . . . . . . . . . . . . . 16  |-  ( x  e.  _V  ->  x  _I  x )
4442, 43ax-mp 5 . . . . . . . . . . . . . . 15  |-  x  _I  x
4542brres 5129 . . . . . . . . . . . . . . 15  |-  ( x (  _I  |`  A ) x  <->  ( x  _I  x  /\  x  e.  A ) )
4644, 45mpbiran 934 . . . . . . . . . . . . . 14  |-  ( x (  _I  |`  A ) x  <->  x  e.  A
)
47 df-br 4416 . . . . . . . . . . . . . 14  |-  ( x (  _I  |`  A ) x  <->  <. x ,  x >.  e.  (  _I  |`  A ) )
4846, 47bitr3i 259 . . . . . . . . . . . . 13  |-  ( x  e.  A  <->  <. x ,  x >.  e.  (  _I  |`  A ) )
4941, 48syl6bbr 271 . . . . . . . . . . . 12  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  (  _I  |`  A )  <-> 
x  e.  A ) )
5049notbid 300 . . . . . . . . . . 11  |-  ( w  =  <. x ,  x >.  ->  ( -.  w  e.  (  _I  |`  A )  <->  -.  x  e.  A
) )
5140, 50imbi12d 326 . . . . . . . . . 10  |-  ( w  =  <. x ,  x >.  ->  ( ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  <->  ( x R x  ->  -.  x  e.  A ) ) )
5237, 51spcv 3151 . . . . . . . . 9  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  ->  ( x R x  ->  -.  x  e.  A ) )
5352con2d 120 . . . . . . . 8  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  ->  ( x  e.  A  ->  -.  x R x ) )
5453alrimiv 1783 . . . . . . 7  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  ->  A. x
( x  e.  A  ->  -.  x R x ) )
55 relres 5150 . . . . . . . . . . . 12  |-  Rel  (  _I  |`  A )
56 elrel 4955 . . . . . . . . . . . 12  |-  ( ( Rel  (  _I  |`  A )  /\  w  e.  (  _I  |`  A )
)  ->  E. y E. z  w  =  <. y ,  z >.
)
5755, 56mpan 681 . . . . . . . . . . 11  |-  ( w  e.  (  _I  |`  A )  ->  E. y E. z  w  =  <. y ,  z >. )
5857ancri 559 . . . . . . . . . 10  |-  ( w  e.  (  _I  |`  A )  ->  ( E. y E. z  w  =  <. y ,  z >.  /\  w  e.  (  _I  |`  A ) ) )
59 eleq1 2527 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )
60 breq12 4420 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  =  y  /\  x  =  y )  ->  ( x R x  <-> 
y R y ) )
6160anidms 655 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
x R x  <->  y R
y ) )
6261notbid 300 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  ( -.  x R x  <->  -.  y R y ) )
6359, 62imbi12d 326 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
( x  e.  A  ->  -.  x R x )  <->  ( y  e.  A  ->  -.  y R y ) ) )
6463spv 2114 . . . . . . . . . . . . . 14  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( y  e.  A  ->  -.  y R y ) )
65 breq2 4419 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  z  ->  (
y R y  <->  y R
z ) )
6665notbid 300 . . . . . . . . . . . . . . . . 17  |-  ( y  =  z  ->  ( -.  y R y  <->  -.  y R z ) )
6766imbi2d 322 . . . . . . . . . . . . . . . 16  |-  ( y  =  z  ->  (
( y  e.  A  ->  -.  y R y )  <->  ( y  e.  A  ->  -.  y R z ) ) )
6867biimpcd 232 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  A  ->  -.  y R y )  ->  ( y  =  z  ->  ( y  e.  A  ->  -.  y R z ) ) )
6968impd 437 . . . . . . . . . . . . . 14  |-  ( ( y  e.  A  ->  -.  y R y )  ->  ( ( y  =  z  /\  y  e.  A )  ->  -.  y R z ) )
7064, 69syl 17 . . . . . . . . . . . . 13  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( ( y  =  z  /\  y  e.  A )  ->  -.  y R z ) )
71 eleq1 2527 . . . . . . . . . . . . . . 15  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  (  _I  |`  A )  <->  <. y ,  z >.  e.  (  _I  |`  A ) ) )
72 vex 3059 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
7372brres 5129 . . . . . . . . . . . . . . . 16  |-  ( y (  _I  |`  A ) z  <->  ( y  _I  z  /\  y  e.  A ) )
74 df-br 4416 . . . . . . . . . . . . . . . 16  |-  ( y (  _I  |`  A ) z  <->  <. y ,  z
>.  e.  (  _I  |`  A ) )
7572ideq 5005 . . . . . . . . . . . . . . . . 17  |-  ( y  _I  z  <->  y  =  z )
7675anbi1i 706 . . . . . . . . . . . . . . . 16  |-  ( ( y  _I  z  /\  y  e.  A )  <->  ( y  =  z  /\  y  e.  A )
)
7773, 74, 763bitr3ri 284 . . . . . . . . . . . . . . 15  |-  ( ( y  =  z  /\  y  e.  A )  <->  <.
y ,  z >.  e.  (  _I  |`  A ) )
7871, 77syl6bbr 271 . . . . . . . . . . . . . 14  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  (  _I  |`  A )  <-> 
( y  =  z  /\  y  e.  A
) ) )
79 eleq1 2527 . . . . . . . . . . . . . . . 16  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  R  <->  <. y ,  z
>.  e.  R ) )
80 df-br 4416 . . . . . . . . . . . . . . . 16  |-  ( y R z  <->  <. y ,  z >.  e.  R
)
8179, 80syl6bbr 271 . . . . . . . . . . . . . . 15  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  R  <->  y R z ) )
8281notbid 300 . . . . . . . . . . . . . 14  |-  ( w  =  <. y ,  z
>.  ->  ( -.  w  e.  R  <->  -.  y R
z ) )
8378, 82imbi12d 326 . . . . . . . . . . . . 13  |-  ( w  =  <. y ,  z
>.  ->  ( ( w  e.  (  _I  |`  A )  ->  -.  w  e.  R )  <->  ( (
y  =  z  /\  y  e.  A )  ->  -.  y R z ) ) )
8470, 83syl5ibrcom 230 . . . . . . . . . . . 12  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( w  =  <. y ,  z >.  ->  (
w  e.  (  _I  |`  A )  ->  -.  w  e.  R )
) )
8584exlimdvv 1790 . . . . . . . . . . 11  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( E. y E. z  w  =  <. y ,  z >.  ->  (
w  e.  (  _I  |`  A )  ->  -.  w  e.  R )
) )
8685impd 437 . . . . . . . . . 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 33 . . . . . . . . 9  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( w  e.  (  _I  |`  A )  ->  -.  w  e.  R
) )
8887con2d 120 . . . . . . . 8  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( w  e.  R  ->  -.  w  e.  (  _I  |`  A )
) )
8988alrimiv 1783 . . . . . . 7  |-  ( A. x ( x  e.  A  ->  -.  x R x )  ->  A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) ) )
9054, 89impbii 192 . . . . . 6  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  <->  A. x ( x  e.  A  ->  -.  x R x ) )
91 df-ral 2753 . . . . . 6  |-  ( A. x  e.  A  -.  x R x  <->  A. x
( x  e.  A  ->  -.  x R x ) )
9290, 91bitr4i 260 . . . . 5  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  <->  A. x  e.  A  -.  x R x )
9335, 36, 923bitri 279 . . . 4  |-  ( ( R  i^i  (  _I  |`  A ) )  =  (/) 
<-> 
A. x  e.  A  -.  x R x )
94 ralcom 2962 . . . . . . 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 2878 . . . . . . . 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 2830 . . . . . . 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 257 . . . . . 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 2830 . . . . 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 4465 . . . . . . . . . . . 12  |-  ( x ( R  i^i  ( A  X.  A ) ) y  <->  ( x R y  /\  x ( A  X.  A ) y ) )
100 brin 4465 . . . . . . . . . . . 12  |-  ( y ( R  i^i  ( A  X.  A ) ) z  <->  ( y R z  /\  y ( A  X.  A ) z ) )
10199, 100anbi12i 708 . . . . . . . . . . 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 838 . . . . . . . . . . . 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 456 . . . . . . . . . . . 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 456 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  A  /\  y  e.  A )  <->  ( y  e.  A  /\  x  e.  A )
)
105104anbi1i 706 . . . . . . . . . . . . . 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 4883 . . . . . . . . . . . . . . 15  |-  ( x ( A  X.  A
) y  <->  ( x  e.  A  /\  y  e.  A ) )
107 brxp 4883 . . . . . . . . . . . . . . 15  |-  ( y ( A  X.  A
) z  <->  ( y  e.  A  /\  z  e.  A ) )
108106, 107anbi12i 708 . . . . . . . . . . . . . 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 842 . . . . . . . . . . . . . 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 285 . . . . . . . . . . . . 13  |-  ( ( x ( A  X.  A ) y  /\  y ( A  X.  A ) z )  <-> 
( y  e.  A  /\  ( x  e.  A  /\  z  e.  A
) ) )
111110anbi1i 706 . . . . . . . . . . . 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 279 . . . . . . . . . . 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 659 . . . . . . . . . . 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 279 . . . . . . . . . 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 1728 . . . . . . . . 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 5023 . . . . . . . . . 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 4416 . . . . . . . . . 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 259 . . . . . . . . 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 2754 . . . . . . . . . 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 2956 . . . . . . . . . 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 259 . . . . . . . . 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 284 . . . . . . . 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 4416 . . . . . . . 8  |-  ( x R z  <->  <. x ,  z >.  e.  R
)
124122, 123imbi12i 332 . . . . . . 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 1702 . . . . . 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 2777 . . . . . . 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 452 . . . . . . . 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 1702 . . . . . . 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 260 . . . . . 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 5351 . . . . . . 7  |-  Rel  (
( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  A
) ) )
131 ssrel 4941 . . . . . . 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 285 . . . . 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 258 . . . 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 708 . . 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 296 . 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 2718 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 189    /\ wa 375   A.wal 1452    = wceq 1454   E.wex 1673    e. wcel 1897    =/= wne 2632   A.wral 2748   E.wrex 2749   _Vcvv 3056    i^i cin 3414    C_ wss 3415   (/)c0 3742   <.cop 3985   class class class wbr 4415    _I cid 4762    Po wpo 4771    X. cxp 4850    |` cres 4854    o. ccom 4856   Rel wrel 4857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-opab 4475  df-id 4767  df-po 4773  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-res 4864
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator