Metamath Proof Explorer

Theorem fullfunfv

Description: The function value of the full function of F agrees with F . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion fullfunfv 
|- ( FullFun F ` A ) = ( F ` A )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = A -> ( FullFun F ` x ) = ( FullFun F ` A ) )
2 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
3 1 2 eqeq12d 
 |-  ( x = A -> ( ( FullFun F ` x ) = ( F ` x ) <-> ( FullFun F ` A ) = ( F ` A ) ) )
4 df-fullfun 
 |-  FullFun F = ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) )
5 4 fveq1i 
 |-  ( FullFun F ` x ) = ( ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) ` x )
6 disjdif 
 |-  ( dom Funpart F i^i ( _V \ dom Funpart F ) ) = (/)
7 funpartfun 
 |-  Fun Funpart F
8 funfn 
 |-  ( Fun Funpart F <-> Funpart F Fn dom Funpart F )
9 7 8 mpbi 
 |-  Funpart F Fn dom Funpart F
10 0ex 
 |-  (/) e. _V
11 10 fconst 
 |-  ( ( _V \ dom Funpart F ) X. { (/) } ) : ( _V \ dom Funpart F ) --> { (/) }
12 ffn 
 |-  ( ( ( _V \ dom Funpart F ) X. { (/) } ) : ( _V \ dom Funpart F ) --> { (/) } -> ( ( _V \ dom Funpart F ) X. { (/) } ) Fn ( _V \ dom Funpart F ) )
13 11 12 ax-mp 
 |-  ( ( _V \ dom Funpart F ) X. { (/) } ) Fn ( _V \ dom Funpart F )
14 fvun1 
 |-  ( ( Funpart F Fn dom Funpart F /\ ( ( _V \ dom Funpart F ) X. { (/) } ) Fn ( _V \ dom Funpart F ) /\ ( ( dom Funpart F i^i ( _V \ dom Funpart F ) ) = (/) /\ x e. dom Funpart F ) ) -> ( ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) ` x ) = ( Funpart F ` x ) )
15 9 13 14 mp3an12 
 |-  ( ( ( dom Funpart F i^i ( _V \ dom Funpart F ) ) = (/) /\ x e. dom Funpart F ) -> ( ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) ` x ) = ( Funpart F ` x ) )
16 6 15 mpan 
 |-  ( x e. dom Funpart F -> ( ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) ` x ) = ( Funpart F ` x ) )
17 vex 
 |-  x e. _V
18 eldif 
 |-  ( x e. ( _V \ dom Funpart F ) <-> ( x e. _V /\ -. x e. dom Funpart F ) )
19 17 18 mpbiran 
 |-  ( x e. ( _V \ dom Funpart F ) <-> -. x e. dom Funpart F )
20 fvun2 
 |-  ( ( Funpart F Fn dom Funpart F /\ ( ( _V \ dom Funpart F ) X. { (/) } ) Fn ( _V \ dom Funpart F ) /\ ( ( dom Funpart F i^i ( _V \ dom Funpart F ) ) = (/) /\ x e. ( _V \ dom Funpart F ) ) ) -> ( ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) ` x ) = ( ( ( _V \ dom Funpart F ) X. { (/) } ) ` x ) )
21 9 13 20 mp3an12 
 |-  ( ( ( dom Funpart F i^i ( _V \ dom Funpart F ) ) = (/) /\ x e. ( _V \ dom Funpart F ) ) -> ( ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) ` x ) = ( ( ( _V \ dom Funpart F ) X. { (/) } ) ` x ) )
22 6 21 mpan 
 |-  ( x e. ( _V \ dom Funpart F ) -> ( ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) ` x ) = ( ( ( _V \ dom Funpart F ) X. { (/) } ) ` x ) )
23 10 fvconst2 
 |-  ( x e. ( _V \ dom Funpart F ) -> ( ( ( _V \ dom Funpart F ) X. { (/) } ) ` x ) = (/) )
24 22 23 eqtrd 
 |-  ( x e. ( _V \ dom Funpart F ) -> ( ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) ` x ) = (/) )
25 19 24 sylbir 
 |-  ( -. x e. dom Funpart F -> ( ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) ` x ) = (/) )
26 ndmfv 
 |-  ( -. x e. dom Funpart F -> ( Funpart F ` x ) = (/) )
27 25 26 eqtr4d 
 |-  ( -. x e. dom Funpart F -> ( ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) ` x ) = ( Funpart F ` x ) )
28 16 27 pm2.61i 
 |-  ( ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) ` x ) = ( Funpart F ` x )
29 funpartfv 
 |-  ( Funpart F ` x ) = ( F ` x )
30 5 28 29 3eqtri 
 |-  ( FullFun F ` x ) = ( F ` x )
31 3 30 vtoclg 
 |-  ( A e. _V -> ( FullFun F ` A ) = ( F ` A ) )
32 fvprc 
 |-  ( -. A e. _V -> ( FullFun F ` A ) = (/) )
33 fvprc 
 |-  ( -. A e. _V -> ( F ` A ) = (/) )
34 32 33 eqtr4d 
 |-  ( -. A e. _V -> ( FullFun F ` A ) = ( F ` A ) )
35 31 34 pm2.61i 
 |-  ( FullFun F ` A ) = ( F ` A )