Metamath Proof Explorer

Theorem fpr2g

Description: A function that maps a pair to a class is a pair of ordered pairs. (Contributed by Thierry Arnoux, 12-Jul-2020)

Ref Expression
Assertion fpr2g 
|- ( ( A e. V /\ B e. W ) -> ( F : { A , B } --> C <-> ( ( F ` A ) e. C /\ ( F ` B ) e. C /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( A e. V /\ B e. W ) /\ F : { A , B } --> C ) -> F : { A , B } --> C )
2 prid1g 
 |-  ( A e. V -> A e. { A , B } )
3 2 ad2antrr 
 |-  ( ( ( A e. V /\ B e. W ) /\ F : { A , B } --> C ) -> A e. { A , B } )
4 1 3 ffvelrnd 
 |-  ( ( ( A e. V /\ B e. W ) /\ F : { A , B } --> C ) -> ( F ` A ) e. C )
5 prid2g 
 |-  ( B e. W -> B e. { A , B } )
6 5 ad2antlr 
 |-  ( ( ( A e. V /\ B e. W ) /\ F : { A , B } --> C ) -> B e. { A , B } )
7 1 6 ffvelrnd 
 |-  ( ( ( A e. V /\ B e. W ) /\ F : { A , B } --> C ) -> ( F ` B ) e. C )
8 ffn 
 |-  ( F : { A , B } --> C -> F Fn { A , B } )
9 8 adantl 
 |-  ( ( ( A e. V /\ B e. W ) /\ F : { A , B } --> C ) -> F Fn { A , B } )
10 fnpr2g 
 |-  ( ( A e. V /\ B e. W ) -> ( F Fn { A , B } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) )
11 10 adantr 
 |-  ( ( ( A e. V /\ B e. W ) /\ F : { A , B } --> C ) -> ( F Fn { A , B } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) )
12 9 11 mpbid 
 |-  ( ( ( A e. V /\ B e. W ) /\ F : { A , B } --> C ) -> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } )
13 4 7 12 3jca 
 |-  ( ( ( A e. V /\ B e. W ) /\ F : { A , B } --> C ) -> ( ( F ` A ) e. C /\ ( F ` B ) e. C /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) )
14 10 biimpar 
 |-  ( ( ( A e. V /\ B e. W ) /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) -> F Fn { A , B } )
15 14 3ad2antr3 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( ( F ` A ) e. C /\ ( F ` B ) e. C /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) ) -> F Fn { A , B } )
16 simpr3 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( ( F ` A ) e. C /\ ( F ` B ) e. C /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) ) -> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } )
17 2 ad2antrr 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( ( F ` A ) e. C /\ ( F ` B ) e. C /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) ) -> A e. { A , B } )
18 simpr1 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( ( F ` A ) e. C /\ ( F ` B ) e. C /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) ) -> ( F ` A ) e. C )
19 17 18 opelxpd 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( ( F ` A ) e. C /\ ( F ` B ) e. C /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) ) -> <. A , ( F ` A ) >. e. ( { A , B } X. C ) )
20 5 ad2antlr 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( ( F ` A ) e. C /\ ( F ` B ) e. C /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) ) -> B e. { A , B } )
21 simpr2 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( ( F ` A ) e. C /\ ( F ` B ) e. C /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) ) -> ( F ` B ) e. C )
22 20 21 opelxpd 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( ( F ` A ) e. C /\ ( F ` B ) e. C /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) ) -> <. B , ( F ` B ) >. e. ( { A , B } X. C ) )
23 19 22 prssd 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( ( F ` A ) e. C /\ ( F ` B ) e. C /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) ) -> { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } C_ ( { A , B } X. C ) )
24 16 23 eqsstrd 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( ( F ` A ) e. C /\ ( F ` B ) e. C /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) ) -> F C_ ( { A , B } X. C ) )
25 dff2 
 |-  ( F : { A , B } --> C <-> ( F Fn { A , B } /\ F C_ ( { A , B } X. C ) ) )
26 15 24 25 sylanbrc 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( ( F ` A ) e. C /\ ( F ` B ) e. C /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) ) -> F : { A , B } --> C )
27 13 26 impbida 
 |-  ( ( A e. V /\ B e. W ) -> ( F : { A , B } --> C <-> ( ( F ` A ) e. C /\ ( F ` B ) e. C /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) ) )