Metamath Proof Explorer


Theorem opfv

Description: Value of a function producing ordered pairs. (Contributed by Thierry Arnoux, 3-Jan-2017)

Ref Expression
Assertion opfv
|- ( ( ( Fun F /\ ran F C_ ( _V X. _V ) ) /\ x e. dom F ) -> ( F ` x ) = <. ( ( 1st o. F ) ` x ) , ( ( 2nd o. F ) ` x ) >. )

Proof

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 ) >. )