Home New Foundations ExplorerTheorem List (p. 44 of 64) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 4301-4400   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremdfpw12 4301 Alternate expression for unit power classes. (Contributed by SF, 26-Jan-2015.)
1 SIk k k

Theorempw1exg 4302 The unit power class preserves sethood. (Contributed by SF, 14-Jan-2015.)
1

Theorempw1ex 4303 The unit power class preserves sethood. (Contributed by SF, 14-Jan-2015.)
1

Theoreminsklem 4304* Lemma for ins2kexg 4305 and ins3kexg 4306. Equality for subsets of 1 1c k k . (Contributed by SF, 14-Jan-2015.)
1 1c k k        1 1c k k

Theoremins2kexg 4305 Ins2k preserves sethood. (Contributed by SF, 14-Jan-2015.)
Ins2k

Theoremins3kexg 4306 Ins3k preserves sethood. (Contributed by SF, 14-Jan-2015.)
Ins3k

Theoremins2kex 4307 Ins2k preserves sethood. (Contributed by SF, 14-Jan-2015.)
Ins2k

Theoremins3kex 4308 Ins3k preserves sethood. (Contributed by SF, 14-Jan-2015.)
Ins3k

Theoremcokexg 4309 The Kuratowski composition of two sets is a set. (Contributed by SF, 14-Jan-2015.)
k

Theoremcokex 4310 The Kuratowski composition of two sets is a set. (Contributed by SF, 14-Jan-2015.)
k

Theoremimagekexg 4311 The Kuratowski image functor preserves sethood. (Contributed by SF, 14-Jan-2015.)
Imagek

Theoremimagekex 4312 The Kuratowski image functor preserves sethood. (Contributed by SF, 14-Jan-2015.)
Imagek

Theoremdfidk2 4313 Definition of k in terms of Sk. (Contributed by SF, 14-Jan-2015.)
k Sk k Sk

Theoremidkex 4314 The Kuratowski identity relationship is a set. (Contributed by SF, 14-Jan-2015.)
k

Theoremdfuni3 4315 Alternate definition of class union for existence proof. (Contributed by SF, 14-Jan-2015.)
1k Sk k

Theoremuniexg 4316 The sum class of a set is a set. (Contributed by SF, 14-Jan-2015.)

Theoremuniex 4317 The sum class of a set is a set. (Contributed by SF, 14-Jan-2015.)

Theoremdfint3 4318 Alternate definition of class intersection for the existence proof. (Contributed by SF, 14-Jan-2015.)
∼ ⋃1kSk k

Theoremintexg 4319 The intersection of a set is a set. (Contributed by SF, 14-Jan-2015.)

Theoremintex 4320 The intersection of a set is a set. (Contributed by SF, 14-Jan-2015.)

Theoremsetswith 4321* Two ways to express the class of all sets that contain . (Contributed by SF, 14-Jan-2015.)
Sk k

Theoremsetswithex 4322* The class of all sets that contain exist. (Contributed by SF, 14-Jan-2015.)

Theoremndisjrelk 4323 Membership in a particular Kuratowski relationship is equivalent to non-disjointedness. (Contributed by SF, 15-Jan-2015.)
Ins3k Sk Ins2k Sk k1 1 1c

Theoremabexv 4324* When does not occur in , is a set. (Contributed by SF, 17-Jan-2015.)

Theoremunipw1 4325 The union of a unit power class is the original set. (Contributed by SF, 20-Jan-2015.)
1

Theorempw1exb 4326 Biconditional existence for unit power class. (Contributed by SF, 20-Jan-2015.)
1

Theoremdfpw2 4327 Definition of power set for existence proof. (Contributed by SF, 21-Jan-2015.)
Sk 1 k k1c

Theorempwexg 4328 The power class of a set is a set. (Contributed by SF, 21-Jan-2015.)

Theorempwex 4329 The power class of a set is a set. (Contributed by SF, 21-Jan-2015.)

Theoremeqpw1uni 4330 A class of singletons is equal to the unit power class of its union. (Contributed by SF, 26-Jan-2015.)
1c 1

Theorempw1equn 4331* A condition for a unit power class to equal a union. (Contributed by SF, 26-Jan-2015.)
1 1 1

Theorempw1eqadj 4332* A condition for a unit power class to work out to an adjunction. (Contributed by SF, 26-Jan-2015.)
1 1

Theoremdfeu2 4333 Alternate definition of existential uniqueness in terms of abstraction. (Contributed by SF, 29-Jan-2015.)
1c

Theoremeuabex 4334 If there is a unique object satisfying a property , then the set of all elements that satisfy exists. (Contributed by SF, 16-Jan-2015.)

Theoremsspw1 4335* A condition for being a subclass of a unit power class. Corollary 2 of theorem IX.6.14 of [Rosser] p. 255. (Contributed by SF, 3-Feb-2015.)
1 1

Theoremsspw12 4336* A set is a subset of cardinal one iff it is the unit power class of some other set. (Contributed by SF, 17-Mar-2015.)
1c 1

2.2.9  Definite description binder (inverted iota)

Syntaxcio 4337 Extend class notation with Russell's definition description binder (inverted iota).

Theoremiotajust 4338* Soundness justification theorem for df-iota 4339. (Contributed by Andrew Salmon, 29-Jun-2011.)

Definitiondf-iota 4339* Define Russell's definition description binder, which can be read as "the unique such that ," where ordinarily contains as a free variable. Our definition is meaningful only when there is exactly one such that is true (see iotaval 4350); otherwise, it evaluates to the empty set (see iotanul 4354). Russell used the inverted iota symbol to represent the binder. (Contributed by SF, 12-Jan-2015.)

Theoremdfiota2 4340* Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.)

Theoremnfiota1 4341 Bound-variable hypothesis builder for the class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)

Theoremnfiotad 4342 Deduction version of nfiota 4343. (Contributed by NM, 18-Feb-2013.)

Theoremnfiota 4343 Bound-variable hypothesis builder for the class. (Contributed by NM, 23-Aug-2011.)

Theoremcbviota 4344 Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)

Theoremcbviotav 4345* Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)

Theoremsb8iota 4346 Variable substitution in description binder. Compare sb8eu 2222. (Contributed by NM, 18-Mar-2013.)

Theoremiotaeq 4347 Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)

Theoremiotabi 4348 Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)

Theoremuniabio 4349* Part of Theorem 8.17 in [Quine] p. 56. This theorem serves as a lemma for the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.)

Theoremiotaval 4350* Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.)

Theoremiotauni 4351 Equivalence between two different forms of . (Contributed by Andrew Salmon, 12-Jul-2011.)

Theoremiotaint 4352 Equivalence between two different forms of . (Contributed by Mario Carneiro, 24-Dec-2016.)

Theoremiota1 4353 Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)

Theoremiotanul 4354 Theorem 8.22 in [Quine] p. 57. This theorem is the result if there isn't exactly one that satisfies . (Contributed by Andrew Salmon, 11-Jul-2011.)

Theoremiotassuni 4355 The class is a subset of the union of all elements satisfying . (Contributed by Mario Carneiro, 24-Dec-2016.)

Theoremiotaex 4356 Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.)

Theoremiota4 4357 Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.)

Theoremiota4an 4358 Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)

Theoremiota5 4359* A method for computing iota. (Contributed by NM, 17-Sep-2013.)

Theoremiotabidv 4360* Formula-building deduction rule for iota. (Contributed by NM, 20-Aug-2011.)

Theoremiotabii 4361 Formula-building deduction rule for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)

Theoremiotacl 4362 Membership law for descriptions.

This can useful for expanding an unbounded iota-based definition (see df-iota 4339). If you have a bounded iota-based definition, riotacl2 in set.mm may be useful.

(Contributed by Andrew Salmon, 1-Aug-2011.)

Theoremreiotacl2 4363 Membership law for descriptions. (Contributed by SF, 21-Aug-2011.)

Theoremreiotacl 4364* Membership law for descriptions. (Contributed by SF, 21-Aug-2011.)

Theoremiota2df 4365 A condition that allows us to represent "the unique element such that " with a class expression . (Contributed by NM, 30-Dec-2014.)

Theoremiota2d 4366* A condition that allows us to represent "the unique element such that " with a class expression . (Contributed by NM, 30-Dec-2014.)

Theoremiota2 4367* The unique element such that . (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)

Theoremreiota2 4368* A condition allowing us to represent "the unique element in such that " with a class expression . (Contributed by Scott Fenton, 7-Jan-2018.)

Theoremsniota 4369 A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.)

Theoremdfiota3 4370 The operation using the operator. (Contributed by Scott Fenton, 6-Oct-2017.)

Theoremcsbiotag 4371* Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.)

Theoremdfiota4 4372 Alternate definition of iota in terms of 1c. (Contributed by SF, 29-Jan-2015.)
1c

2.2.10  Finite cardinals

Syntaxcnnc 4373 Extend the definition of a class to include the set of finite cardinals.
Nn

Syntaxc0c 4374 Extend the definition of a class to include cardinal zero.
0c

Syntaxcplc 4375 Extend the definition of a class to include cardinal addition.

Syntaxcfin 4376 Extend the definition of a class to include the set of all finite sets.
Fin

Definitiondf-0c 4377 Define cardinal zero. (Contributed by SF, 12-Jan-2015.)
0c

Definitiondf-addc 4378* Define cardinal addition. Definition from [Rosser] p. 275. (Contributed by SF, 12-Jan-2015.)

Definitiondf-nnc 4379* Define the finite cardinals. Definition from [Rosser] p. 275. (Contributed by SF, 12-Jan-2015.)
Nn 0c 1c

Definitiondf-fin 4380 Define the set of all finite sets. Definition from [Rosser], p. 417. (Contributed by SF, 12-Jan-2015.)
Fin Nn

Theoremdfaddc2 4381 Alternate definition of cardinal addition to establish stratification. (Contributed by SF, 15-Jan-2015.)
Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 k

Theoremaddcexlem 4382 The expression at the heart of dfaddc2 4381 is a set. (Contributed by SF, 17-Jan-2015.)
Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1c

Theorem0cex 4392 Cardinal zero is a set. (Contributed by SF, 14-Jan-2015.)
0c

Theoremaddcexg 4393 The cardinal sum of two sets is a set. (Contributed by SF, 15-Jan-2015.)

Theoremaddcex 4394 The cardinal sum of two sets is a set. (Contributed by SF, 25-Jan-2015.)

Theoremdfnnc2 4395 Definition of the finite cardinals for existence theorem. (Contributed by SF, 14-Jan-2015.)
Nn 0c Sk Sk k SIk Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1ck1c

Theoremnncex 4396 The class of all finite cardinals is a set. (Contributed by SF, 14-Jan-2015.)
Nn

Theoremfinex 4397 The class of all finite sets is a set. (Contributed by SF, 19-Jan-2015.)
Fin

Theoremeladdc 4398* Membership in cardinal addition. Theorem X.1.1 of [Rosser] p. 275. (Contributed by SF, 16-Jan-2015.)

Theoremeladdci 4399 Inference form of membership in cardinal addition. (Contributed by SF, 26-Jan-2015.)

Theorem0nelsuc 4400 The empty class is not a member of a successor. (Contributed by SF, 14-Jan-2015.)
1c

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6337
 Copyright terms: Public domain < Previous  Next >