| Step |
Hyp |
Ref |
Expression |
| 1 |
|
oppcuprcl2.x |
|- ( ph -> X ( <. F , G >. ( O UP P ) W ) M ) |
| 2 |
|
uptpos.h |
|- ( ph -> tpos G = H ) |
| 3 |
2
|
tposeqd |
|- ( ph -> tpos tpos G = tpos H ) |
| 4 |
|
eqid |
|- ( Base ` O ) = ( Base ` O ) |
| 5 |
1
|
uprcl2 |
|- ( ph -> F ( O Func P ) G ) |
| 6 |
4 5
|
funcfn2 |
|- ( ph -> G Fn ( ( Base ` O ) X. ( Base ` O ) ) ) |
| 7 |
|
fnrel |
|- ( G Fn ( ( Base ` O ) X. ( Base ` O ) ) -> Rel G ) |
| 8 |
6 7
|
syl |
|- ( ph -> Rel G ) |
| 9 |
|
relxp |
|- Rel ( ( Base ` O ) X. ( Base ` O ) ) |
| 10 |
6
|
fndmd |
|- ( ph -> dom G = ( ( Base ` O ) X. ( Base ` O ) ) ) |
| 11 |
10
|
releqd |
|- ( ph -> ( Rel dom G <-> Rel ( ( Base ` O ) X. ( Base ` O ) ) ) ) |
| 12 |
9 11
|
mpbiri |
|- ( ph -> Rel dom G ) |
| 13 |
|
tpostpos2 |
|- ( ( Rel G /\ Rel dom G ) -> tpos tpos G = G ) |
| 14 |
8 12 13
|
syl2anc |
|- ( ph -> tpos tpos G = G ) |
| 15 |
3 14
|
eqtr3d |
|- ( ph -> tpos H = G ) |