Definition df-nnc 4380

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

Assertion

Ref	Expression
df-nnc	⊢ Nn = ∩{b ∣ (0c ∈ b ∧ ∀y ∈ b (y +c 1c) ∈ b)}

Distinct variable group:   y,b

Detailed syntax breakdown of Definition df-nnc

Step	Hyp	Ref	Expression
1		cnnc 4374	. 2 class Nn
2		c0c 4375	. . . . . 6 class 0c
3		vb	. . . . . . 7 setvar b
4	3	cv 1641	. . . . . 6 class b
5	2, 4	wcel 1710	. . . . 5 wff 0c ∈ b
6		vy	. . . . . . . . 9 setvar y
7	6	cv 1641	. . . . . . . 8 class y
8		c1c 4135	. . . . . . . 8 class 1c
9	7, 8	cplc 4376	. . . . . . 7 class (y +c 1c)
10	9, 4	wcel 1710	. . . . . 6 wff (y +c 1c) ∈ b
11	10, 6, 4	wral 2615	. . . . 5 wff ∀y ∈ b (y +c 1c) ∈ b
12	5, 11	wa 358	. . . 4 wff (0c ∈ b ∧ ∀y ∈ b (y +c 1c) ∈ b)
13	12, 3	cab 2339	. . 3 class {b ∣ (0c ∈ b ∧ ∀y ∈ b (y +c 1c) ∈ b)}
14	13	cint 3927	. 2 class ∩{b ∣ (0c ∈ b ∧ ∀y ∈ b (y +c 1c) ∈ b)}
15	1, 14	wceq 1642	1 wff Nn = ∩{b ∣ (0c ∈ b ∧ ∀y ∈ b (y +c 1c) ∈ b)}

This definition is referenced by:  dfnnc2  4396  peano1  4403  peano2  4404  peano5  4410  dfnnc3  5886