 Home New Foundations ExplorerTheorem List (p. 44 of 64) < Previous  Next > Bad symbols? Try the GIF 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.)
1A = ( SIk (A ×k A) “k V)

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

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

Theoreminsklem 4304* Lemma for ins2kexg 4305 and ins3kexg 4306. Equality for subsets of (11c ×k (V ×k V)). (Contributed by SF, 14-Jan-2015.)
A (11c ×k (V ×k V))    &   B (11c ×k (V ×k V))       (A = Bxyz(⟪{{x}}, ⟪y, z⟫⟫ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ B))

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

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

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

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

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

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

Theoremimagekexg 4311 The Kuratowski image functor preserves sethood. (Contributed by SF, 14-Jan-2015.)
(A V → ImagekA V)

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

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

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

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

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

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

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

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

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

Theoremsetswith 4321* Two ways to express the class of all sets that contain A. (Contributed by SF, 14-Jan-2015.)
{x A x} = if(A V, ( Skk {{A}}), )

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

Theoremndisjrelk 4323 Membership in a particular Kuratowski relationship is equivalent to non-disjointedness. (Contributed by SF, 15-Jan-2015.)
A V    &   B V       (⟪A, B (( Ins3k SkIns2k Sk ) “k 111c) ↔ (AB) ≠ )

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

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

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

Theoremdfpw2 4327 Definition of power set for existence proof. (Contributed by SF, 21-Jan-2015.)
A = ∼ (( Sk (1A ×k V)) “k 1c)

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

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

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

Theorempw1equn 4331* A condition for a unit power class to equal a union. (Contributed by SF, 26-Jan-2015.)
A V    &   B V       (1C = (AB) ↔ xy(C = (xy) A = 1x B = 1y))

Theorempw1eqadj 4332* A condition for a unit power class to work out to an adjunction. (Contributed by SF, 26-Jan-2015.)
A V    &   B V       (1C = (A ∪ {B}) ↔ xy(C = (x ∪ {y}) A = 1x B = {y}))

Theoremdfeu2 4333 Alternate definition of existential uniqueness in terms of abstraction. (Contributed by SF, 29-Jan-2015.)
(∃!xφ ↔ {x φ} 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.)
(∃!xφ → {x φ} V)

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.)
A V       (A 1Bx(x B A = 1x))

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.)
A V       (A 1cx A = 1x)

2.2.9  Definite description binder (inverted iota)

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

Theoremiotajust 4338* Soundness justification theorem for df-iota 4339. (Contributed by Andrew Salmon, 29-Jun-2011.)
{y {x φ} = {y}} = {z {x φ} = {z}}

Definitiondf-iota 4339* Define Russell's definition description binder, which can be read as "the unique x such that φ," where φ ordinarily contains x as a free variable. Our definition is meaningful only when there is exactly one x 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.)
(℩xφ) = {y {x φ} = {y}}

Theoremdfiota2 4340* Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.)
(℩xφ) = {y x(φx = y)}

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

Theoremnfiotad 4342 Deduction version of nfiota 4343. (Contributed by NM, 18-Feb-2013.)
yφ    &   (φ → Ⅎxψ)       (φx(℩yψ))

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

Theoremcbviota 4344 Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
(x = y → (φψ))    &   yφ    &   xψ       (℩xφ) = (℩yψ)

Theoremcbviotav 4345* Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
(x = y → (φψ))       (℩xφ) = (℩yψ)

Theoremsb8iota 4346 Variable substitution in description binder. Compare sb8eu 2222. (Contributed by NM, 18-Mar-2013.)
yφ       (℩xφ) = (℩y[y / x]φ)

Theoremiotaeq 4347 Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
(x x = y → (℩xφ) = (℩yφ))

Theoremiotabi 4348 Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
(x(φψ) → (℩xφ) = (℩xψ))

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.)
(x(φx = y) → {x φ} = y)

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

Theoremiotauni 4351 Equivalence between two different forms of . (Contributed by Andrew Salmon, 12-Jul-2011.)
(∃!xφ → (℩xφ) = {x φ})

Theoremiotaint 4352 Equivalence between two different forms of . (Contributed by Mario Carneiro, 24-Dec-2016.)
(∃!xφ → (℩xφ) = {x φ})

Theoremiota1 4353 Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
(∃!xφ → (φ ↔ (℩xφ) = x))

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

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

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.)
(℩xφ) V

Theoremiota4 4357 Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.)
(∃!xφ → [̣(℩xφ) / xφ)

Theoremiota4an 4358 Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
(∃!x(φ ψ) → [̣(℩x(φ ψ)) / xφ)

Theoremiota5 4359* A method for computing iota. (Contributed by NM, 17-Sep-2013.)
((φ A V) → (ψx = A))       ((φ A V) → (℩xψ) = A)

Theoremiotabidv 4360* Formula-building deduction rule for iota. (Contributed by NM, 20-Aug-2011.)
(φ → (ψχ))       (φ → (℩xψ) = (℩xχ))

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

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.)

(∃!xφ → (℩xφ) {x φ})

Theoremreiotacl2 4363 Membership law for descriptions. (Contributed by SF, 21-Aug-2011.)
(∃!x A φ → (℩x(x A φ)) {x A φ})

Theoremreiotacl 4364* Membership law for descriptions. (Contributed by SF, 21-Aug-2011.)
(∃!x A φ → (℩x(x A φ)) A)

Theoremiota2df 4365 A condition that allows us to represent "the unique element such that φ " with a class expression A. (Contributed by NM, 30-Dec-2014.)
(φB V)    &   (φ∃!xψ)    &   ((φ x = B) → (ψχ))    &   xφ    &   (φ → Ⅎxχ)    &   (φxB)       (φ → (χ ↔ (℩xψ) = B))

Theoremiota2d 4366* A condition that allows us to represent "the unique element such that φ " with a class expression A. (Contributed by NM, 30-Dec-2014.)
(φB V)    &   (φ∃!xψ)    &   ((φ x = B) → (ψχ))       (φ → (χ ↔ (℩xψ) = B))

Theoremiota2 4367* The unique element such that φ. (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
(x = A → (φψ))       ((A B ∃!xφ) → (ψ ↔ (℩xφ) = A))

Theoremreiota2 4368* A condition allowing us to represent "the unique element in A such that φ " with a class expression B. (Contributed by Scott Fenton, 7-Jan-2018.)
(x = B → (φψ))       ((B A ∃!x A φ) → (ψ ↔ (℩x(x A φ)) = B))

Theoremsniota 4369 A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.)
(∃!xφ → {x φ} = {(℩xφ)})

Theoremdfiota3 4370 The operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017.)
(℩xφ) = if(∃!xφ, {x φ}, )

Theoremcsbiotag 4371* Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.)
(A V[A / x](℩yφ) = (℩yA / xφ))

Theoremdfiota4 4372 Alternate definition of iota in terms of 1c. (Contributed by SF, 29-Jan-2015.)
(℩xφ) = (1c ∩ {{x φ}})

2.2.10  Finite cardinals

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

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

Syntaxcplc 4375 Extend the definition of a class to include cardinal addition.
class (A +c B)

Syntaxcfin 4376 Extend the definition of a class to include the set of all finite sets.
class 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.)
(A +c B) = {x y A z B ((yz) = x = (yz))}

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

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.)
(A +c B) = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 11B) “k A)

Theoremaddcexlem 4382 The expression at the heart of dfaddc2 4381 is a set. (Contributed by SF, 17-Jan-2015.)
( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) V

(A = B → (A +c C) = (B +c C))

(A = B → (C +c A) = (C +c B))

((A = C B = D) → (A +c B) = (C +c D))

A = B       (A +c C) = (B +c C)

A = B       (C +c A) = (C +c B)

A = B    &   C = D       (A +c C) = (B +c D)

(φA = B)       (φ → (A +c C) = (B +c C))

(φA = B)       (φ → (C +c A) = (C +c B))

(φA = B)    &   (φC = D)       (φ → (A +c C) = (B +c D))

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

Theoremaddcexg 4393 The cardinal sum of two sets is a set. (Contributed by SF, 15-Jan-2015.)
((A V B W) → (A +c B) V)

Theoremaddcex 4394 The cardinal sum of two sets is a set. (Contributed by SF, 25-Jan-2015.)
A V    &   B V       (A +c B) V

Theoremdfnnc2 4395 Definition of the finite cardinals for existence theorem. (Contributed by SF, 14-Jan-2015.)
Nn = ({x 0c x} (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c))

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

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

Theoremeladdc 4398* Membership in cardinal addition. Theorem X.1.1 of [Rosser] p. 275. (Contributed by SF, 16-Jan-2015.)
(A (M +c N) ↔ b M c N ((bc) = A = (bc)))

Theoremeladdci 4399 Inference form of membership in cardinal addition. (Contributed by SF, 26-Jan-2015.)
((A M B N (AB) = ) → (AB) (M +c N))

Theorem0nelsuc 4400 The empty class is not a member of a successor. (Contributed by SF, 14-Jan-2015.)
¬ (A +c 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 >