Definition df-lefin 4441

Description: Define the less than or equal to relationship for finite cardinals. Definition from Ex. X.1.4 of [Rosser] p. 279. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-lefin	⊢ ≤fin = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃w ∈ Nn z = (y +c w))}

Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Definition df-lefin

Step	Hyp	Ref	Expression
1		clefin 4433	. 2 class ≤fin
2		vx	. . . . . . . 8 setvar x
3	2	cv 1641	. . . . . . 7 class x
4		vy	. . . . . . . . 9 setvar y
5	4	cv 1641	. . . . . . . 8 class y
6		vz	. . . . . . . . 9 setvar z
7	6	cv 1641	. . . . . . . 8 class z
8	5, 7	copk 4058	. . . . . . 7 class ⟪y, z⟫
9	3, 8	wceq 1642	. . . . . 6 wff x = ⟪y, z⟫
10		vw	. . . . . . . . . 10 setvar w
11	10	cv 1641	. . . . . . . . 9 class w
12	5, 11	cplc 4376	. . . . . . . 8 class (y +c w)
13	7, 12	wceq 1642	. . . . . . 7 wff z = (y +c w)
14		cnnc 4374	. . . . . . 7 class Nn
15	13, 10, 14	wrex 2616	. . . . . 6 wff ∃w ∈ Nn z = (y +c w)
16	9, 15	wa 358	. . . . 5 wff (x = ⟪y, z⟫ ∧ ∃w ∈ Nn z = (y +c w))
17	16, 6	wex 1541	. . . 4 wff ∃z(x = ⟪y, z⟫ ∧ ∃w ∈ Nn z = (y +c w))
18	17, 4	wex 1541	. . 3 wff ∃y∃z(x = ⟪y, z⟫ ∧ ∃w ∈ Nn z = (y +c w))
19	18, 2	cab 2339	. 2 class {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃w ∈ Nn z = (y +c w))}
20	1, 19	wceq 1642	1 wff ≤fin = {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃w ∈ Nn z = (y +c w))}

This definition is referenced by:  opklefing  4449