Definition df-fac

Description: Define the factorial function on nonnegative integers. For example, ( !5 ) = 1 2 0 because 1 x. 2 x. 3 x. 4 x. 5 = 1 2 0 ( ex-fac ). In the literature, the factorial function is written as a postscript exclamation point. (Contributed by NM, 2-Dec-2004)

	Ref	Expression
Assertion	df-fac	$$⊢!=\left\{⟨0,1⟩\right\}\cup seq1\left(\times ,\mathrm{I}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfa	$$class!$$
1		cc0	$$class0$$
2		c1	$$class1$$
3	1 2	cop	$$class⟨0,1⟩$$
4	3	csn	$$class\left\{⟨0,1⟩\right\}$$
5		cmul	$$class\times$$
6		cid	$$class\mathrm{I}$$
7	5 6 2	cseq	$$classseq1\left(\times ,\mathrm{I}\right)$$
8	4 7	cun	$$class\left(\left\{⟨0,1⟩\right\}\cup seq1\left(\times ,\mathrm{I}\right)\right)$$
9	0 8	wceq	$$wff!=\left\{⟨0,1⟩\right\}\cup seq1\left(\times ,\mathrm{I}\right)$$