P. 42 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 4101-4200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	unexg 4101	The union of two sets is a set. (Contributed by SF, 12-Jan-2015.)
|- ((A e. V /\ B e. W) -> (A u. B) e. _V)
Theorem	difexg 4102	The difference of two sets is a set. (Contributed by SF, 12-Jan-2015.)
|- ((A e. V /\ B e. W) -> (A \ B) e. _V)
Theorem	symdifexg 4103	The symmetric difference of two sets is a set. (Contributed by SF, 12-Jan-2015.)
|- ((A e. V /\ B e. W) -> (A (+) B) e. _V)
Theorem	complex 4104	The complement of a set is a set. (Contributed by SF, 12-Jan-2015.)
|- A e. _V   =>   |- ∼ A e. _V
Theorem	inex 4105	The intersection of two sets is a set. (Contributed by SF, 12-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (A i^i B) e. _V
Theorem	unex 4106	The union of two sets is a set. (Contributed by SF, 12-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (A u. B) e. _V
Theorem	difex 4107	The difference of two sets is a set. (Contributed by SF, 12-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (A \ B) e. _V
Theorem	symdifex 4108	The symmetric difference of two sets is a set. (Contributed by SF, 12-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (A (+) B) e. _V
Theorem	vvex 4109	The universal class exists. This marks a major departure from ZFC set theory, where _V is a proper class. (Contributed by SF, 12-Jan-2015.)
|- _V e. _V
Theorem	0ex 4110	The empty class exists. (Contributed by SF, 12-Jan-2015.)
|- (/) e. _V
Theorem	snex 4111	A singleton always exists. (Contributed by SF, 12-Jan-2015.)
|- {A} e. _V
Theorem	prex 4112	An unordered pair exists. (Contributed by SF, 12-Jan-2015.)
|- {A, B} e. _V
Theorem	opkex 4113	A Kuratowski ordered pair exists. (Contributed by SF, 12-Jan-2015.)
|- <<A, B>> e. _V
Theorem	snelpwg 4114	A singleton of a set belongs to a power class of a set containing it. (Contributed by SF, 1-Feb-2015.)
|- (A e. V -> ({A} e. ~PB <-> A e. B))
Theorem	snelpw 4115	A singleton of a set belongs to a power class of a set containing it. (Contributed by SF, 1-Feb-2015.)
|- A e. _V   =>   |- ({A} e. ~PB <-> A e. B)
Theorem	snelpwi 4116	A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.)
|- (A e. B -> {A} e. ~PB)
Theorem	unipw 4117	A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38. (The proof was shortened by Alan Sare, 28-Dec-2008.) (Contributed by SF, 14-Oct-1996.) (Revised by SF, 29-Dec-2008.)
|- U.~PA = A
Theorem	sspwb 4118	Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by SF, 13-Oct-1996.)
|- (A C_ B <-> ~PA C_ ~PB)
Theorem	pwadjoin 4119*	Compute the power class of an adjoinment. (Contributed by SF, 30-Jan-2015.)
|- ~P(A u. {X}) = (~PA u. {a | E.b e. ~P Aa = (b u. {X})})
2.2.4  Singletons and pairs (continued)
Theorem	snprss1 4120	A singleton is a subset of an unordered pair. (Contributed by SF, 12-Jan-2015.)
|- {A} C_ {A, B}
Theorem	snprss2 4121	A singleton is a subset of an unordered pair. (Contributed by SF, 12-Jan-2015.)
|- {A} C_ {B, A}
Theorem	prprc2 4122	An unordered pair of a proper class. (Contributed by SF, 12-Jan-2015.)
|- (-. A e. _V -> {B, A} = {B})
Theorem	prprc1 4123	An unordered pair of a proper class. (Contributed by SF, 12-Jan-2015.)
|- (-. A e. _V -> {A, B} = {B})
Theorem	preqr1 4124	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. (Contributed by NM, 18-Oct-1995.)
|- A e. _V   &   |- B e. _V   =>   |- ({A, C} = {B, C} -> A = B)
Theorem	preqr2 4125	Reverse equality lemma for unordered pairs. If two unordered pairs have the same first element, the second elements are equal. (Contributed by NM, 5-Aug-1993.)
|- A e. _V   &   |- B e. _V   =>   |- ({C, A} = {C, B} -> A = B)
Theorem	preqr2g 4126	Reverse equality lemma for unordered pairs. If two unordered pairs have the same first element, the second elements are equal. (Contributed by SF, 12-Jan-2015.)
|- ((A e. V /\ B e. W) -> ({C, A} = {C, B} -> A = B))
Theorem	preq12b 4127	Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- D e. _V   =>   |- ({A, B} = {C, D} <-> ((A = C /\ B = D) \/ (A = D /\ B = C)))
Theorem	preq12bg 4128	Closed form of preq12b 4127. (Contributed by Scott Fenton, 28-Mar-2014.)
|- (((A e. V /\ B e. W) /\ (C e. X /\ D e. Y)) -> ({A, B} = {C, D} <-> ((A = C /\ B = D) \/ (A = D /\ B = C))))
2.2.5  Kuratowski ordered pairs (continued)
Theorem	elopk 4129	Membership in a Kuratowski ordered pair. (Contributed by SF, 12-Jan-2015.)
|- (A e. <<B, C>> <-> (A = {B} \/ A = {B, C}))
Theorem	opkth1g 4130	Equality of the first member of a Kuratowski ordered pair, which holds regardless of the sethood of the second members. (Contributed by SF, 12-Jan-2015.)
|- ((A e. V /\ <<A, B>> = <<C, D>>) -> A = C)
Theorem	opkthg 4131	Two Kuratowski ordered pairs are equal iff their components are equal. (Contributed by SF, 12-Jan-2015.)
|- ((A e. V /\ B e. W /\ D e. T) -> (<<A, B>> = <<C, D>> <-> (A = C /\ B = D)))
Theorem	opkth 4132	Two Kuratowski ordered pairs are equal iff their components are equal. (Contributed by SF, 12-Jan-2015.)
|- A e. _V   &   |- B e. _V   &   |- D e. _V   =>   |- (<<A, B>> = <<C, D>> <-> (A = C /\ B = D))
2.2.6  Cardinal one, unit unions, and unit power classes
Syntax	cuni1 4133	Extend class notation to include the unit union of a class (read: 'unit union A')
class ⋃1A
Syntax	c1c 4134	Extend the definition of a class to include cardinal one.
class 1c
Syntax	cpw1 4135	Extend class notation to include unit power class.
class ~P1 A
Definition	df-1c 4136*	Define cardinal one. This is the set of all singletons, or the set of all sets of size one. (Contributed by SF, 12-Jan-2015.)
|- 1c = {x | E.y x = {y}}
Definition	df-pw1 4137	Define unit power class. Definition from [Rosser] p. 252. (Contributed by SF, 12-Jan-2015.)
|- ~P1 A = (~PA i^i 1c)
Definition	df-uni1 4138	Define the unit union of a class. This operation is used implicitly in both Holmes and Hailperin to complete their stratification algorithms, although neither provide explicit notation for it. See eluni1 4173 for membership condition. (Contributed by SF, 12-Jan-2015.)
|- ⋃1A = U.(A i^i 1c)
Theorem	el1c 4139*	Membership in cardinal one. (Contributed by SF, 12-Jan-2015.)
|- (A e. 1c <-> E.x A = {x})
Theorem	snel1c 4140	A singleton is an element of cardinal one. (Contributed by SF, 13-Jan-2015.)
|- A e. _V   =>   |- {A} e. 1c
Theorem	snel1cg 4141	A singleton is an element of cardinal one. (Contributed by SF, 30-Jan-2015.)
|- (A e. V -> {A} e. 1c)
Theorem	1cex 4142	Cardinal one is a set. (Contributed by SF, 12-Jan-2015.)
|- 1c e. _V
Theorem	pw1eq 4143	Equality theorem for unit power class. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> ~P1 A = ~P1 B)
Theorem	elpw1 4144*	Membership in a unit power class. (Contributed by SF, 13-Jan-2015.)
|- (A e. ~P1 B <-> E.x e. B A = {x})
Theorem	elpw12 4145*	Membership in a unit power class applied twice. (Contributed by SF, 15-Jan-2015.)
|- (A e. ~P1 ~P1 B <-> E.x e. B A = {{x}})
Theorem	snelpw1 4146	Membership of a singleton in a unit power class. (Contributed by SF, 13-Jan-2015.)
|- ({A} e. ~P1 B <-> A e. B)
Theorem	elpw11c 4147*	Membership in ~P1 1c. (Contributed by SF, 13-Jan-2015.)
|- (A e. ~P1 1c <-> E.x A = {{x}})
Theorem	elpw121c 4148*	Membership in ~P1 ~P1 1c. (Contributed by SF, 13-Jan-2015.)
|- (A e. ~P1 ~P1 1c <-> E.x A = {{{x}}})
Theorem	elpw131c 4149*	Membership in ~P1 ~P1 ~P1 1c. (Contributed by SF, 14-Jan-2015.)
|- (A e. ~P1 ~P1 ~P1 1c <-> E.x A = {{{{x}}}})
Theorem	elpw141c 4150*	Membership in ~P1 ~P1 ~P1 ~P1 1c. (Contributed by SF, 14-Jan-2015.)
|- (A e. ~P1 ~P1 ~P1 ~P1 1c <-> E.x A = {{{{{x}}}}})
Theorem	elpw151c 4151*	Membership in ~P1 ~P1 ~P1 ~P1 ~P1 1c. (Contributed by SF, 14-Jan-2015.)
|- (A e. ~P1 ~P1 ~P1 ~P1 ~P1 1c <-> E.x A = {{{{{{x}}}}}})
Theorem	elpw161c 4152*	Membership in ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c. (Contributed by SF, 14-Jan-2015.)
|- (A e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c <-> E.x A = {{{{{{{x}}}}}}})
Theorem	elpw171c 4153*	Membership in ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c. (Contributed by SF, 15-Jan-2015.)
|- (A e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c <-> E.x A = {{{{{{{{x}}}}}}}})
Theorem	elpw181c 4154*	Membership in ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c. (Contributed by SF, 15-Jan-2015.)
|- (A e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c <-> E.x A = {{{{{{{{{x}}}}}}}}})
Theorem	elpw191c 4155*	Membership in ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c. (Contributed by SF, 24-Jan-2015.)
|- (A e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c <-> E.x A = {{{{{{{{{{x}}}}}}}}}})
Theorem	elpw1101c 4156*	Membership in ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c. (Contributed by SF, 24-Jan-2015.)
|- (A e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c <-> E.x A = {{{{{{{{{{{x}}}}}}}}}}})
Theorem	elpw1111c 4157*	Membership in ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c. (Contributed by SF, 24-Jan-2015.)
|- (A e. ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 ~P1 1c <-> E.x A = {{{{{{{{{{{{x}}}}}}}}}}}})
Theorem	pw1ss1c 4158	A unit power class is a subset of 1c. (Contributed by SF, 22-Jan-2015.)
|- ~P1 A C_ 1c
Theorem	0nel1c 4159	The empty class is not a singleton. (Contributed by SF, 22-Jan-2015.)
|- -. (/) e. 1c
Theorem	pw0 4160	Compute the power set of the empty set. Theorem 89 of [Suppes] p. 47. (The proof was shortened by Andrew Salmon, 29-Jun-2011.) (Contributed by SF, 5-Aug-1993.) (Revised by SF, 29-Jun-2011.)
|- ~P(/) = {(/)}
Theorem	pw10 4161	Compute the unit power class of (/). (Contributed by SF, 22-Jan-2015.)
|- ~P1 (/) = (/)
Theorem	eqpw1 4162*	A condition for equality to unit power class. (Contributed by SF, 21-Jan-2015.)
|- (A = ~P1 B <-> (A C_ 1c /\ A.x({x} e. A <-> x e. B)))
Theorem	pw1un 4163	Unit power class distributes over union. (Contributed by SF, 22-Jan-2015.)
|- ~P1 (A u. B) = (~P1 A u. ~P1 B)
Theorem	pw1in 4164	Unit power class distributes over intersection. (Contributed by SF, 13-Feb-2015.)
|- ~P1 (A i^i B) = (~P1 A i^i ~P1 B)
Theorem	pw1sn 4165	Compute the unit power class of a singleton. (Contributed by SF, 22-Jan-2015.)
|- A e. _V   =>   |- ~P1 {A} = {{A}}
Theorem	pw10b 4166	The unit power class of a class is empty iff the class itself is empty. (Contributed by SF, 22-Jan-2015.)
|- (~P1 A = (/) <-> A = (/))
Theorem	pw1disj 4167	Two unit power classes are disjoint iff the classes themselves are disjoint. (Contributed by SF, 26-Jan-2015.)
|- ((~P1 A i^i ~P1 B) = (/) <-> (A i^i B) = (/))
Theorem	df1c2 4168	Cardinal one is the unit power class of the universe. (Contributed by SF, 29-Jan-2015.)
|- 1c = ~P1 _V
Theorem	pw1ss 4169	Unit power set preserves subset. (Contributed by SF, 3-Feb-2015.)
|- (A C_ B -> ~P1 A C_ ~P1 B)
Theorem	pw111 4170	The unit power class operation is one-to-one. (Contributed by SF, 26-Feb-2015.)
|- (~P1 A = ~P1 B <-> A = B)
Theorem	pw1sspw 4171	A unit power class is a subset of a power class. (Contributed by SF, 10-Mar-2015.)
|- ~P1 A C_ ~PA
Theorem	eluni1g 4172	Membership in a unit union. (Contributed by SF, 15-Mar-2015.)
|- (A e. V -> (A e. ⋃1B <-> {A} e. B))
Theorem	eluni1 4173	Membership in a unit union. (Contributed by SF, 15-Mar-2015.)
|- A e. _V   =>   |- (A e. ⋃1B <-> {A} e. B)
2.2.7  Kuratowski relationships
Syntax	cxpk 4174	Extend the definition of a class to include the Kuratowski cross product.
class (A X.k B)
Syntax	ccnvk 4175	Extend the definition of a class to include the Kuratowski converse of a class.
class `'kA
Syntax	cins2k 4176	Extend the definition of a class to include the Kuratowski second insertion operator.
class Ins2k A
Syntax	cins3k 4177	Extend the definition of a class to include the Kuratowski third insertion operator.
class Ins3k A
Syntax	cp6 4178	Extend the definition of a class to include the P6 operator (the set guaranteed by ax-typlower 4086).
class P6 A
Syntax	cimak 4179	Extend the definition of a class to include the Kuratowski image of a class. (Read: The image of B under A.)
class (A"kB)
Syntax	ccomk 4180	Extend the definition of a class to include the Kuratowski composition of two classes. (Read: The composition of A and B.)
class (A o.k B)
Syntax	csik 4181	Extend the definition of a class to include the Kuratowski singleton image.
class SIk A
Syntax	cimagek 4182	Extend the definition of a class to include the Kuratowski image functor.
class ImagekA
Syntax	cssetk 4183	Extend the definition of a class to include the Kuratowski subset relationship.
class Sk
Syntax	cidk 4184	Extend the definition of a class to include the Kuratowski identity relationship.
class _I_kk
Definition	df-xpk 4185*	Define the Kuratowski cross product. This definition through df-idk 4195 set up the Kuratowski relationships. These are used mainly to prove the properties of df-op 4566, and are not used thereafter. (Contributed by SF, 12-Jan-2015.)
|- (A X.k B) = {x | E.yE.z(x = <<y, z>> /\ (y e. A /\ z e. B))}
Definition	df-cnvk 4186*	Define the Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
|- `'kA = {x | E.yE.z(x = <<y, z>> /\ <<z, y>> e. A)}
Definition	df-ins2k 4187*	Define the Kuratowski second insertion operator. (Contributed by SF, 12-Jan-2015.)
|- Ins2k A = {x | E.yE.z(x = <<y, z>> /\ E.tE.uE.v(y = {{t}} /\ z = <<u, v>> /\ <<t, v>> e. A))}
Definition	df-ins3k 4188*	Define the Kuratowski third insertion operator. (Contributed by SF, 12-Jan-2015.)
|- Ins3k A = {x | E.yE.z(x = <<y, z>> /\ E.tE.uE.v(y = {{t}} /\ z = <<u, v>> /\ <<t, u>> e. A))}
Definition	df-imak 4189*	Define the Kuratowski image operator. (Contributed by SF, 12-Jan-2015.)
|- (A"kB) = {x | E.y e. B <<y, x>> e. A}
Definition	df-cok 4190	Define the Kuratowski composition operator. (Contributed by SF, 12-Jan-2015.)
|- (A o.k B) = (( Ins2k A i^i Ins3k `'kB)"k_V)
Definition	df-p6 4191*	Define the P6 operator. This is the set guaranteed by ax-typlower 4086. (Contributed by SF, 12-Jan-2015.)
|- P6 A = {x | (_V X.k {{x}}) C_ A}
Definition	df-sik 4192*	Define the Kuratowski singleton image operation. (Contributed by SF, 12-Jan-2015.)
|- SIk A = {x | E.yE.z(x = <<y, z>> /\ E.tE.u(y = {t} /\ z = {u} /\ <<t, u>> e. A))}
Definition	df-ssetk 4193*	Define the Kuratowski subset relationship. (Contributed by SF, 12-Jan-2015.)
|- Sk = {x | E.yE.z(x = <<y, z>> /\ y C_ z)}
Definition	df-imagek 4194	Define the Kuratowski image function. See opkelimagek 4272 for membership. (Contributed by SF, 12-Jan-2015.)
|- ImagekA = ((_V X.k _V) \ (( Ins2k Sk (+) Ins3k ( Sk o.k `'k SIk A))"k~P1 ~P1 1c))
Definition	df-idk 4195*	Define the Kuratowski identity relationship. (Contributed by SF, 12-Jan-2015.)
|- _I_kk = {x | E.yE.z(x = <<y, z>> /\ y = z)}
Theorem	elxpk 4196*	Membership in a Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
|- (A e. (B X.k C) <-> E.xE.y(A = <<x, y>> /\ (x e. B /\ y e. C)))
Theorem	elxpk2 4197*	Membership in a cross product. (Contributed by SF, 12-Jan-2015.)
|- (A e. (B X.k C) <-> E.x e. B E.y e. C A = <<x, y>>)
Theorem	xpkeq1 4198	Equality theorem for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> (A X.k C) = (B X.k C))
Theorem	xpkeq2 4199	Equality theorem for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> (C X.k A) = (C X.k B))
Theorem	xpkeq12 4200	Equality theorem for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
|- ((A = B /\ C = D) -> (A X.k C) = (B X.k D))