| Step |
Hyp |
Ref |
Expression |
| 1 |
|
simpr |
|- ( ( f = F /\ g = G ) -> g = G ) |
| 2 |
1
|
releqd |
|- ( ( f = F /\ g = G ) -> ( Rel g <-> Rel G ) ) |
| 3 |
1
|
dmeqd |
|- ( ( f = F /\ g = G ) -> dom g = dom G ) |
| 4 |
3
|
releqd |
|- ( ( f = F /\ g = G ) -> ( Rel dom g <-> Rel dom G ) ) |
| 5 |
2 4
|
anbi12d |
|- ( ( f = F /\ g = G ) -> ( ( Rel g /\ Rel dom g ) <-> ( Rel G /\ Rel dom G ) ) ) |
| 6 |
|
simpl |
|- ( ( f = F /\ g = G ) -> f = F ) |
| 7 |
1
|
tposeqd |
|- ( ( f = F /\ g = G ) -> tpos g = tpos G ) |
| 8 |
6 7
|
opeq12d |
|- ( ( f = F /\ g = G ) -> <. f , tpos g >. = <. F , tpos G >. ) |
| 9 |
5 8
|
ifbieq1d |
|- ( ( f = F /\ g = G ) -> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) |
| 10 |
|
df-oppf |
|- oppFunc = ( f e. _V , g e. _V |-> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) ) |
| 11 |
|
opex |
|- <. F , tpos G >. e. _V |
| 12 |
|
0ex |
|- (/) e. _V |
| 13 |
11 12
|
ifex |
|- if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) e. _V |
| 14 |
9 10 13
|
ovmpoa |
|- ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) |