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 ∘ ( ( 1^st ⊗ ( ( V ∖ I ) ∘ 2^nd ) ) ∘ ^◡ E ) ) )

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	⊢ 1^st
6		cid	⊢ I
7	1 6	cdif	⊢ ( V ∖ I )
8		c2nd	⊢ 2^nd
9	7 8	ccom	⊢ ( ( V ∖ I ) ∘ 2^nd )
10	5 9	ctxp	⊢ ( 1^st ⊗ ( ( V ∖ I ) ∘ 2^nd ) )
11	4	ccnv	⊢ ^◡ E
12	10 11	ccom	⊢ ( ( 1^st ⊗ ( ( V ∖ I ) ∘ 2^nd ) ) ∘ ^◡ E )
13	4 12	ccom	⊢ ( E ∘ ( ( 1^st ⊗ ( ( V ∖ I ) ∘ 2^nd ) ) ∘ ^◡ E ) )
14	13	cfix	⊢ Fix ( E ∘ ( ( 1^st ⊗ ( ( V ∖ I ) ∘ 2^nd ) ) ∘ ^◡ E ) )
15	3 14	cdif	⊢ ( 𝒫 ( V × V ) ∖ Fix ( E ∘ ( ( 1^st ⊗ ( ( V ∖ I ) ∘ 2^nd ) ) ∘ ^◡ E ) ) )
16	0 15	wceq	⊢ Funs = ( 𝒫 ( V × V ) ∖ Fix ( E ∘ ( ( 1^st ⊗ ( ( V ∖ I ) ∘ 2^nd ) ) ∘ ^◡ E ) ) )

Metamath Proof Explorer