funpartfun

Description: The functional part of F is a function. (Contributed by Scott Fenton, 16-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

		Ref	Expression
	Assertion	funpartfun	$⊢ Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F$

Proof

Step	Hyp	Ref	Expression
1		relres	$⊢ Rel ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))})$
2		vex	$⊢ z \in V$
3	2	brresi	$⊢ x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) z \leftrightarrow (x \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \land x F z)$
4	3	simprbi	$⊢ x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) z \to x F z$
5		vex	$⊢ y \in V$
6	5	brresi	$⊢ x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) y \leftrightarrow (x \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \land x F y)$
7		funpartlem	$⊢ x \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \leftrightarrow \exists w F [\{x\}] = \{w\}$
8	7	anbi1i	$⊢ (x \in dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)) \land x F y) \leftrightarrow (\exists w F [\{x\}] = \{w\} \land x F y)$
9	6 8	bitri	$⊢ x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) y \leftrightarrow (\exists w F [\{x\}] = \{w\} \land x F y)$
10		df-br	$⊢ x F y \leftrightarrow ⟨x, y⟩ \in F$
11		df-br	$⊢ x F z \leftrightarrow ⟨x, z⟩ \in F$
12	10 11	anbi12i	$⊢ (x F y \land x F z) \leftrightarrow (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F)$
13		vex	$⊢ x \in V$
14	13 5	elimasn	$⊢ y \in F [\{x\}] \leftrightarrow ⟨x, y⟩ \in F$
15	13 2	elimasn	$⊢ z \in F [\{x\}] \leftrightarrow ⟨x, z⟩ \in F$
16	14 15	anbi12i	$⊢ (y \in F [\{x\}] \land z \in F [\{x\}]) \leftrightarrow (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F)$
17	12 16	bitr4i	$⊢ (x F y \land x F z) \leftrightarrow (y \in F [\{x\}] \land z \in F [\{x\}])$
18		eleq2	$⊢ F [\{x\}] = \{w\} \to (y \in F [\{x\}] \leftrightarrow y \in \{w\})$
19		eleq2	$⊢ F [\{x\}] = \{w\} \to (z \in F [\{x\}] \leftrightarrow z \in \{w\})$
20	18 19	anbi12d	$⊢ F [\{x\}] = \{w\} \to ((y \in F [\{x\}] \land z \in F [\{x\}]) \leftrightarrow (y \in \{w\} \land z \in \{w\}))$
21		velsn	$⊢ y \in \{w\} \leftrightarrow y = w$
22		velsn	$⊢ z \in \{w\} \leftrightarrow z = w$
23		equtr2	$⊢ (y = w \land z = w) \to y = z$
24	21 22 23	syl2anb	$⊢ (y \in \{w\} \land z \in \{w\}) \to y = z$
25	20 24	syl6bi	$⊢ F [\{x\}] = \{w\} \to ((y \in F [\{x\}] \land z \in F [\{x\}]) \to y = z)$
26	17 25	syl5bi	$⊢ F [\{x\}] = \{w\} \to ((x F y \land x F z) \to y = z)$
27	26	exlimiv	$⊢ \exists w F [\{x\}] = \{w\} \to ((x F y \land x F z) \to y = z)$
28	27	impl	$⊢ ((\exists w F [\{x\}] = \{w\} \land x F y) \land x F z) \to y = z$
29	9 28	sylanb	$⊢ (x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) y \land x F z) \to y = z$
30	4 29	sylan2	$⊢ (x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) y \land x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) z) \to y = z$
31	30	gen2	$⊢ \forall y \forall z ((x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) y \land x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) z) \to y = z)$
32	31	ax-gen	$⊢ \forall x \forall y \forall z ((x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) y \land x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) z) \to y = z)$
33		df-funpart	$⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F = {F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}$
34	33	funeqi	$⊢ Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \leftrightarrow Fun ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))})$
35		dffun2	$⊢ Fun ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) \leftrightarrow (Rel ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) \land \forall x \forall y \forall z ((x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) y \land x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) z) \to y = z))$
36	34 35	bitri	$⊢ Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \leftrightarrow (Rel ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) \land \forall x \forall y \forall z ((x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) y \land x ({F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}) z) \to y = z))$
37	1 32 36	mpbir2an	$⊢ Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F$

Metamath Proof Explorer

Theorem funpartfun

Proof