Definition df-fac 10908

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 15864). In the literature, the factorial function is written as a postscript exclamation point. (Contributed by NM, 2-Dec-2004.)

Assertion

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

Detailed syntax breakdown of Definition df-fac

Step	Hyp	Ref	Expression
1		cfa 10907	. 2 class !
2		cc0 7960	. . . . 5 class 0
3		c1 7961	. . . . 5 class 1
4	2, 3	cop 3646	. . . 4 class <. 0 , 1 >.
5	4	csn 3643	. . 3 class { <. 0 , 1 >. }
6		cmul 7965	. . . 4 class x.
7		cid 4353	. . . 4 class _I
8	6, 7, 3	cseq 10629	. . 3 class seq 1 ( x. , _I )
9	5, 8	cun 3172	. 2 class ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
10	1, 9	wceq 1373	1 wff ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )

This definition is referenced by:  facnn  10909  fac0  10910