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	$⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F Fn V$

Proof

Step	Hyp	Ref	Expression
1		funpartfun	$⊢ Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F$
2		funfn	$⊢ Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \leftrightarrow 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F$
3	1 2	mpbi	$⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F$
4		0ex	$⊢ \emptyset \in V$
5	4	fconst	$⊢ ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) : V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ⟶ \{\emptyset\}$
6		ffn	$⊢ ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) : V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ⟶ \{\emptyset\} \to ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) Fn (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F)$
7	5 6	ax-mp	$⊢ ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) Fn (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F)$
8	3 7	pm3.2i	$⊢ (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \land ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) Fn (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F))$
9		disjdif	$⊢ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cap (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) = \emptyset$
10		fnun	$⊢ ((𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \land ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) Fn (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F)) \land dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cap (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) = \emptyset) \to (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) Fn (dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F))$
11	8 9 10	mp2an	$⊢ (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) Fn (dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F))$
12		df-fullfun	$⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})$
13	12	fneq1i	$⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F Fn V \leftrightarrow (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) Fn V$
14		unvdif	$⊢ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) = V$
15	14	eqcomi	$⊢ V = dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F)$
16	15	fneq2i	$⊢ (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) Fn V \leftrightarrow (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) Fn (dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F))$
17	13 16	bitri	$⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F Fn V \leftrightarrow (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) Fn (dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F))$
18	11 17	mpbir	$⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F Fn V$