Step |
Hyp |
Ref |
Expression |
1 |
|
tposmpo.1 |
|- F = ( x e. A , y e. B |-> C ) |
2 |
|
df-mpo |
|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } |
3 |
|
ancom |
|- ( ( x e. A /\ y e. B ) <-> ( y e. B /\ x e. A ) ) |
4 |
3
|
anbi1i |
|- ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( y e. B /\ x e. A ) /\ z = C ) ) |
5 |
4
|
oprabbii |
|- { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } = { <. <. x , y >. , z >. | ( ( y e. B /\ x e. A ) /\ z = C ) } |
6 |
1 2 5
|
3eqtri |
|- F = { <. <. x , y >. , z >. | ( ( y e. B /\ x e. A ) /\ z = C ) } |
7 |
6
|
tposoprab |
|- tpos F = { <. <. y , x >. , z >. | ( ( y e. B /\ x e. A ) /\ z = C ) } |
8 |
|
df-mpo |
|- ( y e. B , x e. A |-> C ) = { <. <. y , x >. , z >. | ( ( y e. B /\ x e. A ) /\ z = C ) } |
9 |
7 8
|
eqtr4i |
|- tpos F = ( y e. B , x e. A |-> C ) |