Definition df-fun

Description: Define predicate that determines if some class A is a function. Definition 10.1 of Quine p. 65. For example, the expression Fun cos is true once we define cosine ( df-cos ). This is not the same as defining a specific function's mapping, which is typically done using the format of cmpt with the maps-to notation (see df-mpt and df-mpo ). Contrast this predicate with the predicates to determine if some class is a function with a given domain ( df-fn ), a function with a given domain and codomain ( df-f ), a one-to-one function ( df-f1 ), an onto function ( df-fo ), or a one-to-one onto function ( df-f1o ). For alternate definitions, see dffun2 , dffun3 , dffun4 , dffun5 , dffun6 , dffun7 , dffun8 , and dffun9 . (Contributed by NM, 1-Aug-1994)

	Ref	Expression
Assertion	df-fun	$$⊢\mathrm{Fun}A\leftrightarrow \left(\mathrm{Rel}A\wedge A\circ A^{-1}\subseteq \mathrm{I}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	wfun	$$wff\mathrm{Fun}A$$
2	0	wrel	$$wff\mathrm{Rel}A$$
3	0	ccnv	$$class{A}^{-1}$$
4	0 3	ccom	$$class\left(A\circ A^{-1}\right)$$
5		cid	$$class\mathrm{I}$$
6	4 5	wss	$$wffA\circ A^{-1}\subseteq \mathrm{I}$$
7	2 6	wa	$$wff\left(\mathrm{Rel}A\wedge A\circ A^{-1}\subseteq \mathrm{I}\right)$$
8	1 7	wb	$$wff\left(\mathrm{Fun}A\leftrightarrow \left(\mathrm{Rel}A\wedge A\circ A^{-1}\subseteq \mathrm{I}\right)\right)$$