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