New Foundations Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-sfin		Unicode version

---

Definition df-sfin 4446

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

Assertion

Ref	Expression
df-sfin	Sfin Nn Nn 1

Distinct variable groups:   ,   ,

---

Detailed syntax breakdown of Definition df-sfin

Step	Hyp	Ref	Expression
1		cM	. . 3
2		cN	. . 3
3	1, 2	wsfin 4438	. 2 Sfin
4		cnnc 4373	. . . 4 Nn
5	1, 4	wcel 1710	. . 3 Nn
6	2, 4	wcel 1710	. . 3 Nn
7		va	. . . . . . . 8
8	7	cv 1641	. . . . . . 7
9	8	cpw1 4135	. . . . . 6 1
10	9, 1	wcel 1710	. . . . 5 1
11	8	cpw 3722	. . . . . 6
12	11, 2	wcel 1710	. . . . 5
13	10, 12	wa 358	. . . 4 1
14	13, 7	wex 1541	. . 3 1
15	5, 6, 14	w3a 934	. 2 Nn Nn 1
16	3, 15	wb 176	1 Sfin Nn Nn 1

Colors of variables: wff setvar class

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

Copyright terms: Public domain

W3C validator