Metamath Proof Explorer

Theorem funpartfv

Description: The function value of the functional part is identical to the original functional value. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion funpartfv 
|- ( Funpart F ` A ) = ( F ` A )

Proof

Step Hyp Ref Expression
1 df-funpart 
 |-  Funpart F = ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) )
2 1 fveq1i 
 |-  ( Funpart F ` A ) = ( ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) ` A )
3 fvres 
 |-  ( A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) -> ( ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) ` A ) = ( F ` A ) )
4 nfvres 
 |-  ( -. A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) -> ( ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) ` A ) = (/) )
5 funpartlem 
 |-  ( A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) <-> E. x ( F " { A } ) = { x } )
6 eusn 
 |-  ( E! x x e. ( F " { A } ) <-> E. x ( F " { A } ) = { x } )
7 5 6 bitr4i 
 |-  ( A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) <-> E! x x e. ( F " { A } ) )
8 elimasng 
 |-  ( ( A e. _V /\ x e. _V ) -> ( x e. ( F " { A } ) <-> <. A , x >. e. F ) )
9 8 elvd 
 |-  ( A e. _V -> ( x e. ( F " { A } ) <-> <. A , x >. e. F ) )
10 df-br 
 |-  ( A F x <-> <. A , x >. e. F )
11 9 10 bitr4di 
 |-  ( A e. _V -> ( x e. ( F " { A } ) <-> A F x ) )
12 11 eubidv 
 |-  ( A e. _V -> ( E! x x e. ( F " { A } ) <-> E! x A F x ) )
13 7 12 bitrid 
 |-  ( A e. _V -> ( A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) <-> E! x A F x ) )
14 13 notbid 
 |-  ( A e. _V -> ( -. A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) <-> -. E! x A F x ) )
15 tz6.12-2 
 |-  ( -. E! x A F x -> ( F ` A ) = (/) )
16 14 15 biimtrdi 
 |-  ( A e. _V -> ( -. A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) -> ( F ` A ) = (/) ) )
17 fvprc 
 |-  ( -. A e. _V -> ( F ` A ) = (/) )
18 17 a1d 
 |-  ( -. A e. _V -> ( -. A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) -> ( F ` A ) = (/) ) )
19 16 18 pm2.61i 
 |-  ( -. A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) -> ( F ` A ) = (/) )
20 4 19 eqtr4d 
 |-  ( -. A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) -> ( ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) ` A ) = ( F ` A ) )
21 3 20 pm2.61i 
 |-  ( ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) ` A ) = ( F ` A )
22 2 21 eqtri 
 |-  ( Funpart F ` A ) = ( F ` A )