Step |
Hyp |
Ref |
Expression |
1 |
|
simplr |
|- ( ( ( Fun F /\ ran F C_ ( _V X. _V ) ) /\ x e. dom F ) -> ran F C_ ( _V X. _V ) ) |
2 |
|
fvelrn |
|- ( ( Fun F /\ x e. dom F ) -> ( F ` x ) e. ran F ) |
3 |
2
|
adantlr |
|- ( ( ( Fun F /\ ran F C_ ( _V X. _V ) ) /\ x e. dom F ) -> ( F ` x ) e. ran F ) |
4 |
1 3
|
sseldd |
|- ( ( ( Fun F /\ ran F C_ ( _V X. _V ) ) /\ x e. dom F ) -> ( F ` x ) e. ( _V X. _V ) ) |
5 |
|
1st2ndb |
|- ( ( F ` x ) e. ( _V X. _V ) <-> ( F ` x ) = <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. ) |
6 |
4 5
|
sylib |
|- ( ( ( Fun F /\ ran F C_ ( _V X. _V ) ) /\ x e. dom F ) -> ( F ` x ) = <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. ) |
7 |
|
fvco |
|- ( ( Fun F /\ x e. dom F ) -> ( ( 1st o. F ) ` x ) = ( 1st ` ( F ` x ) ) ) |
8 |
|
fvco |
|- ( ( Fun F /\ x e. dom F ) -> ( ( 2nd o. F ) ` x ) = ( 2nd ` ( F ` x ) ) ) |
9 |
7 8
|
opeq12d |
|- ( ( Fun F /\ x e. dom F ) -> <. ( ( 1st o. F ) ` x ) , ( ( 2nd o. F ) ` x ) >. = <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. ) |
10 |
9
|
adantlr |
|- ( ( ( Fun F /\ ran F C_ ( _V X. _V ) ) /\ x e. dom F ) -> <. ( ( 1st o. F ) ` x ) , ( ( 2nd o. F ) ` x ) >. = <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. ) |
11 |
6 10
|
eqtr4d |
|- ( ( ( Fun F /\ ran F C_ ( _V X. _V ) ) /\ x e. dom F ) -> ( F ` x ) = <. ( ( 1st o. F ) ` x ) , ( ( 2nd o. F ) ` x ) >. ) |