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

Metamath Proof Explorer

Definition df-fullfun

Description: Define the full function over F . This is a function with domain _V that always agrees with F for its value. (Contributed by Scott Fenton, 17-Apr-2014)

Ref Expression
Assertion df-fullfun FullFun 𝐹 = ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cF ⊢ 𝐹
1 0 cfullfn ⊢ FullFun 𝐹
2 0 cfunpart ⊢ Funpart 𝐹
3 cvv ⊢ V
4 2 cdm ⊢ dom Funpart 𝐹
5 3 4 cdif ⊢ ( V ∖ dom Funpart 𝐹 )
6 c0 ⊢ ∅
7 6 csn ⊢ { ∅ }
8 5 7 cxp ⊢ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } )
9 2 8 cun ⊢ ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) )
10 1 9 wceq ⊢ FullFun 𝐹 = ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) )