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