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 e. _V   &   |- B e. _V   =>   |- (A"kB) e. _V
Theorem	dfpw12 4302	Alternate expression for unit power classes. (Contributed by SF, 26-Jan-2015.)
|- ~P1 A = ( SIk (A X.k A)"k_V)
Theorem	pw1exg 4303	The unit power class preserves sethood. (Contributed by SF, 14-Jan-2015.)
|- (A e. V -> ~P1 A e. _V)
Theorem	pw1ex 4304	The unit power class preserves sethood. (Contributed by SF, 14-Jan-2015.)
|- A e. _V   =>   |- ~P1 A e. _V
Theorem	insklem 4305*	Lemma for ins2kexg 4306 and ins3kexg 4307. Equality for subsets of (~P1 1c X.k (_V X.k _V)). (Contributed by SF, 14-Jan-2015.)
|- A C_ (~P1 1c X.k (_V X.k _V))   &   |- B C_ (~P1 1c X.k (_V X.k _V))   =>   |- (A = B <-> A.xA.yA.z(<<{{x}}, <<y, z>>>> e. A <-> <<{{x}}, <<y, z>>>> e. B))
Theorem	ins2kexg 4306	Ins2k preserves sethood. (Contributed by SF, 14-Jan-2015.)
|- (A e. V -> Ins2k A e. _V)
Theorem	ins3kexg 4307	Ins3k preserves sethood. (Contributed by SF, 14-Jan-2015.)
|- (A e. V -> Ins3k A e. _V)
Theorem	ins2kex 4308	Ins2k preserves sethood. (Contributed by SF, 14-Jan-2015.)
|- A e. _V   =>   |- Ins2k A e. _V
Theorem	ins3kex 4309	Ins3k preserves sethood. (Contributed by SF, 14-Jan-2015.)
|- A e. _V   =>   |- Ins3k A e. _V
Theorem	cokexg 4310	The Kuratowski composition of two sets is a set. (Contributed by SF, 14-Jan-2015.)
|- ((A e. V /\ B e. W) -> (A o.k B) e. _V)
Theorem	cokex 4311	The Kuratowski composition of two sets is a set. (Contributed by SF, 14-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (A o.k B) e. _V
Theorem	imagekexg 4312	The Kuratowski image functor preserves sethood. (Contributed by SF, 14-Jan-2015.)
|- (A e. V -> ImagekA e. _V)
Theorem	imagekex 4313	The Kuratowski image functor preserves sethood. (Contributed by SF, 14-Jan-2015.)
|- A e. _V   =>   |- ImagekA e. _V
Theorem	dfidk2 4314	Definition of _I_kk in terms of Sk. (Contributed by SF, 14-Jan-2015.)
|- _I_kk = ( Sk i^i `'k Sk )
Theorem	idkex 4315	The Kuratowski identity relationship is a set. (Contributed by SF, 14-Jan-2015.)
|- _I_kk e. _V
Theorem	dfuni3 4316	Alternate definition of class union for existence proof. (Contributed by SF, 14-Jan-2015.)
|- U.A = ⋃1(`'k Sk "kA)
Theorem	uniexg 4317	The sum class of a set is a set. (Contributed by SF, 14-Jan-2015.)
|- (A e. V -> U.A e. _V)
Theorem	uniex 4318	The sum class of a set is a set. (Contributed by SF, 14-Jan-2015.)
|- A e. _V   =>   |- U.A e. _V
Theorem	dfint3 4319	Alternate definition of class intersection for the existence proof. (Contributed by SF, 14-Jan-2015.)
|- |^|A = ∼ ⋃1(`'k ∼ Sk "kA)
Theorem	intexg 4320	The intersection of a set is a set. (Contributed by SF, 14-Jan-2015.)
|- (A e. V -> |^|A e. _V)
Theorem	intex 4321	The intersection of a set is a set. (Contributed by SF, 14-Jan-2015.)
|- A e. _V   =>   |- |^|A e. _V
Theorem	setswith 4322*	Two ways to express the class of all sets that contain A. (Contributed by SF, 14-Jan-2015.)
|- {x | A e. x} = if(A e. _V, ( Sk "k{{A}}), (/))
Theorem	setswithex 4323*	The class of all sets that contain A exist. (Contributed by SF, 14-Jan-2015.)
|- {x | A e. x} e. _V
Theorem	ndisjrelk 4324	Membership in a particular Kuratowski relationship is equivalent to non-disjointedness. (Contributed by SF, 15-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<<A, B>> e. (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) <-> (A i^i B) =/= (/))
Theorem	abexv 4325*	When x does not occur in ph, {x | ph} is a set. (Contributed by SF, 17-Jan-2015.)
|- {x | ph} e. _V
Theorem	unipw1 4326	The union of a unit power class is the original set. (Contributed by SF, 20-Jan-2015.)
|- U.~P1 A = A
Theorem	pw1exb 4327	Biconditional existence for unit power class. (Contributed by SF, 20-Jan-2015.)
|- (~P1 A e. _V <-> A e. _V)
Theorem	dfpw2 4328	Definition of power set for existence proof. (Contributed by SF, 21-Jan-2015.)
|- ~PA = ∼ (( Sk \ (~P1 A X.k _V))"k1c)
Theorem	pwexg 4329	The power class of a set is a set. (Contributed by SF, 21-Jan-2015.)
|- (A e. V -> ~PA e. _V)
Theorem	pwex 4330	The power class of a set is a set. (Contributed by SF, 21-Jan-2015.)
|- A e. _V   =>   |- ~PA e. _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 C_ 1c -> A = ~P1 U.A)
Theorem	pw1equn 4332*	A condition for a unit power class to equal a union. (Contributed by SF, 26-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (~P1 C = (A u. B) <-> E.xE.y(C = (x u. y) /\ A = ~P1 x /\ B = ~P1 y))
Theorem	pw1eqadj 4333*	A condition for a unit power class to work out to an adjunction. (Contributed by SF, 26-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (~P1 C = (A u. {B}) <-> E.xE.y(C = (x u. {y}) /\ A = ~P1 x /\ B = {y}))
Theorem	dfeu2 4334	Alternate definition of existential uniqueness in terms of abstraction. (Contributed by SF, 29-Jan-2015.)
|- (E!xph <-> {x | ph} e. 1c)
Theorem	euabex 4335	If there is a unique object satisfying a property ph, then the set of all elements that satisfy ph exists. (Contributed by SF, 16-Jan-2015.)
|- (E!xph -> {x | ph} e. _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 e. _V   =>   |- (A C_ ~P1 B <-> E.x(x C_ B /\ A = ~P1 x))
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 e. _V   =>   |- (A C_ 1c <-> E.x A = ~P1 x)
2.2.9  Definite description binder (inverted iota)
Syntax	cio 4338	Extend class notation with Russell's definition description binder (inverted iota).
class (iotaxph)
Theorem	iotajust 4339*	Soundness justification theorem for df-iota 4340. (Contributed by Andrew Salmon, 29-Jun-2011.)
|- U.{y | {x | ph} = {y}} = U.{z | {x | ph} = {z}}
Definition	df-iota 4340*	Define Russell's definition description binder, which can be read as "the unique x such that ph," where ph ordinarily contains x as a free variable. Our definition is meaningful only when there is exactly one x such that ph is true (see iotaval 4351); otherwise, it evaluates to the empty set (see iotanul 4355). Russell used the inverted iota symbol iota to represent the binder. (Contributed by SF, 12-Jan-2015.)
|- (iotaxph) = U.{y | {x | ph} = {y}}
Theorem	dfiota2 4341*	Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- (iotaxph) = U.{y | A.x(ph <-> x = y)}
Theorem	nfiota1 4342	Bound-variable hypothesis builder for the iota class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_x(iotaxph)
Theorem	nfiotad 4343	Deduction version of nfiota 4344. (Contributed by NM, 18-Feb-2013.)
|- F/yph   &   |- (ph -> F/xps)   =>   |- (ph -> F/_x(iotayps))
Theorem	nfiota 4344	Bound-variable hypothesis builder for the iota class. (Contributed by NM, 23-Aug-2011.)
|- F/xph   =>   |- F/_x(iotayph)
Theorem	cbviota 4345	Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
|- (x = y -> (ph <-> ps))   &   |- F/yph   &   |- F/xps   =>   |- (iotaxph) = (iotayps)
Theorem	cbviotav 4346*	Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.)
|- (x = y -> (ph <-> ps))   =>   |- (iotaxph) = (iotayps)
Theorem	sb8iota 4347	Variable substitution in description binder. Compare sb8eu 2222. (Contributed by NM, 18-Mar-2013.)
|- F/yph   =>   |- (iotaxph) = (iotay[y / x]ph)
Theorem	iotaeq 4348	Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- (A.x x = y -> (iotaxph) = (iotayph))
Theorem	iotabi 4349	Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.)
|- (A.x(ph <-> ps) -> (iotaxph) = (iotaxps))
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.)
|- (A.x(ph <-> x = y) -> U.{x | ph} = 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.)
|- (A.x(ph <-> x = y) -> (iotaxph) = y)
Theorem	iotauni 4352	Equivalence between two different forms of iota. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- (E!xph -> (iotaxph) = U.{x | ph})
Theorem	iotaint 4353	Equivalence between two different forms of iota. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- (E!xph -> (iotaxph) = |^|{x | ph})
Theorem	iota1 4354	Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
|- (E!xph -> (ph <-> (iotaxph) = 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 ph. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- (-. E!xph -> (iotaxph) = (/))
Theorem	iotassuni 4356	The iota class is a subset of the union of all elements satisfying ph. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- (iotaxph) C_ U.{x | ph}
Theorem	iotaex 4357	Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the iota class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- (iotaxph) e. _V
Theorem	iota4 4358	Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- (E!xph -> [.(iotaxph) / x ].ph)
Theorem	iota4an 4359	Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
|- (E!x(ph /\ ps) -> [.(iotax(ph /\ ps)) / x ].ph)
Theorem	iota5 4360*	A method for computing iota. (Contributed by NM, 17-Sep-2013.)
|- ((ph /\ A e. V) -> (ps <-> x = A))   =>   |- ((ph /\ A e. V) -> (iotaxps) = A)
Theorem	iotabidv 4361*	Formula-building deduction rule for iota. (Contributed by NM, 20-Aug-2011.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> (iotaxps) = (iotaxch))
Theorem	iotabii 4362	Formula-building deduction rule for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- (ph <-> ps)   =>   |- (iotaxph) = (iotaxps)
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.)
|- (E!xph -> (iotaxph) e. {x | ph})
Theorem	reiotacl2 4364	Membership law for descriptions. (Contributed by SF, 21-Aug-2011.)
|- (E!x e. A ph -> (iotax(x e. A /\ ph)) e. {x e. A | ph})
Theorem	reiotacl 4365*	Membership law for descriptions. (Contributed by SF, 21-Aug-2011.)
|- (E!x e. A ph -> (iotax(x e. A /\ ph)) e. A)
Theorem	iota2df 4366	A condition that allows us to represent "the unique element such that ph " with a class expression A. (Contributed by NM, 30-Dec-2014.)
|- (ph -> B e. V)   &   |- (ph -> E!xps)   &   |- ((ph /\ x = B) -> (ps <-> ch))   &   |- F/xph   &   |- (ph -> F/xch)   &   |- (ph -> F/_xB)   =>   |- (ph -> (ch <-> (iotaxps) = B))
Theorem	iota2d 4367*	A condition that allows us to represent "the unique element such that ph " with a class expression A. (Contributed by NM, 30-Dec-2014.)
|- (ph -> B e. V)   &   |- (ph -> E!xps)   &   |- ((ph /\ x = B) -> (ps <-> ch))   =>   |- (ph -> (ch <-> (iotaxps) = B))
Theorem	iota2 4368*	The unique element such that ph. (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
|- (x = A -> (ph <-> ps))   =>   |- ((A e. B /\ E!xph) -> (ps <-> (iotaxph) = A))
Theorem	reiota2 4369*	A condition allowing us to represent "the unique element in A such that ph " with a class expression B. (Contributed by Scott Fenton, 7-Jan-2018.)
|- (x = B -> (ph <-> ps))   =>   |- ((B e. A /\ E!x e. A ph) -> (ps <-> (iotax(x e. A /\ ph)) = B))
Theorem	sniota 4370	A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- (E!xph -> {x | ph} = {(iotaxph)})
Theorem	dfiota3 4371	The iota operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017.)
|- (iotaxph) = if(E!xph, U.{x | ph}, (/))
Theorem	csbiotag 4372*	Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.)
|- (A e. V -> [_A / x]_(iotayph) = (iotay [.A / x ].ph))
Theorem	dfiota4 4373	Alternate definition of iota in terms of 1c. (Contributed by SF, 29-Jan-2015.)
|- (iotaxph) = U.U.(1c i^i {{x | ph}})
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 +o 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 +o B) = {x | E.y e. A E.z e. B ((y i^i z) = (/) /\ x = (y u. z))}
Definition	df-nnc 4380*	Define the finite cardinals. Definition from [Rosser] p. 275. (Contributed by SF, 12-Jan-2015.)
|- Nn = |^|{b | (0c e. b /\ A.y e. b (y +o 1c) e. b)}
Definition	df-fin 4381	Define the set of all finite sets. Definition from [Rosser], p. 417. (Contributed by SF, 12-Jan-2015.)
|- Fin = U. Nn
Theorem	dfaddc2 4382	Alternate definition of cardinal addition to establish stratification. (Contributed by SF, 15-Jan-2015.)
|- (A +o B) = ((( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 B)"kA)
Theorem	addcexlem 4383	The expression at the heart of dfaddc2 4382 is a set. (Contributed by SF, 17-Jan-2015.)
|- ( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c)) e. _V
Theorem	addceq1 4384	Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.)
|- (A = B -> (A +o C) = (B +o C))
Theorem	addceq2 4385	Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.)
|- (A = B -> (C +o A) = (C +o B))
Theorem	addceq12 4386	Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.)
|- ((A = C /\ B = D) -> (A +o B) = (C +o D))
Theorem	addceq1i 4387	Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.)
|- A = B   =>   |- (A +o C) = (B +o C)
Theorem	addceq2i 4388	Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.)
|- A = B   =>   |- (C +o A) = (C +o B)
Theorem	addceq12i 4389	Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.)
|- A = B   &   |- C = D   =>   |- (A +o C) = (B +o D)
Theorem	addceq1d 4390	Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.)
|- (ph -> A = B)   =>   |- (ph -> (A +o C) = (B +o C))
Theorem	addceq2d 4391	Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.)
|- (ph -> A = B)   =>   |- (ph -> (C +o A) = (C +o B))
Theorem	addceq12d 4392	Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A +o C) = (B +o D))
Theorem	0cex 4393	Cardinal zero is a set. (Contributed by SF, 14-Jan-2015.)
|- 0c e. _V
Theorem	addcexg 4394	The cardinal sum of two sets is a set. (Contributed by SF, 15-Jan-2015.)
|- ((A e. V /\ B e. W) -> (A +o B) e. _V)
Theorem	addcex 4395	The cardinal sum of two sets is a set. (Contributed by SF, 25-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (A +o B) e. _V
Theorem	dfnnc2 4396	Definition of the finite cardinals for existence theorem. (Contributed by SF, 14-Jan-2015.)
|- Nn = |^|({x | 0c e. x} \ (( Sk \ ( Sk o.k SIk Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c)))"k1c))
Theorem	nncex 4397	The class of all finite cardinals is a set. (Contributed by SF, 14-Jan-2015.)
|- Nn e. _V
Theorem	finex 4398	The class of all finite sets is a set. (Contributed by SF, 19-Jan-2015.)
|- Fin e. _V
Theorem	eladdc 4399*	Membership in cardinal addition. Theorem X.1.1 of [Rosser] p. 275. (Contributed by SF, 16-Jan-2015.)
|- (A e. (M +o N) <-> E.b e. M E.c e. N ((b i^i c) = (/) /\ A = (b u. c)))
Theorem	eladdci 4400	Inference form of membership in cardinal addition. (Contributed by SF, 26-Jan-2015.)
|- ((A e. M /\ B e. N /\ (A i^i B) = (/)) -> (A u. B) e. (M +o N))