funpartfv

Description: The function value of the functional part is identical to the original functional value. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	funpartfv	$⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F (A) = F (A)$

Proof

Step	Hyp	Ref	Expression
1		df-funpart	$⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F = {F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}$
2	1	fveq1i	$⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F (A) = ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) (A)$
3		fvres	$⊢ A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \to ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) (A) = F (A)$
4		nfvres	$⊢ \neg A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \to ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) (A) = \emptyset$
5		funpartlem	$⊢ A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \leftrightarrow \exists x F [\{A\}] = \{x\}$
6		eusn	$⊢ \exists! x x \in F [\{A\}] \leftrightarrow \exists x F [\{A\}] = \{x\}$
7	5 6	bitr4i	$⊢ A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \leftrightarrow \exists! x x \in F [\{A\}]$
8		elimasng	$⊢ (A \in V \land x \in V) \to (x \in F [\{A\}] \leftrightarrow ⟨A, x⟩ \in F)$
9	8	elvd	$⊢ A \in V \to (x \in F [\{A\}] \leftrightarrow ⟨A, x⟩ \in F)$
10		df-br	$⊢ A F x \leftrightarrow ⟨A, x⟩ \in F$
11	9 10	bitr4di	$⊢ A \in V \to (x \in F [\{A\}] \leftrightarrow A F x)$
12	11	eubidv	$⊢ A \in V \to (\exists! x x \in F [\{A\}] \leftrightarrow \exists! x A F x)$
13	7 12	syl5bb	$⊢ A \in V \to (A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \leftrightarrow \exists! x A F x)$
14	13	notbid	$⊢ A \in V \to (\neg A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \leftrightarrow \neg \exists! x A F x)$
15		tz6.12-2	$⊢ \neg \exists! x A F x \to F (A) = \emptyset$
16	14 15	syl6bi	$⊢ A \in V \to (\neg A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \to F (A) = \emptyset)$
17		fvprc	$⊢ \neg A \in V \to F (A) = \emptyset$
18	17	a1d	$⊢ \neg A \in V \to (\neg A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \to F (A) = \emptyset)$
19	16 18	pm2.61i	$⊢ \neg A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \to F (A) = \emptyset$
20	4 19	eqtr4d	$⊢ \neg A \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \to ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) (A) = F (A)$
21	3 20	pm2.61i	$⊢ ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) (A) = F (A)$
22	2 21	eqtri	$⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F (A) = F (A)$

Metamath Proof Explorer

Theorem funpartfv

Proof