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	inexg 4101	The intersection of two sets is a set. (Contributed by SF, 12-Jan-2015.)
|- ((A e. V /\ B e. W) -> (A i^i B) e. _V)
Theorem	unexg 4102	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 4103	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 4104	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 4105	The complement of a set is a set. (Contributed by SF, 12-Jan-2015.)
|- A e. _V   =>   |- ∼ A e. _V
Theorem	inex 4106	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 4107	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 4108	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 4109	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 4110	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 4111	The empty class exists. (Contributed by SF, 12-Jan-2015.)
|- (/) e. _V
Theorem	snex 4112	A singleton always exists. (Contributed by SF, 12-Jan-2015.)
|- {A} e. _V
Theorem	prex 4113	An unordered pair exists. (Contributed by SF, 12-Jan-2015.)
|- {A, B} e. _V
Theorem	opkex 4114	A Kuratowski ordered pair exists. (Contributed by SF, 12-Jan-2015.)
|- <<A, B>> e. _V
Theorem	snelpwg 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	snelpw 4116	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 4117	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 4118	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 4119	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 4120*	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 4121	A singleton is a subset of an unordered pair. (Contributed by SF, 12-Jan-2015.)
|- {A} C_ {A, B}
Theorem	snprss2 4122	A singleton is a subset of an unordered pair. (Contributed by SF, 12-Jan-2015.)
|- {A} C_ {B, A}
Theorem	prprc2 4123	An unordered pair of a proper class. (Contributed by SF, 12-Jan-2015.)
|- (-. A e. _V -> {B, A} = {B})
Theorem	prprc1 4124	An unordered pair of a proper class. (Contributed by SF, 12-Jan-2015.)
|- (-. A e. _V -> {A, B} = {B})
Theorem	preqr1 4125	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 4126	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 4127	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 4128	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 4129	Closed form of preq12b 4128. (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 4130	Membership in a Kuratowski ordered pair. (Contributed by SF, 12-Jan-2015.)
|- (A e. <<B, C>> <-> (A = {B} \/ A = {B, C}))
Theorem	opkth1g 4131	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 4132	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 4133	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 4134	Extend class notation to include the unit union of a class (read: 'unit union A')
class ⋃1A
Syntax	c1c 4135	Extend the definition of a class to include cardinal one.
class 1c
Syntax	cpw1 4136	Extend class notation to include unit power class.
class ~P1 A
Definition	df-1c 4137*	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 4138	Define unit power class. Definition from [Rosser] p. 252. (Contributed by SF, 12-Jan-2015.)
|- ~P1 A = (~PA i^i 1c)
Definition	df-uni1 4139	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 4174 for membership condition. (Contributed by SF, 12-Jan-2015.)
|- ⋃1A = U.(A i^i 1c)
Theorem	el1c 4140*	Membership in cardinal one. (Contributed by SF, 12-Jan-2015.)
|- (A e. 1c <-> E.x A = {x})
Theorem	snel1c 4141	A singleton is an element of cardinal one. (Contributed by SF, 13-Jan-2015.)
|- A e. _V   =>   |- {A} e. 1c
Theorem	snel1cg 4142	A singleton is an element of cardinal one. (Contributed by SF, 30-Jan-2015.)
|- (A e. V -> {A} e. 1c)
Theorem	1cex 4143	Cardinal one is a set. (Contributed by SF, 12-Jan-2015.)
|- 1c e. _V
Theorem	pw1eq 4144	Equality theorem for unit power class. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> ~P1 A = ~P1 B)
Theorem	elpw1 4145*	Membership in a unit power class. (Contributed by SF, 13-Jan-2015.)
|- (A e. ~P1 B <-> E.x e. B A = {x})
Theorem	elpw12 4146*	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 4147	Membership of a singleton in a unit power class. (Contributed by SF, 13-Jan-2015.)
|- ({A} e. ~P1 B <-> A e. B)
Theorem	elpw11c 4148*	Membership in ~P1 1c. (Contributed by SF, 13-Jan-2015.)
|- (A e. ~P1 1c <-> E.x A = {{x}})
Theorem	elpw121c 4149*	Membership in ~P1 ~P1 1c. (Contributed by SF, 13-Jan-2015.)
|- (A e. ~P1 ~P1 1c <-> E.x A = {{{x}}})
Theorem	elpw131c 4150*	Membership in ~P1 ~P1 ~P1 1c. (Contributed by SF, 14-Jan-2015.)
|- (A e. ~P1 ~P1 ~P1 1c <-> E.x A = {{{{x}}}})
Theorem	elpw141c 4151*	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 4152*	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 4153*	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 4154*	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 4155*	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 4156*	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 4157*	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 4158*	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 4159	A unit power class is a subset of 1c. (Contributed by SF, 22-Jan-2015.)
|- ~P1 A C_ 1c
Theorem	0nel1c 4160	The empty class is not a singleton. (Contributed by SF, 22-Jan-2015.)
|- -. (/) e. 1c
Theorem	pw0 4161	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 4162	Compute the unit power class of (/). (Contributed by SF, 22-Jan-2015.)
|- ~P1 (/) = (/)
Theorem	eqpw1 4163*	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 4164	Unit power class distributes over union. (Contributed by SF, 22-Jan-2015.)
|- ~P1 (A u. B) = (~P1 A u. ~P1 B)
Theorem	pw1in 4165	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 4166	Compute the unit power class of a singleton. (Contributed by SF, 22-Jan-2015.)
|- A e. _V   =>   |- ~P1 {A} = {{A}}
Theorem	pw10b 4167	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 4168	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 4169	Cardinal one is the unit power class of the universe. (Contributed by SF, 29-Jan-2015.)
|- 1c = ~P1 _V
Theorem	pw1ss 4170	Unit power set preserves subset. (Contributed by SF, 3-Feb-2015.)
|- (A C_ B -> ~P1 A C_ ~P1 B)
Theorem	pw111 4171	The unit power class operation is one-to-one. (Contributed by SF, 26-Feb-2015.)
|- (~P1 A = ~P1 B <-> A = B)
Theorem	pw1sspw 4172	A unit power class is a subset of a power class. (Contributed by SF, 10-Mar-2015.)
|- ~P1 A C_ ~PA
Theorem	eluni1g 4173	Membership in a unit union. (Contributed by SF, 15-Mar-2015.)
|- (A e. V -> (A e. ⋃1B <-> {A} e. B))
Theorem	eluni1 4174	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 4175	Extend the definition of a class to include the Kuratowski cross product.
class (A X.k B)
Syntax	ccnvk 4176	Extend the definition of a class to include the Kuratowski converse of a class.
class `'kA
Syntax	cins2k 4177	Extend the definition of a class to include the Kuratowski second insertion operator.
class Ins2k A
Syntax	cins3k 4178	Extend the definition of a class to include the Kuratowski third insertion operator.
class Ins3k A
Syntax	cp6 4179	Extend the definition of a class to include the P6 operator (the set guaranteed by ax-typlower 4087).
class P6 A
Syntax	cimak 4180	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 4181	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 4182	Extend the definition of a class to include the Kuratowski singleton image.
class SIk A
Syntax	cimagek 4183	Extend the definition of a class to include the Kuratowski image functor.
class ImagekA
Syntax	cssetk 4184	Extend the definition of a class to include the Kuratowski subset relationship.
class Sk
Syntax	cidk 4185	Extend the definition of a class to include the Kuratowski identity relationship.
class _I_kk
Definition	df-xpk 4186*	Define the Kuratowski cross product. This definition through df-idk 4196 set up the Kuratowski relationships. These are used mainly to prove the properties of df-op 4567, 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 4187*	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 4188*	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 4189*	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 4190*	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 4191	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 4192*	Define the P6 operator. This is the set guaranteed by ax-typlower 4087. (Contributed by SF, 12-Jan-2015.)
|- P6 A = {x | (_V X.k {{x}}) C_ A}
Definition	df-sik 4193*	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 4194*	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 4195	Define the Kuratowski image function. See opkelimagek 4273 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 4196*	Define the Kuratowski identity relationship. (Contributed by SF, 12-Jan-2015.)
|- _I_kk = {x | E.yE.z(x = <<y, z>> /\ y = z)}
Theorem	elxpk 4197*	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 4198*	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 4199	Equality theorem for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> (A X.k C) = (B X.k C))
Theorem	xpkeq2 4200	Equality theorem for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> (C X.k A) = (C X.k B))