Definition df-tfin 4444

Description: Define the finite T operator. Definition from [Rosser] p. 528. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-tfin	|- Tfin M = if(M = (/), (/), (iotan(n e. Nn /\ E.a e. M ~P1 a e. n)))

Distinct variable group:   n,M,a

Detailed syntax breakdown of Definition df-tfin

Step	Hyp	Ref	Expression
1		cM	. . 3 class M
2	1	ctfin 4436	. 2 class Tfin M
3		c0 3551	. . . 4 class (/)
4	1, 3	wceq 1642	. . 3 wff M = (/)
5		vn	. . . . . . 7 setvar n
6	5	cv 1641	. . . . . 6 class n
7		cnnc 4374	. . . . . 6 class Nn
8	6, 7	wcel 1710	. . . . 5 wff n e. Nn
9		va	. . . . . . . . 9 setvar a
10	9	cv 1641	. . . . . . . 8 class a
11	10	cpw1 4136	. . . . . . 7 class ~P1 a
12	11, 6	wcel 1710	. . . . . 6 wff ~P1 a e. n
13	12, 9, 1	wrex 2616	. . . . 5 wff E.a e. M ~P1 a e. n
14	8, 13	wa 358	. . . 4 wff (n e. Nn /\ E.a e. M ~P1 a e. n)
15	14, 5	cio 4338	. . 3 class (iotan(n e. Nn /\ E.a e. M ~P1 a e. n))
16	4, 3, 15	cif 3663	. 2 class if(M = (/), (/), (iotan(n e. Nn /\ E.a e. M ~P1 a e. n)))
17	2, 16	wceq 1642	1 wff Tfin M = if(M = (/), (/), (iotan(n e. Nn /\ E.a e. M ~P1 a e. n)))

This definition is referenced by:  tfinex  4486  eqtfinrelk  4487  tfineq  4489  tfinprop  4490  tfinnul  4492