Metamath Proof Explorer

Theorem fgraphopab

Description: Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Assertion fgraphopab 
|- ( F : A --> B -> F = { <. a , b >. | ( ( a e. A /\ b e. B ) /\ ( F ` a ) = b ) } )

Proof

Step Hyp Ref Expression
1 fssxp 
 |-  ( F : A --> B -> F C_ ( A X. B ) )
2 dfss2 
 |-  ( F C_ ( A X. B ) <-> ( F i^i ( A X. B ) ) = F )
3 1 2 sylib 
 |-  ( F : A --> B -> ( F i^i ( A X. B ) ) = F )
4 ffn 
 |-  ( F : A --> B -> F Fn A )
5 dffn5 
 |-  ( F Fn A <-> F = ( a e. A |-> ( F ` a ) ) )
6 4 5 sylib 
 |-  ( F : A --> B -> F = ( a e. A |-> ( F ` a ) ) )
7 6 ineq1d 
 |-  ( F : A --> B -> ( F i^i ( A X. B ) ) = ( ( a e. A |-> ( F ` a ) ) i^i ( A X. B ) ) )
8 3 7 eqtr3d 
 |-  ( F : A --> B -> F = ( ( a e. A |-> ( F ` a ) ) i^i ( A X. B ) ) )
9 df-mpt 
 |-  ( a e. A |-> ( F ` a ) ) = { <. a , b >. | ( a e. A /\ b = ( F ` a ) ) }
10 df-xp 
 |-  ( A X. B ) = { <. a , b >. | ( a e. A /\ b e. B ) }
11 9 10 ineq12i 
 |-  ( ( a e. A |-> ( F ` a ) ) i^i ( A X. B ) ) = ( { <. a , b >. | ( a e. A /\ b = ( F ` a ) ) } i^i { <. a , b >. | ( a e. A /\ b e. B ) } )
12 inopab 
 |-  ( { <. a , b >. | ( a e. A /\ b = ( F ` a ) ) } i^i { <. a , b >. | ( a e. A /\ b e. B ) } ) = { <. a , b >. | ( ( a e. A /\ b = ( F ` a ) ) /\ ( a e. A /\ b e. B ) ) }
13 anandi 
 |-  ( ( a e. A /\ ( b = ( F ` a ) /\ b e. B ) ) <-> ( ( a e. A /\ b = ( F ` a ) ) /\ ( a e. A /\ b e. B ) ) )
14 ancom 
 |-  ( ( b = ( F ` a ) /\ b e. B ) <-> ( b e. B /\ b = ( F ` a ) ) )
15 14 anbi2i 
 |-  ( ( a e. A /\ ( b = ( F ` a ) /\ b e. B ) ) <-> ( a e. A /\ ( b e. B /\ b = ( F ` a ) ) ) )
16 anass 
 |-  ( ( ( a e. A /\ b e. B ) /\ b = ( F ` a ) ) <-> ( a e. A /\ ( b e. B /\ b = ( F ` a ) ) ) )
17 eqcom 
 |-  ( b = ( F ` a ) <-> ( F ` a ) = b )
18 17 anbi2i 
 |-  ( ( ( a e. A /\ b e. B ) /\ b = ( F ` a ) ) <-> ( ( a e. A /\ b e. B ) /\ ( F ` a ) = b ) )
19 15 16 18 3bitr2i 
 |-  ( ( a e. A /\ ( b = ( F ` a ) /\ b e. B ) ) <-> ( ( a e. A /\ b e. B ) /\ ( F ` a ) = b ) )
20 13 19 bitr3i 
 |-  ( ( ( a e. A /\ b = ( F ` a ) ) /\ ( a e. A /\ b e. B ) ) <-> ( ( a e. A /\ b e. B ) /\ ( F ` a ) = b ) )
21 20 opabbii 
 |-  { <. a , b >. | ( ( a e. A /\ b = ( F ` a ) ) /\ ( a e. A /\ b e. B ) ) } = { <. a , b >. | ( ( a e. A /\ b e. B ) /\ ( F ` a ) = b ) }
22 11 12 21 3eqtri 
 |-  ( ( a e. A |-> ( F ` a ) ) i^i ( A X. B ) ) = { <. a , b >. | ( ( a e. A /\ b e. B ) /\ ( F ` a ) = b ) }
23 8 22 eqtrdi 
 |-  ( F : A --> B -> F = { <. a , b >. | ( ( a e. A /\ b e. B ) /\ ( F ` a ) = b ) } )