Step |
Hyp |
Ref |
Expression |
1 |
|
elex |
|- ( F e. V -> F e. _V ) |
2 |
1
|
adantr |
|- ( ( F e. V /\ G e. W ) -> F e. _V ) |
3 |
|
elex |
|- ( G e. W -> G e. _V ) |
4 |
3
|
adantl |
|- ( ( F e. V /\ G e. W ) -> G e. _V ) |
5 |
|
funmpt |
|- Fun ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) |
6 |
5
|
a1i |
|- ( ( F e. V /\ G e. W ) -> Fun ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) |
7 |
|
dftpos4 |
|- tpos F = ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) |
8 |
|
tposexg |
|- ( F e. V -> tpos F e. _V ) |
9 |
8
|
adantr |
|- ( ( F e. V /\ G e. W ) -> tpos F e. _V ) |
10 |
7 9
|
eqeltrrid |
|- ( ( F e. V /\ G e. W ) -> ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) e. _V ) |
11 |
|
dftpos4 |
|- tpos G = ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) |
12 |
|
tposexg |
|- ( G e. W -> tpos G e. _V ) |
13 |
12
|
adantl |
|- ( ( F e. V /\ G e. W ) -> tpos G e. _V ) |
14 |
11 13
|
eqeltrrid |
|- ( ( F e. V /\ G e. W ) -> ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) e. _V ) |
15 |
|
ofco2 |
|- ( ( ( F e. _V /\ G e. _V ) /\ ( Fun ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) /\ ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) e. _V /\ ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) e. _V ) ) -> ( ( F oF R G ) o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) = ( ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) oF R ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) ) ) |
16 |
2 4 6 10 14 15
|
syl23anc |
|- ( ( F e. V /\ G e. W ) -> ( ( F oF R G ) o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) = ( ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) oF R ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) ) ) |
17 |
|
dftpos4 |
|- tpos ( F oF R G ) = ( ( F oF R G ) o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) |
18 |
7 11
|
oveq12i |
|- ( tpos F oF R tpos G ) = ( ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) oF R ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) ) |
19 |
16 17 18
|
3eqtr4g |
|- ( ( F e. V /\ G e. W ) -> tpos ( F oF R G ) = ( tpos F oF R tpos G ) ) |