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

Metamath Proof Explorer

Theorem fullfunfnv

Description: The full functional part of F is a function over _V . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion fullfunfnv 
|- FullFun F Fn _V

Proof

Step Hyp Ref Expression
1 funpartfun 
 |-  Fun Funpart F
2 funfn 
 |-  ( Fun Funpart F <-> Funpart F Fn dom Funpart F )
3 1 2 mpbi 
 |-  Funpart F Fn dom Funpart F
4 0ex 
 |-  (/) e. _V
5 4 fconst 
 |-  ( ( _V \ dom Funpart F ) X. { (/) } ) : ( _V \ dom Funpart F ) --> { (/) }
6 ffn 
 |-  ( ( ( _V \ dom Funpart F ) X. { (/) } ) : ( _V \ dom Funpart F ) --> { (/) } -> ( ( _V \ dom Funpart F ) X. { (/) } ) Fn ( _V \ dom Funpart F ) )
7 5 6 ax-mp 
 |-  ( ( _V \ dom Funpart F ) X. { (/) } ) Fn ( _V \ dom Funpart F )
8 3 7 pm3.2i 
 |-  ( Funpart F Fn dom Funpart F /\ ( ( _V \ dom Funpart F ) X. { (/) } ) Fn ( _V \ dom Funpart F ) )
9 disjdif 
 |-  ( dom Funpart F i^i ( _V \ dom Funpart F ) ) = (/)
10 fnun 
 |-  ( ( ( 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 ) ) = (/) ) -> ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) Fn ( dom Funpart F u. ( _V \ dom Funpart F ) ) )
11 8 9 10 mp2an 
 |-  ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) Fn ( dom Funpart F u. ( _V \ dom Funpart F ) )
12 df-fullfun 
 |-  FullFun F = ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) )
13 12 fneq1i 
 |-  ( FullFun F Fn _V <-> ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) Fn _V )
14 unvdif 
 |-  ( dom Funpart F u. ( _V \ dom Funpart F ) ) = _V
15 14 eqcomi 
 |-  _V = ( dom Funpart F u. ( _V \ dom Funpart F ) )
16 15 fneq2i 
 |-  ( ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) Fn _V <-> ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) Fn ( dom Funpart F u. ( _V \ dom Funpart F ) ) )
17 13 16 bitri 
 |-  ( FullFun F Fn _V <-> ( Funpart F u. ( ( _V \ dom Funpart F ) X. { (/) } ) ) Fn ( dom Funpart F u. ( _V \ dom Funpart F ) ) )
18 11 17 mpbir 
 |-  FullFun F Fn _V