This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dffn5

Description: Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013) (Proof shortened by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion dffn5 
|- ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )

Proof

Step Hyp Ref Expression
1 fnrel 
 |-  ( F Fn A -> Rel F )
2 dfrel4v 
 |-  ( Rel F <-> F = { <. x , y >. | x F y } )
3 1 2 sylib 
 |-  ( F Fn A -> F = { <. x , y >. | x F y } )
4 fnbr 
 |-  ( ( F Fn A /\ x F y ) -> x e. A )
5 4 ex 
 |-  ( F Fn A -> ( x F y -> x e. A ) )
6 5 pm4.71rd 
 |-  ( F Fn A -> ( x F y <-> ( x e. A /\ x F y ) ) )
7 eqcom 
 |-  ( y = ( F ` x ) <-> ( F ` x ) = y )
8 fnbrfvb 
 |-  ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = y <-> x F y ) )
9 7 8 bitrid 
 |-  ( ( F Fn A /\ x e. A ) -> ( y = ( F ` x ) <-> x F y ) )
10 9 pm5.32da 
 |-  ( F Fn A -> ( ( x e. A /\ y = ( F ` x ) ) <-> ( x e. A /\ x F y ) ) )
11 6 10 bitr4d 
 |-  ( F Fn A -> ( x F y <-> ( x e. A /\ y = ( F ` x ) ) ) )
12 11 opabbidv 
 |-  ( F Fn A -> { <. x , y >. | x F y } = { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) } )
13 3 12 eqtrd 
 |-  ( F Fn A -> F = { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) } )
14 df-mpt 
 |-  ( x e. A |-> ( F ` x ) ) = { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) }
15 13 14 eqtr4di 
 |-  ( F Fn A -> F = ( x e. A |-> ( F ` x ) ) )
16 fvex 
 |-  ( F ` x ) e. _V
17 eqid 
 |-  ( x e. A |-> ( F ` x ) ) = ( x e. A |-> ( F ` x ) )
18 16 17 fnmpti 
 |-  ( x e. A |-> ( F ` x ) ) Fn A
19 fneq1 
 |-  ( F = ( x e. A |-> ( F ` x ) ) -> ( F Fn A <-> ( x e. A |-> ( F ` x ) ) Fn A ) )
20 18 19 mpbiri 
 |-  ( F = ( x e. A |-> ( F ` x ) ) -> F Fn A )
21 15 20 impbii 
 |-  ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )