P. 44 of Theorem List - New Foundations Explorer

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

Type	Label	Description
Statement
Theorem	imakex 4301	The image of a set under a set is a set. (Contributed by SF, 14-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A “k B) ∈ V
Theorem	dfpw12 4302	Alternate expression for unit power classes. (Contributed by SF, 26-Jan-2015.)
⊢ ℘1A = ( SIk (A ×k A) “k V)
Theorem	pw1exg 4303	The unit power class preserves sethood. (Contributed by SF, 14-Jan-2015.)
⊢ (A ∈ V → ℘1A ∈ V)
Theorem	pw1ex 4304	The unit power class preserves sethood. (Contributed by SF, 14-Jan-2015.)
⊢ A ∈ V    ⇒   ⊢ ℘1A ∈ V
Theorem	insklem 4305*	Lemma for ins2kexg 4306 and ins3kexg 4307. 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 = B ↔ ∀x∀y∀z(⟪{{x}}, ⟪y, z⟫⟫ ∈ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ ∈ B))
Theorem	ins2kexg 4306	Ins2k preserves sethood. (Contributed by SF, 14-Jan-2015.)
⊢ (A ∈ V → Ins2k A ∈ V)
Theorem	ins3kexg 4307	Ins3k preserves sethood. (Contributed by SF, 14-Jan-2015.)
⊢ (A ∈ V → Ins3k A ∈ V)
Theorem	ins2kex 4308	Ins2k preserves sethood. (Contributed by SF, 14-Jan-2015.)
⊢ A ∈ V    ⇒   ⊢ Ins2k A ∈ V
Theorem	ins3kex 4309	Ins3k preserves sethood. (Contributed by SF, 14-Jan-2015.)
⊢ A ∈ V    ⇒   ⊢ Ins3k A ∈ V
Theorem	cokexg 4310	The Kuratowski composition of two sets is a set. (Contributed by SF, 14-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A ∘k B) ∈ V)
Theorem	cokex 4311	The Kuratowski composition of two sets is a set. (Contributed by SF, 14-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A ∘k B) ∈ V
Theorem	imagekexg 4312	The Kuratowski image functor preserves sethood. (Contributed by SF, 14-Jan-2015.)
⊢ (A ∈ V → ImagekA ∈ V)
Theorem	imagekex 4313	The Kuratowski image functor preserves sethood. (Contributed by SF, 14-Jan-2015.)
⊢ A ∈ V    ⇒   ⊢ ImagekA ∈ V
Theorem	dfidk2 4314	Definition of Ik in terms of Sk. (Contributed by SF, 14-Jan-2015.)
⊢ Ik = ( Sk ∩ ◡k Sk )
Theorem	idkex 4315	The Kuratowski identity relationship is a set. (Contributed by SF, 14-Jan-2015.)
⊢ Ik ∈ V
Theorem	dfuni3 4316	Alternate definition of class union for existence proof. (Contributed by SF, 14-Jan-2015.)
⊢ ∪A = ⋃1(◡k Sk “k A)
Theorem	uniexg 4317	The sum class of a set is a set. (Contributed by SF, 14-Jan-2015.)
⊢ (A ∈ V → ∪A ∈ V)
Theorem	uniex 4318	The sum class of a set is a set. (Contributed by SF, 14-Jan-2015.)
⊢ A ∈ V    ⇒   ⊢ ∪A ∈ V
Theorem	dfint3 4319	Alternate definition of class intersection for the existence proof. (Contributed by SF, 14-Jan-2015.)
⊢ ∩A = ∼ ⋃1(◡k ∼ Sk “k A)
Theorem	intexg 4320	The intersection of a set is a set. (Contributed by SF, 14-Jan-2015.)
⊢ (A ∈ V → ∩A ∈ V)
Theorem	intex 4321	The intersection of a set is a set. (Contributed by SF, 14-Jan-2015.)
⊢ A ∈ V    ⇒   ⊢ ∩A ∈ V
Theorem	setswith 4322*	Two ways to express the class of all sets that contain A. (Contributed by SF, 14-Jan-2015.)
⊢ {x ∣ A ∈ x} = if(A ∈ V, ( Sk “k {{A}}), ∅)
Theorem	setswithex 4323*	The class of all sets that contain A exist. (Contributed by SF, 14-Jan-2015.)
⊢ {x ∣ A ∈ x} ∈ V
Theorem	ndisjrelk 4324	Membership in a particular Kuratowski relationship is equivalent to non-disjointedness. (Contributed by SF, 15-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (⟪A, B⟫ ∈ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ↔ (A ∩ B) ≠ ∅)
Theorem	abexv 4325*	When x does not occur in φ, {x ∣ φ} is a set. (Contributed by SF, 17-Jan-2015.)
⊢ {x ∣ φ} ∈ V
Theorem	unipw1 4326	The union of a unit power class is the original set. (Contributed by SF, 20-Jan-2015.)
⊢ ∪℘1A = A
Theorem	pw1exb 4327	Biconditional existence for unit power class. (Contributed by SF, 20-Jan-2015.)
⊢ (℘1A ∈ V ↔ A ∈ V)
Theorem	dfpw2 4328	Definition of power set for existence proof. (Contributed by SF, 21-Jan-2015.)
⊢ ℘A = ∼ (( Sk ∖ (℘1A ×k V)) “k 1c)
Theorem	pwexg 4329	The power class of a set is a set. (Contributed by SF, 21-Jan-2015.)
⊢ (A ∈ V → ℘A ∈ V)
Theorem	pwex 4330	The power class of a set is a set. (Contributed by SF, 21-Jan-2015.)
⊢ A ∈ V    ⇒   ⊢ ℘A ∈ V
Theorem	eqpw1uni 4331	A class of singletons is equal to the unit power class of its union. (Contributed by SF, 26-Jan-2015.)
⊢ (A ⊆ 1c → A = ℘1∪A)
Theorem	pw1equn 4332*	A condition for a unit power class to equal a union. (Contributed by SF, 26-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (℘1C = (A ∪ B) ↔ ∃x∃y(C = (x ∪ y) ∧ A = ℘1x ∧ B = ℘1y))
Theorem	pw1eqadj 4333*	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}) ↔ ∃x∃y(C = (x ∪ {y}) ∧ A = ℘1x ∧ B = {y}))
Theorem	dfeu2 4334	Alternate definition of existential uniqueness in terms of abstraction. (Contributed by SF, 29-Jan-2015.)
⊢ (∃!xφ ↔ {x ∣ φ} ∈ 1c)
Theorem	euabex 4335	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)
Theorem	sspw1 4336*	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 ⊆ ℘1B ↔ ∃x(x ⊆ B ∧ A = ℘1x))
Theorem	sspw12 4337*	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 ⊆ 1c ↔ ∃x A = ℘1x)
2.2.9  Definite description binder (inverted iota)
Syntax	cio 4338	Extend class notation with Russell's definition description binder (inverted iota).
class (℩xφ)
Theorem	iotajust 4339*	Soundness justification theorem for df-iota 4340. (Contributed by Andrew Salmon, 29-Jun-2011.)
⊢ ∪{y ∣ {x ∣ φ} = {y}} = ∪{z ∣ {x ∣ φ} = {z}}
Definition	df-iota 4340*	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 4351); otherwise, it evaluates to the empty set (see iotanul 4355). Russell used the inverted iota symbol ℩ to represent the binder. (Contributed by SF, 12-Jan-2015.)
⊢ (℩xφ) = ∪{y ∣ {x ∣ φ} = {y}}
Theorem	dfiota2 4341*	Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (℩xφ) = ∪{y ∣ ∀x(φ ↔ x = y)}
Theorem	nfiota1 4342	Bound-variable hypothesis builder for the ℩ class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎx(℩xφ)
Theorem	nfiotad 4343	Deduction version of nfiota 4344. (Contributed by NM, 18-Feb-2013.)
⊢ Ⅎyφ    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx(℩yψ))
Theorem	nfiota 4344	Bound-variable hypothesis builder for the ℩ class. (Contributed by NM, 23-Aug-2011.)
⊢ Ⅎxφ    ⇒   ⊢ Ⅎx(℩yφ)
Theorem	cbviota 4345	Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
⊢ (x = y → (φ ↔ ψ))    &   ⊢ Ⅎyφ    &   ⊢ Ⅎxψ    ⇒   ⊢ (℩xφ) = (℩yψ)
Theorem	cbviotav 4346*	Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (℩xφ) = (℩yψ)
Theorem	sb8iota 4347	Variable substitution in description binder. Compare sb8eu 2222. (Contributed by NM, 18-Mar-2013.)
⊢ Ⅎyφ    ⇒   ⊢ (℩xφ) = (℩y[y / x]φ)
Theorem	iotaeq 4348	Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (∀x x = y → (℩xφ) = (℩yφ))
Theorem	iotabi 4349	Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
⊢ (∀x(φ ↔ ψ) → (℩xφ) = (℩xψ))
Theorem	uniabio 4350*	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)
Theorem	iotaval 4351*	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)
Theorem	iotauni 4352	Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!xφ → (℩xφ) = ∪{x ∣ φ})
Theorem	iotaint 4353	Equivalence between two different forms of ℩. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (∃!xφ → (℩xφ) = ∩{x ∣ φ})
Theorem	iota1 4354	Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!xφ → (φ ↔ (℩xφ) = x))
Theorem	iotanul 4355	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φ) = ∅)
Theorem	iotassuni 4356	The ℩ class is a subset of the union of all elements satisfying φ. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (℩xφ) ⊆ ∪{x ∣ φ}
Theorem	iotaex 4357	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
Theorem	iota4 4358	Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!xφ → [̣(℩xφ) / x]̣φ)
Theorem	iota4an 4359	Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!x(φ ∧ ψ) → [̣(℩x(φ ∧ ψ)) / x]̣φ)
Theorem	iota5 4360*	A method for computing iota. (Contributed by NM, 17-Sep-2013.)
⊢ ((φ ∧ A ∈ V) → (ψ ↔ x = A))    ⇒   ⊢ ((φ ∧ A ∈ V) → (℩xψ) = A)
Theorem	iotabidv 4361*	Formula-building deduction rule for iota. (Contributed by NM, 20-Aug-2011.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (℩xψ) = (℩xχ))
Theorem	iotabii 4362	Formula-building deduction rule for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (℩xφ) = (℩xψ)
Theorem	iotacl 4363	Membership law for descriptions. This can useful for expanding an unbounded iota-based definition (see df-iota 4340). 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 ∣ φ})
Theorem	reiotacl2 4364	Membership law for descriptions. (Contributed by SF, 21-Aug-2011.)
⊢ (∃!x ∈ A φ → (℩x(x ∈ A ∧ φ)) ∈ {x ∈ A ∣ φ})
Theorem	reiotacl 4365*	Membership law for descriptions. (Contributed by SF, 21-Aug-2011.)
⊢ (∃!x ∈ A φ → (℩x(x ∈ A ∧ φ)) ∈ A)
Theorem	iota2df 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φ    &   ⊢ (φ → Ⅎxχ)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → (χ ↔ (℩xψ) = B))
Theorem	iota2d 4367*	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))
Theorem	iota2 4368*	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))
Theorem	reiota2 4369*	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))
Theorem	sniota 4370	A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ (∃!xφ → {x ∣ φ} = {(℩xφ)})
Theorem	dfiota3 4371	The ℩ operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017.)
⊢ (℩xφ) = if(∃!xφ, ∪{x ∣ φ}, ∅)
Theorem	csbiotag 4372*	Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.)
⊢ (A ∈ V → [A / x](℩yφ) = (℩y[̣A / x]̣φ))
Theorem	dfiota4 4373	Alternate definition of iota in terms of 1c. (Contributed by SF, 29-Jan-2015.)
⊢ (℩xφ) = ∪∪(1c ∩ {{x ∣ φ}})
2.2.10  Finite cardinals
Syntax	cnnc 4374	Extend the definition of a class to include the set of finite cardinals.
class Nn
Syntax	c0c 4375	Extend the definition of a class to include cardinal zero.
class 0c
Syntax	cplc 4376	Extend the definition of a class to include cardinal addition.
class (A +c B)
Syntax	cfin 4377	Extend the definition of a class to include the set of all finite sets.
class Fin
Definition	df-0c 4378	Define cardinal zero. (Contributed by SF, 12-Jan-2015.)
⊢ 0c = {∅}
Definition	df-addc 4379*	Define cardinal addition. Definition from [Rosser] p. 275. (Contributed by SF, 12-Jan-2015.)
⊢ (A +c B) = {x ∣ ∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z))}
Definition	df-nnc 4380*	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)}
Definition	df-fin 4381	Define the set of all finite sets. Definition from [Rosser], p. 417. (Contributed by SF, 12-Jan-2015.)
⊢ Fin = ∪ Nn
Theorem	dfaddc2 4382	Alternate definition of cardinal addition to establish stratification. (Contributed by SF, 15-Jan-2015.)
⊢ (A +c B) = ((( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘1B) “k A)
Theorem	addcexlem 4383	The expression at the heart of dfaddc2 4382 is a set. (Contributed by SF, 17-Jan-2015.)
⊢ ( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c)) ∈ V
Theorem	addceq1 4384	Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.)
⊢ (A = B → (A +c C) = (B +c C))
Theorem	addceq2 4385	Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.)
⊢ (A = B → (C +c A) = (C +c B))
Theorem	addceq12 4386	Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.)
⊢ ((A = C ∧ B = D) → (A +c B) = (C +c D))
Theorem	addceq1i 4387	Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.)
⊢ A = B    ⇒   ⊢ (A +c C) = (B +c C)
Theorem	addceq2i 4388	Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.)
⊢ A = B    ⇒   ⊢ (C +c A) = (C +c B)
Theorem	addceq12i 4389	Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.)
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (A +c C) = (B +c D)
Theorem	addceq1d 4390	Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A +c C) = (B +c C))
Theorem	addceq2d 4391	Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (C +c A) = (C +c B))
Theorem	addceq12d 4392	Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (A +c C) = (B +c D))
Theorem	0cex 4393	Cardinal zero is a set. (Contributed by SF, 14-Jan-2015.)
⊢ 0c ∈ V
Theorem	addcexg 4394	The cardinal sum of two sets is a set. (Contributed by SF, 15-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A +c B) ∈ V)
Theorem	addcex 4395	The cardinal sum of two sets is a set. (Contributed by SF, 25-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A +c B) ∈ V
Theorem	dfnnc2 4396	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 Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c))) “k 1c))
Theorem	nncex 4397	The class of all finite cardinals is a set. (Contributed by SF, 14-Jan-2015.)
⊢ Nn ∈ V
Theorem	finex 4398	The class of all finite sets is a set. (Contributed by SF, 19-Jan-2015.)
⊢ Fin ∈ V
Theorem	eladdc 4399*	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 ((b ∩ c) = ∅ ∧ A = (b ∪ c)))
Theorem	eladdci 4400	Inference form of membership in cardinal addition. (Contributed by SF, 26-Jan-2015.)
⊢ ((A ∈ M ∧ B ∈ N ∧ (A ∩ B) = ∅) → (A ∪ B) ∈ (M +c N))