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 A b B F a = b

Proof

Step Hyp Ref Expression
1 fssxp F : A B F A × B
2 df-ss F A × B F A × B = F
3 1 2 sylib F : A B F A × B = F
4 ffn F : A B F Fn A
5 dffn5 F Fn A F = a A F a
6 4 5 sylib F : A B F = a A F a
7 6 ineq1d F : A B F A × B = a A F a A × B
8 3 7 eqtr3d F : A B F = a A F a A × B
9 df-mpt a A F a = a b | a A b = F a
10 df-xp A × B = a b | a A b B
11 9 10 ineq12i a A F a A × B = a b | a A b = F a a b | a A b B
12 inopab a b | a A b = F a a b | a A b B = a b | a A b = F a a A b B
13 anandi a A b = F a b B a A b = F a a A b B
14 ancom b = F a b B b B b = F a
15 14 anbi2i a A b = F a b B a A b B b = F a
16 anass a A b B b = F a a A b B b = F a
17 eqcom b = F a F a = b
18 17 anbi2i a A b B b = F a a A b B F a = b
19 15 16 18 3bitr2i a A b = F a b B a A b B F a = b
20 13 19 bitr3i a A b = F a a A b B a A b B F a = b
21 20 opabbii a b | a A b = F a a A b B = a b | a A b B F a = b
22 11 12 21 3eqtri a A F a A × B = a b | a A b B F a = b
23 8 22 eqtrdi F : A B F = a b | a A b B F a = b