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 | E.yE.z(x = <<y, z>> /\ E.w e. Nn z = (y +o 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 +o w)
13	7, 12	wceq 1642	. . . . . . 7 wff z = (y +o w)
14		cnnc 4374	. . . . . . 7 class Nn
15	13, 10, 14	wrex 2616	. . . . . 6 wff E.w e. Nn z = (y +o w)
16	9, 15	wa 358	. . . . 5 wff (x = <<y, z>> /\ E.w e. Nn z = (y +o w))
17	16, 6	wex 1541	. . . 4 wff E.z(x = <<y, z>> /\ E.w e. Nn z = (y +o w))
18	17, 4	wex 1541	. . 3 wff E.yE.z(x = <<y, z>> /\ E.w e. Nn z = (y +o w))
19	18, 2	cab 2339	. 2 class {x | E.yE.z(x = <<y, z>> /\ E.w e. Nn z = (y +o w))}
20	1, 19	wceq 1642	1 wff <_fin = {x | E.yE.z(x = <<y, z>> /\ E.w e. Nn z = (y +o w))}

This definition is referenced by:  opklefing  4449