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 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = 𝐴 → ( FullFun 𝐹 ‘ 𝑥 ) = ( FullFun 𝐹 ‘ 𝐴 ) )
2		fveq2	⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
3	1 2	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( FullFun 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ↔ ( FullFun 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ) )
4		df-fullfun	⊢ FullFun 𝐹 = ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) )
5	4	fveq1i	⊢ ( FullFun 𝐹 ‘ 𝑥 ) = ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 )
6		disjdif	⊢ ( dom Funpart 𝐹 ∩ ( V ∖ dom Funpart 𝐹 ) ) = ∅
7		funpartfun	⊢ Fun Funpart 𝐹
8		funfn	⊢ ( Fun Funpart 𝐹 ↔ Funpart 𝐹 Fn dom Funpart 𝐹 )
9	7 8	mpbi	⊢ Funpart 𝐹 Fn dom Funpart 𝐹
10		0ex	⊢ ∅ ∈ V
11	10	fconst	⊢ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) : ( V ∖ dom Funpart 𝐹 ) ⟶ { ∅ }
12		ffn	⊢ ( ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) : ( V ∖ dom Funpart 𝐹 ) ⟶ { ∅ } → ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) Fn ( V ∖ dom Funpart 𝐹 ) )
13	11 12	ax-mp	⊢ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) Fn ( V ∖ dom Funpart 𝐹 )
14		fvun1	⊢ ( ( Funpart 𝐹 Fn dom Funpart 𝐹 ∧ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) Fn ( V ∖ dom Funpart 𝐹 ) ∧ ( ( dom Funpart 𝐹 ∩ ( V ∖ dom Funpart 𝐹 ) ) = ∅ ∧ 𝑥 ∈ dom Funpart 𝐹 ) ) → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ( Funpart 𝐹 ‘ 𝑥 ) )
15	9 13 14	mp3an12	⊢ ( ( ( dom Funpart 𝐹 ∩ ( V ∖ dom Funpart 𝐹 ) ) = ∅ ∧ 𝑥 ∈ dom Funpart 𝐹 ) → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ( Funpart 𝐹 ‘ 𝑥 ) )
16	6 15	mpan	⊢ ( 𝑥 ∈ dom Funpart 𝐹 → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ( Funpart 𝐹 ‘ 𝑥 ) )
17		vex	⊢ 𝑥 ∈ V
18		eldif	⊢ ( 𝑥 ∈ ( V ∖ dom Funpart 𝐹 ) ↔ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ dom Funpart 𝐹 ) )
19	17 18	mpbiran	⊢ ( 𝑥 ∈ ( V ∖ dom Funpart 𝐹 ) ↔ ¬ 𝑥 ∈ dom Funpart 𝐹 )
20		fvun2	⊢ ( ( Funpart 𝐹 Fn dom Funpart 𝐹 ∧ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) Fn ( V ∖ dom Funpart 𝐹 ) ∧ ( ( dom Funpart 𝐹 ∩ ( V ∖ dom Funpart 𝐹 ) ) = ∅ ∧ 𝑥 ∈ ( V ∖ dom Funpart 𝐹 ) ) ) → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ( ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ‘ 𝑥 ) )
21	9 13 20	mp3an12	⊢ ( ( ( dom Funpart 𝐹 ∩ ( V ∖ dom Funpart 𝐹 ) ) = ∅ ∧ 𝑥 ∈ ( V ∖ dom Funpart 𝐹 ) ) → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ( ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ‘ 𝑥 ) )
22	6 21	mpan	⊢ ( 𝑥 ∈ ( V ∖ dom Funpart 𝐹 ) → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ( ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ‘ 𝑥 ) )
23	10	fvconst2	⊢ ( 𝑥 ∈ ( V ∖ dom Funpart 𝐹 ) → ( ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ‘ 𝑥 ) = ∅ )
24	22 23	eqtrd	⊢ ( 𝑥 ∈ ( V ∖ dom Funpart 𝐹 ) → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ∅ )
25	19 24	sylbir	⊢ ( ¬ 𝑥 ∈ dom Funpart 𝐹 → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ∅ )
26		ndmfv	⊢ ( ¬ 𝑥 ∈ dom Funpart 𝐹 → ( Funpart 𝐹 ‘ 𝑥 ) = ∅ )
27	25 26	eqtr4d	⊢ ( ¬ 𝑥 ∈ dom Funpart 𝐹 → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ( Funpart 𝐹 ‘ 𝑥 ) )
28	16 27	pm2.61i	⊢ ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ( Funpart 𝐹 ‘ 𝑥 )
29		funpartfv	⊢ ( Funpart 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 )
30	5 28 29	3eqtri	⊢ ( FullFun 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 )
31	3 30	vtoclg	⊢ ( 𝐴 ∈ V → ( FullFun 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
32		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( FullFun 𝐹 ‘ 𝐴 ) = ∅ )
33		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( 𝐹 ‘ 𝐴 ) = ∅ )
34	32 33	eqtr4d	⊢ ( ¬ 𝐴 ∈ V → ( FullFun 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
35	31 34	pm2.61i	⊢ ( FullFun 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 )