Definition df-sfin 4447

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 ∈ Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ 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 4439	. 2 wff Sfin (M, N)
4		cnnc 4374	. . . 4 class Nn
5	1, 4	wcel 1710	. . 3 wff M ∈ Nn
6	2, 4	wcel 1710	. . 3 wff N ∈ Nn
7		va	. . . . . . . 8 setvar a
8	7	cv 1641	. . . . . . 7 class a
9	8	cpw1 4136	. . . . . 6 class ℘1a
10	9, 1	wcel 1710	. . . . 5 wff ℘1a ∈ M
11	8	cpw 3723	. . . . . 6 class ℘a
12	11, 2	wcel 1710	. . . . 5 wff ℘a ∈ N
13	10, 12	wa 358	. . . 4 wff (℘1a ∈ M ∧ ℘a ∈ N)
14	13, 7	wex 1541	. . 3 wff ∃a(℘1a ∈ M ∧ ℘a ∈ N)
15	5, 6, 14	w3a 934	. 2 wff (M ∈ Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ N))
16	3, 15	wb 176	1 wff ( Sfin (M, N) ↔ (M ∈ Nn ∧ N ∈ Nn ∧ ∃a(℘1a ∈ M ∧ ℘a ∈ N)))

This definition is used by:  srelk  4525  sfineq1  4527  sfineq2  4528  sfin01  4529  sfin112  4530  sfindbl  4531  sfintfin  4533  sfinltfin  4536  sfin111  4537  spfinsfincl  4540  vfinspnn  4542  1cvsfin  4543  vfinspsslem1  4551