Definition df-spfin 4448

Description: Define the finite Sp set. Definition from [Rosser] p. 533. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-spfin	⊢ Spfin = ∩{a ∣ ( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a))}

Distinct variable group:   x,a,z

Detailed syntax breakdown of Definition df-spfin

Step	Hyp	Ref	Expression
1		cspfin 4440	. 2 class Spfin
2		cvv 2860	. . . . . . 7 class V
3	2	cncfin 4435	. . . . . 6 class Ncfin V
4		va	. . . . . . 7 setvar a
5	4	cv 1641	. . . . . 6 class a
6	3, 5	wcel 1710	. . . . 5 wff Ncfin V ∈ a
7		vz	. . . . . . . . . 10 setvar z
8	7	cv 1641	. . . . . . . . 9 class z
9		vx	. . . . . . . . . 10 setvar x
10	9	cv 1641	. . . . . . . . 9 class x
11	8, 10	wsfin 4439	. . . . . . . 8 wff Sfin (z, x)
12	7, 4	wel 1711	. . . . . . . 8 wff z ∈ a
13	11, 12	wi 4	. . . . . . 7 wff ( Sfin (z, x) → z ∈ a)
14	13, 7	wal 1540	. . . . . 6 wff ∀z( Sfin (z, x) → z ∈ a)
15	14, 9, 5	wral 2615	. . . . 5 wff ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a)
16	6, 15	wa 358	. . . 4 wff ( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a))
17	16, 4	cab 2339	. . 3 class {a ∣ ( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a))}
18	17	cint 3927	. 2 class ∩{a ∣ ( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a))}
19	1, 18	wceq 1642	1 wff Spfin = ∩{a ∣ ( Ncfin V ∈ a ∧ ∀x ∈ a ∀z( Sfin (z, x) → z ∈ a))}

This definition is used by:  spfinex  4538  ncvspfin  4539  spfinsfincl  4540  spfininduct  4541