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	$⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F (A) = F (A)$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ x = A \to 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F (x) = 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F (A)$
2		fveq2	$⊢ x = A \to F (x) = F (A)$
3	1 2	eqeq12d	$⊢ x = A \to (𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F (x) = F (x) \leftrightarrow 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F (A) = F (A))$
4		df-fullfun	$⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})$
5	4	fveq1i	$⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F (x) = (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) (x)$
6		disjdif	$⊢ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cap (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) = \emptyset$
7		funpartfun	$⊢ Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F$
8		funfn	$⊢ Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \leftrightarrow 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F$
9	7 8	mpbi	$⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F$
10		0ex	$⊢ \emptyset \in V$
11	10	fconst	$⊢ ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) : V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ⟶ \{\emptyset\}$
12		ffn	$⊢ ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) : V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ⟶ \{\emptyset\} \to ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) Fn (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F)$
13	11 12	ax-mp	$⊢ ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) Fn (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F)$
14		fvun1	$⊢ (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \land ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) Fn (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \land (dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cap (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) = \emptyset \land x \in dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F)) \to (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) (x) = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F (x)$
15	9 13 14	mp3an12	$⊢ (dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cap (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) = \emptyset \land x \in dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \to (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) (x) = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F (x)$
16	6 15	mpan	$⊢ x \in dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \to (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) (x) = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F (x)$
17		vex	$⊢ x \in V$
18		eldif	$⊢ x \in (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \leftrightarrow (x \in V \land \neg x \in dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F)$
19	17 18	mpbiran	$⊢ x \in (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \leftrightarrow \neg x \in dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F$
20		fvun2	$⊢ (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \land ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) Fn (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \land (dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cap (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) = \emptyset \land x \in (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F))) \to (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) (x) = ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) (x)$
21	9 13 20	mp3an12	$⊢ (dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cap (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) = \emptyset \land x \in (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F)) \to (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) (x) = ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) (x)$
22	6 21	mpan	$⊢ x \in (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \to (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) (x) = ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) (x)$
23	10	fvconst2	$⊢ x \in (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \to ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}) (x) = \emptyset$
24	22 23	eqtrd	$⊢ x \in (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \to (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) (x) = \emptyset$
25	19 24	sylbir	$⊢ \neg x \in dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \to (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) (x) = \emptyset$
26		ndmfv	$⊢ \neg x \in dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \to 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F (x) = \emptyset$
27	25 26	eqtr4d	$⊢ \neg x \in dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \to (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) (x) = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F (x)$
28	16 27	pm2.61i	$⊢ (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})) (x) = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F (x)$
29		funpartfv	$⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F (x) = F (x)$
30	5 28 29	3eqtri	$⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F (x) = F (x)$
31	3 30	vtoclg	$⊢ A \in V \to 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F (A) = F (A)$
32		fvprc	$⊢ \neg A \in V \to 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F (A) = \emptyset$
33		fvprc	$⊢ \neg A \in V \to F (A) = \emptyset$
34	32 33	eqtr4d	$⊢ \neg A \in V \to 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F (A) = F (A)$
35	31 34	pm2.61i	$⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F (A) = F (A)$

Metamath Proof Explorer

Theorem fullfunfv

Proof