| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-of |
|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) |
| 2 |
1
|
a1i |
|- ( F e. _V -> oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) ) |
| 3 |
|
dmeq |
|- ( f = F -> dom f = dom F ) |
| 4 |
|
dmeq |
|- ( g = (/) -> dom g = dom (/) ) |
| 5 |
3 4
|
ineqan12d |
|- ( ( f = F /\ g = (/) ) -> ( dom f i^i dom g ) = ( dom F i^i dom (/) ) ) |
| 6 |
5
|
mpteq1d |
|- ( ( f = F /\ g = (/) ) -> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) = ( x e. ( dom F i^i dom (/) ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) |
| 7 |
6
|
adantl |
|- ( ( F e. _V /\ ( f = F /\ g = (/) ) ) -> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) = ( x e. ( dom F i^i dom (/) ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) |
| 8 |
|
dm0 |
|- dom (/) = (/) |
| 9 |
8
|
ineq2i |
|- ( dom F i^i dom (/) ) = ( dom F i^i (/) ) |
| 10 |
|
in0 |
|- ( dom F i^i (/) ) = (/) |
| 11 |
9 10
|
eqtri |
|- ( dom F i^i dom (/) ) = (/) |
| 12 |
11
|
a1i |
|- ( ( F e. _V /\ ( f = F /\ g = (/) ) ) -> ( dom F i^i dom (/) ) = (/) ) |
| 13 |
12
|
mpteq1d |
|- ( ( F e. _V /\ ( f = F /\ g = (/) ) ) -> ( x e. ( dom F i^i dom (/) ) |-> ( ( f ` x ) R ( g ` x ) ) ) = ( x e. (/) |-> ( ( f ` x ) R ( g ` x ) ) ) ) |
| 14 |
|
mpt0 |
|- ( x e. (/) |-> ( ( f ` x ) R ( g ` x ) ) ) = (/) |
| 15 |
14
|
a1i |
|- ( ( F e. _V /\ ( f = F /\ g = (/) ) ) -> ( x e. (/) |-> ( ( f ` x ) R ( g ` x ) ) ) = (/) ) |
| 16 |
7 13 15
|
3eqtrd |
|- ( ( F e. _V /\ ( f = F /\ g = (/) ) ) -> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) = (/) ) |
| 17 |
|
id |
|- ( F e. _V -> F e. _V ) |
| 18 |
|
0ex |
|- (/) e. _V |
| 19 |
18
|
a1i |
|- ( F e. _V -> (/) e. _V ) |
| 20 |
2 16 17 19 19
|
ovmpod |
|- ( F e. _V -> ( F oF R (/) ) = (/) ) |
| 21 |
1
|
reldmmpo |
|- Rel dom oF R |
| 22 |
21
|
ovprc1 |
|- ( -. F e. _V -> ( F oF R (/) ) = (/) ) |
| 23 |
20 22
|
pm2.61i |
|- ( F oF R (/) ) = (/) |