Definition df-fac 4869

Description: Define the factorial function on nonnegative integers. In the literature, the factorial function is written as a postscript exclamation point.

Assertion

Ref	Expression
df-fac	|- ! = (( x. seq(I |` NN)) u. {<.0, 1>.})

Detailed syntax breakdown of Definition df-fac

Step	Hyp	Ref	Expression
1		cfa 4868	. 2 class !
2		cmulc 4032	. . . 4 class x.
3		cid 2057	. . . . 5 class I
4		cn 4093	. . . . 5 class NN
5	3, 4	cres 2412	. . . 4 class (I |` NN)
6		cseq 4660	. . . 4 class seq
7	2, 5, 6	co 3001	. . 3 class ( x. seq(I |` NN))
8		cc0 4028	. . . . 5 class 0
9		c1 4029	. . . . 5 class 1
10	8, 9	cop 1810	. . . 4 class <.0, 1>.
11	10	csn 1808	. . 3 class {<.0, 1>.}
12	7, 11	cun 1485	. 2 class (( x. seq(I |` NN)) u. {<.0, 1>.})
13	1, 12	wceq 1091	1 wff ! = (( x. seq(I |` NN)) u. {<.0, 1>.})

This definition is referenced by:  facnnt 4870  fac0 4871

metamath.org