Step |
Hyp |
Ref |
Expression |
1 |
|
xrnrel |
|- Rel ( R |X. S ) |
2 |
|
dfrel4v |
|- ( Rel ( R |X. S ) <-> ( R |X. S ) = { <. u , z >. | u ( R |X. S ) z } ) |
3 |
1 2
|
mpbi |
|- ( R |X. S ) = { <. u , z >. | u ( R |X. S ) z } |
4 |
|
breq2 |
|- ( z = <. x , y >. -> ( u ( R |X. S ) z <-> u ( R |X. S ) <. x , y >. ) ) |
5 |
|
brxrn2 |
|- ( u e. _V -> ( u ( R |X. S ) z <-> E. x E. y ( z = <. x , y >. /\ u R x /\ u S y ) ) ) |
6 |
5
|
elv |
|- ( u ( R |X. S ) z <-> E. x E. y ( z = <. x , y >. /\ u R x /\ u S y ) ) |
7 |
|
brxrn |
|- ( ( u e. _V /\ x e. _V /\ y e. _V ) -> ( u ( R |X. S ) <. x , y >. <-> ( u R x /\ u S y ) ) ) |
8 |
7
|
el3v |
|- ( u ( R |X. S ) <. x , y >. <-> ( u R x /\ u S y ) ) |
9 |
8
|
anbi2i |
|- ( ( z = <. x , y >. /\ u ( R |X. S ) <. x , y >. ) <-> ( z = <. x , y >. /\ ( u R x /\ u S y ) ) ) |
10 |
|
3anass |
|- ( ( z = <. x , y >. /\ u R x /\ u S y ) <-> ( z = <. x , y >. /\ ( u R x /\ u S y ) ) ) |
11 |
9 10
|
bitr4i |
|- ( ( z = <. x , y >. /\ u ( R |X. S ) <. x , y >. ) <-> ( z = <. x , y >. /\ u R x /\ u S y ) ) |
12 |
11
|
2exbii |
|- ( E. x E. y ( z = <. x , y >. /\ u ( R |X. S ) <. x , y >. ) <-> E. x E. y ( z = <. x , y >. /\ u R x /\ u S y ) ) |
13 |
4
|
copsex2gb |
|- ( E. x E. y ( z = <. x , y >. /\ u ( R |X. S ) <. x , y >. ) <-> ( z e. ( _V X. _V ) /\ u ( R |X. S ) z ) ) |
14 |
6 12 13
|
3bitr2i |
|- ( u ( R |X. S ) z <-> ( z e. ( _V X. _V ) /\ u ( R |X. S ) z ) ) |
15 |
14
|
simplbi |
|- ( u ( R |X. S ) z -> z e. ( _V X. _V ) ) |
16 |
4 15
|
cnvoprab |
|- `' { <. <. x , y >. , u >. | u ( R |X. S ) <. x , y >. } = { <. u , z >. | u ( R |X. S ) z } |
17 |
8
|
oprabbii |
|- { <. <. x , y >. , u >. | u ( R |X. S ) <. x , y >. } = { <. <. x , y >. , u >. | ( u R x /\ u S y ) } |
18 |
17
|
cnveqi |
|- `' { <. <. x , y >. , u >. | u ( R |X. S ) <. x , y >. } = `' { <. <. x , y >. , u >. | ( u R x /\ u S y ) } |
19 |
3 16 18
|
3eqtr2i |
|- ( R |X. S ) = `' { <. <. x , y >. , u >. | ( u R x /\ u S y ) } |