Definition df-sfin 4446

Description: Define the finite S relationship. This relationship encapsulates the idea of M being a "smaller" number than N. Definition from [Rosser] p. 530. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-sfin	|- ( Sfin (M, N) <-> (M e. Nn /\ N e. Nn /\ E.a(~P1 a e. M /\ ~Pa e. N)))

Distinct variable groups:   M,a   N,a

Detailed syntax breakdown of Definition df-sfin

Step	Hyp	Ref	Expression
1		cM	. . 3 class M
2		cN	. . 3 class N
3	1, 2	wsfin 4438	. 2 wff Sfin (M, N)
4		cnnc 4373	. . . 4 class Nn
5	1, 4	wcel 1710	. . 3 wff M e. Nn
6	2, 4	wcel 1710	. . 3 wff N e. Nn
7		va	. . . . . . . 8 setvar a
8	7	cv 1641	. . . . . . 7 class a
9	8	cpw1 4135	. . . . . 6 class ~P1 a
10	9, 1	wcel 1710	. . . . 5 wff ~P1 a e. M
11	8	cpw 3722	. . . . . 6 class ~Pa
12	11, 2	wcel 1710	. . . . 5 wff ~Pa e. N
13	10, 12	wa 358	. . . 4 wff (~P1 a e. M /\ ~Pa e. N)
14	13, 7	wex 1541	. . 3 wff E.a(~P1 a e. M /\ ~Pa e. N)
15	5, 6, 14	w3a 934	. 2 wff (M e. Nn /\ N e. Nn /\ E.a(~P1 a e. M /\ ~Pa e. N))
16	3, 15	wb 176	1 wff ( Sfin (M, N) <-> (M e. Nn /\ N e. Nn /\ E.a(~P1 a e. M /\ ~Pa e. N)))

This definition is referenced by:  srelk  4524  sfineq1  4526  sfineq2  4527  sfin01  4528  sfin112  4529  sfindbl  4530  sfintfin  4532  sfinltfin  4535  sfin111  4536  spfinsfincl  4539  vfinspnn  4541  1cvsfin  4542  vfinspsslem1  4550