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 = ∅, ∅, (℩n(n ∈ Nn ∧ ∃a ∈ M ℘1a ∈ 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 ∈ Nn
9		va	. . . . . . . . 9 setvar a
10	9	cv 1641	. . . . . . . 8 class a
11	10	cpw1 4136	. . . . . . 7 class ℘1a
12	11, 6	wcel 1710	. . . . . 6 wff ℘1a ∈ n
13	12, 9, 1	wrex 2616	. . . . 5 wff ∃a ∈ M ℘1a ∈ n
14	8, 13	wa 358	. . . 4 wff (n ∈ Nn ∧ ∃a ∈ M ℘1a ∈ n)
15	14, 5	cio 4338	. . 3 class (℩n(n ∈ Nn ∧ ∃a ∈ M ℘1a ∈ n))
16	4, 3, 15	cif 3663	. 2 class if(M = ∅, ∅, (℩n(n ∈ Nn ∧ ∃a ∈ M ℘1a ∈ n)))
17	2, 16	wceq 1642	1 wff Tfin M = if(M = ∅, ∅, (℩n(n ∈ Nn ∧ ∃a ∈ M ℘1a ∈ n)))

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