Definition 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	⊢ Funs = ( 𝒫 ( V × V ) ∖ Fix ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfuns	⊢ Funs
1		cvv	⊢ V
2	1 1	cxp	⊢ ( V × V )
3	2	cpw	⊢ 𝒫 ( V × V )
4		cep	⊢ E
5		c1st	⊢ 1st
6		cid	⊢ I
7	1 6	cdif	⊢ ( V ∖ I )
8		c2nd	⊢ 2nd
9	7 8	ccom	⊢ ( ( V ∖ I ) ∘ 2nd )
10	5 9	ctxp	⊢ ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) )
11	4	ccnv	⊢ ◡ E
12	10 11	ccom	⊢ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E )
13	4 12	ccom	⊢ ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) )
14	13	cfix	⊢ Fix ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) )
15	3 14	cdif	⊢ ( 𝒫 ( V × V ) ∖ Fix ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) ) )
16	0 15	wceq	⊢ Funs = ( 𝒫 ( V × V ) ∖ Fix ( E ∘ ( ( 1st ⊗ ( ( V ∖ I ) ∘ 2nd ) ) ∘ ◡ E ) ) )