df-funs

Description: Define the class of all functions. See elfuns for membership. (Contributed by Scott Fenton, 18-Feb-2013)

		Ref	Expression
	Assertion	df-funs	$⊢ 𝖥𝗎𝗇𝗌 = 𝒫 (V \times V) ∖ 𝖥𝗂𝗑 (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1}))$

Step	Hyp	Ref	Expression
0		cfuns	$class 𝖥𝗎𝗇𝗌$
1		cvv	$class V$
2	1 1	cxp	$class (V \times V)$
3	2	cpw	$class 𝒫 (V \times V)$
4		cep	$class E$
5		c1st	$class 1^{st}$
6		cid	$class I$
7	1 6	cdif	$class (V ∖ I)$
8		c2nd	$class 2^{nd}$
9	7 8	ccom	$class ((V ∖ I) \circ 2^{nd})$
10	5 9	ctxp	$class (1^{st} \otimes ((V ∖ I) \circ 2^{nd}))$
11	4	ccnv	$class E^{-1}$
12	10 11	ccom	$class ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1})$
13	4 12	ccom	$class (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1}))$
14	13	cfix	$class 𝖥𝗂𝗑 (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1}))$
15	3 14	cdif	$class (𝒫 (V \times V) ∖ 𝖥𝗂𝗑 (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1})))$
16	0 15	wceq	$wff 𝖥𝗎𝗇𝗌 = 𝒫 (V \times V) ∖ 𝖥𝗂𝗑 (E \circ ((1^{st} \otimes ((V ∖ I) \circ 2^{nd})) \circ E^{-1}))$

Metamath Proof Explorer