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

Theorem dfpo2 30346
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 4732 . . . 4  |-  R  Po  (/)
2 res0 5071 . . . . . . 7  |-  (  _I  |`  (/) )  =  (/)
32ineq2i 3604 . . . . . 6  |-  ( R  i^i  (  _I  |`  (/) ) )  =  ( R  i^i  (/) )
4 in0 3733 . . . . . 6  |-  ( R  i^i  (/) )  =  (/)
53, 4eqtri 2450 . . . . 5  |-  ( R  i^i  (  _I  |`  (/) ) )  =  (/)
6 xp0 5217 . . . . . . . . . 10  |-  ( A  X.  (/) )  =  (/)
76ineq2i 3604 . . . . . . . . 9  |-  ( R  i^i  ( A  X.  (/) ) )  =  ( R  i^i  (/) )
87, 4eqtri 2450 . . . . . . . 8  |-  ( R  i^i  ( A  X.  (/) ) )  =  (/)
98coeq2i 4957 . . . . . . 7  |-  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  =  ( ( R  i^i  ( A  X.  A ) )  o.  (/) )
10 co02 5311 . . . . . . 7  |-  ( ( R  i^i  ( A  X.  A ) )  o.  (/) )  =  (/)
119, 10eqtri 2450 . . . . . 6  |-  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  =  (/)
12 0ss 3736 . . . . . 6  |-  (/)  C_  R
1311, 12eqsstri 3437 . . . . 5  |-  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  C_  R
145, 13pm3.2i 456 . . . 4  |-  ( ( R  i^i  (  _I  |`  (/) ) )  =  (/)  /\  ( ( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) ) 
C_  R )
151, 142th 242 . . 3  |-  ( R  Po  (/)  <->  ( ( R  i^i  (  _I  |`  (/) ) )  =  (/)  /\  (
( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  (/) ) ) )  C_  R )
)
16 poeq2 4721 . . . 4  |-  ( A  =  (/)  ->  ( R  Po  A  <->  R  Po  (/) ) )
17 reseq2 5062 . . . . . . 7  |-  ( A  =  (/)  ->  (  _I  |`  A )  =  (  _I  |`  (/) ) )
1817ineq2d 3607 . . . . . 6  |-  ( A  =  (/)  ->  ( R  i^i  (  _I  |`  A ) )  =  ( R  i^i  (  _I  |`  (/) ) ) )
1918eqeq1d 2430 . . . . 5  |-  ( A  =  (/)  ->  ( ( R  i^i  (  _I  |`  A ) )  =  (/) 
<->  ( R  i^i  (  _I  |`  (/) ) )  =  (/) ) )
20 xpeq2 4811 . . . . . . . 8  |-  ( A  =  (/)  ->  ( A  X.  A )  =  ( A  X.  (/) ) )
2120ineq2d 3607 . . . . . . 7  |-  ( A  =  (/)  ->  ( R  i^i  ( A  X.  A ) )  =  ( R  i^i  ( A  X.  (/) ) ) )
2221coeq2d 4959 . . . . . 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 3434 . . . . 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 715 . . . 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 322 . . 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 236 . 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 3837 . . . . . . 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 2804 . . . . . 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 3837 . . . . . 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 256 . . . . 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 2804 . . . 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 2894 . . . 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 264 . . 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 4717 . . 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 3778 . . . . 5  |-  ( ( R  i^i  (  _I  |`  A ) )  =  (/) 
<-> 
A. w  e.  R  -.  w  e.  (  _I  |`  A ) )
36 df-ral 2719 . . . . 5  |-  ( A. w  e.  R  -.  w  e.  (  _I  |`  A )  <->  A. w
( w  e.  R  ->  -.  w  e.  (  _I  |`  A )
) )
37 opex 4628 . . . . . . . . . 10  |-  <. x ,  x >.  e.  _V
38 eleq1 2494 . . . . . . . . . . . 12  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  R  <->  <. x ,  x >.  e.  R ) )
39 df-br 4367 . . . . . . . . . . . 12  |-  ( x R x  <->  <. x ,  x >.  e.  R
)
4038, 39syl6bbr 266 . . . . . . . . . . 11  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  R  <->  x R x ) )
41 eleq1 2494 . . . . . . . . . . . . 13  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  (  _I  |`  A )  <->  <. x ,  x >.  e.  (  _I  |`  A ) ) )
42 vex 3025 . . . . . . . . . . . . . . . 16  |-  x  e. 
_V
43 ididg 4950 . . . . . . . . . . . . . . . 16  |-  ( x  e.  _V  ->  x  _I  x )
4442, 43ax-mp 5 . . . . . . . . . . . . . . 15  |-  x  _I  x
4542brres 5073 . . . . . . . . . . . . . . 15  |-  ( x (  _I  |`  A ) x  <->  ( x  _I  x  /\  x  e.  A ) )
4644, 45mpbiran 926 . . . . . . . . . . . . . 14  |-  ( x (  _I  |`  A ) x  <->  x  e.  A
)
47 df-br 4367 . . . . . . . . . . . . . 14  |-  ( x (  _I  |`  A ) x  <->  <. x ,  x >.  e.  (  _I  |`  A ) )
4846, 47bitr3i 254 . . . . . . . . . . . . 13  |-  ( x  e.  A  <->  <. x ,  x >.  e.  (  _I  |`  A ) )
4941, 48syl6bbr 266 . . . . . . . . . . . 12  |-  ( w  =  <. x ,  x >.  ->  ( w  e.  (  _I  |`  A )  <-> 
x  e.  A ) )
5049notbid 295 . . . . . . . . . . 11  |-  ( w  =  <. x ,  x >.  ->  ( -.  w  e.  (  _I  |`  A )  <->  -.  x  e.  A
) )
5140, 50imbi12d 321 . . . . . . . . . 10  |-  ( w  =  <. x ,  x >.  ->  ( ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  <->  ( x R x  ->  -.  x  e.  A ) ) )
5237, 51spcv 3115 . . . . . . . . 9  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  ->  ( x R x  ->  -.  x  e.  A ) )
5352con2d 118 . . . . . . . 8  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  ->  ( x  e.  A  ->  -.  x R x ) )
5453alrimiv 1767 . . . . . . 7  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  ->  A. x
( x  e.  A  ->  -.  x R x ) )
55 relres 5094 . . . . . . . . . . . 12  |-  Rel  (  _I  |`  A )
56 elrel 4899 . . . . . . . . . . . 12  |-  ( ( Rel  (  _I  |`  A )  /\  w  e.  (  _I  |`  A )
)  ->  E. y E. z  w  =  <. y ,  z >.
)
5755, 56mpan 674 . . . . . . . . . . 11  |-  ( w  e.  (  _I  |`  A )  ->  E. y E. z  w  =  <. y ,  z >. )
5857ancri 554 . . . . . . . . . 10  |-  ( w  e.  (  _I  |`  A )  ->  ( E. y E. z  w  =  <. y ,  z >.  /\  w  e.  (  _I  |`  A ) ) )
59 eleq1 2494 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )
60 breq12 4371 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  =  y  /\  x  =  y )  ->  ( x R x  <-> 
y R y ) )
6160anidms 649 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
x R x  <->  y R
y ) )
6261notbid 295 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  ( -.  x R x  <->  -.  y R y ) )
6359, 62imbi12d 321 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
( x  e.  A  ->  -.  x R x )  <->  ( y  e.  A  ->  -.  y R y ) ) )
6463spv 2076 . . . . . . . . . . . . . 14  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( y  e.  A  ->  -.  y R y ) )
65 breq2 4370 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  z  ->  (
y R y  <->  y R
z ) )
6665notbid 295 . . . . . . . . . . . . . . . . 17  |-  ( y  =  z  ->  ( -.  y R y  <->  -.  y R z ) )
6766imbi2d 317 . . . . . . . . . . . . . . . 16  |-  ( y  =  z  ->  (
( y  e.  A  ->  -.  y R y )  <->  ( y  e.  A  ->  -.  y R z ) ) )
6867biimpcd 227 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  A  ->  -.  y R y )  ->  ( y  =  z  ->  ( y  e.  A  ->  -.  y R z ) ) )
6968impd 432 . . . . . . . . . . . . . 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 2494 . . . . . . . . . . . . . . 15  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  (  _I  |`  A )  <->  <. y ,  z >.  e.  (  _I  |`  A ) ) )
72 vex 3025 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
7372brres 5073 . . . . . . . . . . . . . . . 16  |-  ( y (  _I  |`  A ) z  <->  ( y  _I  z  /\  y  e.  A ) )
74 df-br 4367 . . . . . . . . . . . . . . . 16  |-  ( y (  _I  |`  A ) z  <->  <. y ,  z
>.  e.  (  _I  |`  A ) )
7572ideq 4949 . . . . . . . . . . . . . . . . 17  |-  ( y  _I  z  <->  y  =  z )
7675anbi1i 699 . . . . . . . . . . . . . . . 16  |-  ( ( y  _I  z  /\  y  e.  A )  <->  ( y  =  z  /\  y  e.  A )
)
7773, 74, 763bitr3ri 279 . . . . . . . . . . . . . . 15  |-  ( ( y  =  z  /\  y  e.  A )  <->  <.
y ,  z >.  e.  (  _I  |`  A ) )
7871, 77syl6bbr 266 . . . . . . . . . . . . . 14  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  (  _I  |`  A )  <-> 
( y  =  z  /\  y  e.  A
) ) )
79 eleq1 2494 . . . . . . . . . . . . . . . 16  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  R  <->  <. y ,  z
>.  e.  R ) )
80 df-br 4367 . . . . . . . . . . . . . . . 16  |-  ( y R z  <->  <. y ,  z >.  e.  R
)
8179, 80syl6bbr 266 . . . . . . . . . . . . . . 15  |-  ( w  =  <. y ,  z
>.  ->  ( w  e.  R  <->  y R z ) )
8281notbid 295 . . . . . . . . . . . . . 14  |-  ( w  =  <. y ,  z
>.  ->  ( -.  w  e.  R  <->  -.  y R
z ) )
8378, 82imbi12d 321 . . . . . . . . . . . . 13  |-  ( w  =  <. y ,  z
>.  ->  ( ( w  e.  (  _I  |`  A )  ->  -.  w  e.  R )  <->  ( (
y  =  z  /\  y  e.  A )  ->  -.  y R z ) ) )
8470, 83syl5ibrcom 225 . . . . . . . . . . . 12  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( w  =  <. y ,  z >.  ->  (
w  e.  (  _I  |`  A )  ->  -.  w  e.  R )
) )
8584exlimdvv 1773 . . . . . . . . . . 11  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( E. y E. z  w  =  <. y ,  z >.  ->  (
w  e.  (  _I  |`  A )  ->  -.  w  e.  R )
) )
8685impd 432 . . . . . . . . . 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 118 . . . . . . . 8  |-  ( A. x ( x  e.  A  ->  -.  x R x )  -> 
( w  e.  R  ->  -.  w  e.  (  _I  |`  A )
) )
8988alrimiv 1767 . . . . . . 7  |-  ( A. x ( x  e.  A  ->  -.  x R x )  ->  A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) ) )
9054, 89impbii 190 . . . . . 6  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  <->  A. x ( x  e.  A  ->  -.  x R x ) )
91 df-ral 2719 . . . . . 6  |-  ( A. x  e.  A  -.  x R x  <->  A. x
( x  e.  A  ->  -.  x R x ) )
9290, 91bitr4i 255 . . . . 5  |-  ( A. w ( w  e.  R  ->  -.  w  e.  (  _I  |`  A ) )  <->  A. x  e.  A  -.  x R x )
9335, 36, 923bitri 274 . . . 4  |-  ( ( R  i^i  (  _I  |`  A ) )  =  (/) 
<-> 
A. x  e.  A  -.  x R x )
94 ralcom 2928 . . . . . . 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 2844 . . . . . . . 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 2796 . . . . . . 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 252 . . . . . 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 2796 . . . . 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 4416 . . . . . . . . . . . 12  |-  ( x ( R  i^i  ( A  X.  A ) ) y  <->  ( x R y  /\  x ( A  X.  A ) y ) )
100 brin 4416 . . . . . . . . . . . 12  |-  ( y ( R  i^i  ( A  X.  A ) ) z  <->  ( y R z  /\  y ( A  X.  A ) z ) )
10199, 100anbi12i 701 . . . . . . . . . . 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 831 . . . . . . . . . . . 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 451 . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  A  /\  y  e.  A )  <->  ( y  e.  A  /\  x  e.  A )
)
105104anbi1i 699 . . . . . . . . . . . . . 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 4827 . . . . . . . . . . . . . . 15  |-  ( x ( A  X.  A
) y  <->  ( x  e.  A  /\  y  e.  A ) )
107 brxp 4827 . . . . . . . . . . . . . . 15  |-  ( y ( A  X.  A
) z  <->  ( y  e.  A  /\  z  e.  A ) )
108106, 107anbi12i 701 . . . . . . . . . . . . . 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 835 . . . . . . . . . . . . . 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 280 . . . . . . . . . . . . 13  |-  ( ( x ( A  X.  A ) y  /\  y ( A  X.  A ) z )  <-> 
( y  e.  A  /\  ( x  e.  A  /\  z  e.  A
) ) )
111110anbi1i 699 . . . . . . . . . . . 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 274 . . . . . . . . . . 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 653 . . . . . . . . . . 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 274 . . . . . . . . . 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 1712 . . . . . . . . 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 4967 . . . . . . . . . 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 4367 . . . . . . . . . 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 254 . . . . . . . . 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 2720 . . . . . . . . . 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 2922 . . . . . . . . . 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 254 . . . . . . . . 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 279 . . . . . . . 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 4367 . . . . . . . 8  |-  ( x R z  <->  <. x ,  z >.  e.  R
)
124122, 123imbi12i 327 . . . . . . 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 1686 . . . . . 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 2743 . . . . . . 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 447 . . . . . . . 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 1686 . . . . . . 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 255 . . . . . 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 5295 . . . . . . 7  |-  Rel  (
( R  i^i  ( A  X.  A ) )  o.  ( R  i^i  ( A  X.  A
) ) )
131 ssrel 4885 . . . . . . 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 280 . . . . 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 253 . . . 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 701 . . 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 291 . 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 2684 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 187    /\ wa 370   A.wal 1435    = wceq 1437   E.wex 1657    e. wcel 1872    =/= wne 2599   A.wral 2714   E.wrex 2715   _Vcvv 3022    i^i cin 3378    C_ wss 3379   (/)c0 3704   <.cop 3947   class class class wbr 4366    _I cid 4706    Po wpo 4715    X. cxp 4794    |` cres 4798    o. ccom 4800   Rel wrel 4801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-br 4367  df-opab 4426  df-id 4711  df-po 4717  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-res 4808
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator