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 𝐹 Fn V

Proof

Step	Hyp	Ref	Expression
1		funpartfun	⊢ Fun Funpart 𝐹
2		funfn	⊢ ( Fun Funpart 𝐹 ↔ Funpart 𝐹 Fn dom Funpart 𝐹 )
3	1 2	mpbi	⊢ Funpart 𝐹 Fn dom Funpart 𝐹
4		0ex	⊢ ∅ ∈ V
5	4	fconst	⊢ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) : ( V ∖ dom Funpart 𝐹 ) ⟶ { ∅ }
6		ffn	⊢ ( ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) : ( V ∖ dom Funpart 𝐹 ) ⟶ { ∅ } → ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) Fn ( V ∖ dom Funpart 𝐹 ) )
7	5 6	ax-mp	⊢ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) Fn ( V ∖ dom Funpart 𝐹 )
8	3 7	pm3.2i	⊢ ( Funpart 𝐹 Fn dom Funpart 𝐹 ∧ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) Fn ( V ∖ dom Funpart 𝐹 ) )
9		disjdif	⊢ ( dom Funpart 𝐹 ∩ ( V ∖ dom Funpart 𝐹 ) ) = ∅
10		fnun	⊢ ( ( ( Funpart 𝐹 Fn dom Funpart 𝐹 ∧ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) Fn ( V ∖ dom Funpart 𝐹 ) ) ∧ ( dom Funpart 𝐹 ∩ ( V ∖ dom Funpart 𝐹 ) ) = ∅ ) → ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) Fn ( dom Funpart 𝐹 ∪ ( V ∖ dom Funpart 𝐹 ) ) )
11	8 9 10	mp2an	⊢ ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) Fn ( dom Funpart 𝐹 ∪ ( V ∖ dom Funpart 𝐹 ) )
12		df-fullfun	⊢ FullFun 𝐹 = ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) )
13	12	fneq1i	⊢ ( FullFun 𝐹 Fn V ↔ ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) Fn V )
14		unvdif	⊢ ( dom Funpart 𝐹 ∪ ( V ∖ dom Funpart 𝐹 ) ) = V
15	14	eqcomi	⊢ V = ( dom Funpart 𝐹 ∪ ( V ∖ dom Funpart 𝐹 ) )
16	15	fneq2i	⊢ ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) Fn V ↔ ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) Fn ( dom Funpart 𝐹 ∪ ( V ∖ dom Funpart 𝐹 ) ) )
17	13 16	bitri	⊢ ( FullFun 𝐹 Fn V ↔ ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) Fn ( dom Funpart 𝐹 ∪ ( V ∖ dom Funpart 𝐹 ) ) )
18	11 17	mpbir	⊢ FullFun 𝐹 Fn V