Home | New
Foundations Explorer Theorem 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 |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfpw12 4301 | Alternate expression for unit power classes. (Contributed by SF, 26-Jan-2015.) |
_{1} SI_{k} _{k} _{k} | ||
Theorem | pw1exg 4302 | The unit power class preserves sethood. (Contributed by SF, 14-Jan-2015.) |
_{1} | ||
Theorem | pw1ex 4303 | The unit power class preserves sethood. (Contributed by SF, 14-Jan-2015.) |
_{1} | ||
Theorem | insklem 4304* | Lemma for ins2kexg 4305 and ins3kexg 4306. Equality for subsets of _{1} 1_{c} _{k} _{k} . (Contributed by SF, 14-Jan-2015.) |
_{1} 1_{c} _{k} _{k} _{1} 1_{c} _{k} _{k} | ||
Theorem | ins2kexg 4305 | Ins2_{k} preserves sethood. (Contributed by SF, 14-Jan-2015.) |
Ins2_{k} | ||
Theorem | ins3kexg 4306 | Ins3_{k} preserves sethood. (Contributed by SF, 14-Jan-2015.) |
Ins3_{k} | ||
Theorem | ins2kex 4307 | Ins2_{k} preserves sethood. (Contributed by SF, 14-Jan-2015.) |
Ins2_{k} | ||
Theorem | ins3kex 4308 | Ins3_{k} preserves sethood. (Contributed by SF, 14-Jan-2015.) |
Ins3_{k} | ||
Theorem | cokexg 4309 | The Kuratowski composition of two sets is a set. (Contributed by SF, 14-Jan-2015.) |
_{k} | ||
Theorem | cokex 4310 | The Kuratowski composition of two sets is a set. (Contributed by SF, 14-Jan-2015.) |
_{k} | ||
Theorem | imagekexg 4311 | The Kuratowski image functor preserves sethood. (Contributed by SF, 14-Jan-2015.) |
Image_{k} | ||
Theorem | imagekex 4312 | The Kuratowski image functor preserves sethood. (Contributed by SF, 14-Jan-2015.) |
Image_{k} | ||
Theorem | dfidk2 4313 | Definition of _{k} in terms of S_{k}. (Contributed by SF, 14-Jan-2015.) |
_{k} S_{k} _{k} S_{k} | ||
Theorem | idkex 4314 | The Kuratowski identity relationship is a set. (Contributed by SF, 14-Jan-2015.) |
_{k} | ||
Theorem | dfuni3 4315 | Alternate definition of class union for existence proof. (Contributed by SF, 14-Jan-2015.) |
⋃_{1}_{k} S_{k} _{k} | ||
Theorem | uniexg 4316 | The sum class of a set is a set. (Contributed by SF, 14-Jan-2015.) |
Theorem | uniex 4317 | The sum class of a set is a set. (Contributed by SF, 14-Jan-2015.) |
Theorem | dfint3 4318 | Alternate definition of class intersection for the existence proof. (Contributed by SF, 14-Jan-2015.) |
∼ ⋃_{1}_{k} ∼ S_{k} _{k} | ||
Theorem | intexg 4319 | The intersection of a set is a set. (Contributed by SF, 14-Jan-2015.) |
Theorem | intex 4320 | The intersection of a set is a set. (Contributed by SF, 14-Jan-2015.) |
Theorem | setswith 4321* | Two ways to express the class of all sets that contain . (Contributed by SF, 14-Jan-2015.) |
S_{k} _{k} | ||
Theorem | setswithex 4322* | The class of all sets that contain exist. (Contributed by SF, 14-Jan-2015.) |
Theorem | ndisjrelk 4323 | Membership in a particular Kuratowski relationship is equivalent to non-disjointedness. (Contributed by SF, 15-Jan-2015.) |
Ins3_{k} S_{k} Ins2_{k} S_{k} _{k}_{1} _{1} 1_{c} | ||
Theorem | abexv 4324* | When does not occur in , is a set. (Contributed by SF, 17-Jan-2015.) |
Theorem | unipw1 4325 | The union of a unit power class is the original set. (Contributed by SF, 20-Jan-2015.) |
_{1} | ||
Theorem | pw1exb 4326 | Biconditional existence for unit power class. (Contributed by SF, 20-Jan-2015.) |
_{1} | ||
Theorem | dfpw2 4327 | Definition of power set for existence proof. (Contributed by SF, 21-Jan-2015.) |
∼ S_{k} _{1} _{k} _{k}1_{c} | ||
Theorem | pwexg 4328 | The power class of a set is a set. (Contributed by SF, 21-Jan-2015.) |
Theorem | pwex 4329 | The power class of a set is a set. (Contributed by SF, 21-Jan-2015.) |
Theorem | eqpw1uni 4330 | A class of singletons is equal to the unit power class of its union. (Contributed by SF, 26-Jan-2015.) |
1_{c} _{1} | ||
Theorem | pw1equn 4331* | A condition for a unit power class to equal a union. (Contributed by SF, 26-Jan-2015.) |
_{1} _{1} _{1} | ||
Theorem | pw1eqadj 4332* | A condition for a unit power class to work out to an adjunction. (Contributed by SF, 26-Jan-2015.) |
_{1} _{1} | ||
Theorem | dfeu2 4333 | Alternate definition of existential uniqueness in terms of abstraction. (Contributed by SF, 29-Jan-2015.) |
1_{c} | ||
Theorem | euabex 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.) |
Theorem | sspw1 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} | ||
Theorem | sspw12 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.) |
1_{c} _{1} | ||
Syntax | cio 4337 | Extend class notation with Russell's definition description binder (inverted iota). |
Theorem | iotajust 4338* | Soundness justification theorem for df-iota 4339. (Contributed by Andrew Salmon, 29-Jun-2011.) |
Definition | df-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.) |
Theorem | dfiota2 4340* | Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.) |
Theorem | nfiota1 4341 | Bound-variable hypothesis builder for the class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | nfiotad 4342 | Deduction version of nfiota 4343. (Contributed by NM, 18-Feb-2013.) |
Theorem | nfiota 4343 | Bound-variable hypothesis builder for the class. (Contributed by NM, 23-Aug-2011.) |
Theorem | cbviota 4344 | Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.) |
Theorem | cbviotav 4345* | Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.) |
Theorem | sb8iota 4346 | Variable substitution in description binder. Compare sb8eu 2222. (Contributed by NM, 18-Mar-2013.) |
Theorem | iotaeq 4347 | Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.) |
Theorem | iotabi 4348 | Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.) |
Theorem | uniabio 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.) |
Theorem | iotaval 4350* | Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.) |
Theorem | iotauni 4351 | Equivalence between two different forms of . (Contributed by Andrew Salmon, 12-Jul-2011.) |
Theorem | iotaint 4352 | Equivalence between two different forms of . (Contributed by Mario Carneiro, 24-Dec-2016.) |
Theorem | iota1 4353 | Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
Theorem | iotanul 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.) |
Theorem | iotassuni 4355 | The class is a subset of the union of all elements satisfying . (Contributed by Mario Carneiro, 24-Dec-2016.) |
Theorem | iotaex 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.) |
Theorem | iota4 4357 | Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.) |
Theorem | iota4an 4358 | Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.) |
Theorem | iota5 4359* | A method for computing iota. (Contributed by NM, 17-Sep-2013.) |
Theorem | iotabidv 4360* | Formula-building deduction rule for iota. (Contributed by NM, 20-Aug-2011.) |
Theorem | iotabii 4361 | Formula-building deduction rule for iota. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Theorem | iotacl 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.) |
Theorem | reiotacl2 4363 | Membership law for descriptions. (Contributed by SF, 21-Aug-2011.) |
Theorem | reiotacl 4364* | Membership law for descriptions. (Contributed by SF, 21-Aug-2011.) |
Theorem | iota2df 4365 | A condition that allows us to represent "the unique element such that " with a class expression . (Contributed by NM, 30-Dec-2014.) |
Theorem | iota2d 4366* | A condition that allows us to represent "the unique element such that " with a class expression . (Contributed by NM, 30-Dec-2014.) |
Theorem | iota2 4367* | The unique element such that . (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
Theorem | reiota2 4368* | A condition allowing us to represent "the unique element in such that " with a class expression . (Contributed by Scott Fenton, 7-Jan-2018.) |
Theorem | sniota 4369 | A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.) |
Theorem | dfiota3 4370 | The operation using the operator. (Contributed by Scott Fenton, 6-Oct-2017.) |
Theorem | csbiotag 4371* | Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.) |
Theorem | dfiota4 4372 | Alternate definition of iota in terms of 1_{c}. (Contributed by SF, 29-Jan-2015.) |
1_{c} | ||
Syntax | cnnc 4373 | Extend the definition of a class to include the set of finite cardinals. |
Nn | ||
Syntax | c0c 4374 | Extend the definition of a class to include cardinal zero. |
0_{c} | ||
Syntax | cplc 4375 | Extend the definition of a class to include cardinal addition. |
Syntax | cfin 4376 | Extend the definition of a class to include the set of all finite sets. |
Fin | ||
Definition | df-0c 4377 | Define cardinal zero. (Contributed by SF, 12-Jan-2015.) |
0_{c} | ||
Definition | df-addc 4378* | Define cardinal addition. Definition from [Rosser] p. 275. (Contributed by SF, 12-Jan-2015.) |
Definition | df-nnc 4379* | Define the finite cardinals. Definition from [Rosser] p. 275. (Contributed by SF, 12-Jan-2015.) |
Nn 0_{c} 1_{c} | ||
Definition | df-fin 4380 | Define the set of all finite sets. Definition from [Rosser], p. 417. (Contributed by SF, 12-Jan-2015.) |
Fin Nn | ||
Theorem | dfaddc2 4381 | Alternate definition of cardinal addition to establish stratification. (Contributed by SF, 15-Jan-2015.) |
Ins3_{k} ∼ Ins3_{k} S_{k} Ins2_{k} S_{k} _{k}_{1} _{1} 1_{c} Ins2_{k} Ins2_{k} S_{k} Ins2_{k} Ins3_{k} S_{k} Ins3_{k} SI_{k} SI_{k} S_{k} _{k}_{1} _{1} _{1} _{1} 1_{c}_{k}_{1} _{1} _{k} | ||
Theorem | addcexlem 4382 | The expression at the heart of dfaddc2 4381 is a set. (Contributed by SF, 17-Jan-2015.) |
Ins3_{k} ∼ Ins3_{k} S_{k} Ins2_{k} S_{k} _{k}_{1} _{1} 1_{c} Ins2_{k} Ins2_{k} S_{k} Ins2_{k} Ins3_{k} S_{k} Ins3_{k} SI_{k} SI_{k} S_{k} _{k}_{1} _{1} _{1} _{1} 1_{c} | ||
Theorem | addceq1 4383 | Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.) |
Theorem | addceq2 4384 | Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.) |
Theorem | addceq12 4385 | Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.) |
Theorem | addceq1i 4386 | Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.) |
Theorem | addceq2i 4387 | Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.) |
Theorem | addceq12i 4388 | Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.) |
Theorem | addceq1d 4389 | Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.) |
Theorem | addceq2d 4390 | Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.) |
Theorem | addceq12d 4391 | Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.) |
Theorem | 0cex 4392 | Cardinal zero is a set. (Contributed by SF, 14-Jan-2015.) |
0_{c} | ||
Theorem | addcexg 4393 | The cardinal sum of two sets is a set. (Contributed by SF, 15-Jan-2015.) |
Theorem | addcex 4394 | The cardinal sum of two sets is a set. (Contributed by SF, 25-Jan-2015.) |
Theorem | dfnnc2 4395 | Definition of the finite cardinals for existence theorem. (Contributed by SF, 14-Jan-2015.) |
Nn 0_{c} S_{k} S_{k} _{k} SI_{k} Image_{k} Ins3_{k} ∼ Ins3_{k} S_{k} Ins2_{k} S_{k} _{k}_{1} _{1} 1_{c} Ins2_{k} Ins2_{k} S_{k} Ins2_{k} Ins3_{k} S_{k} Ins3_{k} SI_{k} SI_{k} S_{k} _{k}_{1} _{1} _{1} _{1} 1_{c}_{k}_{1} _{1} 1_{c}_{k}1_{c} | ||
Theorem | nncex 4396 | The class of all finite cardinals is a set. (Contributed by SF, 14-Jan-2015.) |
Nn | ||
Theorem | finex 4397 | The class of all finite sets is a set. (Contributed by SF, 19-Jan-2015.) |
Fin | ||
Theorem | eladdc 4398* | Membership in cardinal addition. Theorem X.1.1 of [Rosser] p. 275. (Contributed by SF, 16-Jan-2015.) |
Theorem | eladdci 4399 | Inference form of membership in cardinal addition. (Contributed by SF, 26-Jan-2015.) |
Theorem | 0nelsuc 4400 | The empty class is not a member of a successor. (Contributed by SF, 14-Jan-2015.) |
1_{c} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |