P. 43 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 4201-4300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xpkeq12 4201	Equality theorem for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
|- ((A = B /\ C = D) -> (A X.k C) = (B X.k D))
Theorem	xpkeq1i 4202	Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
|- A = B   =>   |- (A X.k C) = (B X.k C)
Theorem	xpkeq2i 4203	Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
|- A = B   =>   |- (C X.k A) = (C X.k B)
Theorem	xpkeq12i 4204	Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
|- A = B   &   |- C = D   =>   |- (A X.k C) = (B X.k D)
Theorem	xpkeq1d 4205	Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
|- (ph -> A = B)   =>   |- (ph -> (A X.k C) = (B X.k C))
Theorem	xpkeq2d 4206	Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
|- (ph -> A = B)   =>   |- (ph -> (C X.k A) = (C X.k B))
Theorem	xpkeq12d 4207	Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A X.k C) = (B X.k D))
Theorem	elvvk 4208*	Membership in (_V X.k _V). (Contributed by SF, 13-Jan-2015.)
|- (A e. (_V X.k _V) <-> E.xE.y A = <<x, y>>)
Theorem	opkabssvvk 4209*	Any Kuratowski ordered pair abstraction is a subset of (_V X.k _V). (Contributed by SF, 13-Jan-2015.)
|- {x | E.yE.z(x = <<y, z>> /\ ph)} C_ (_V X.k _V)
Theorem	opkabssvvki 4210*	Any Kuratowski ordered pair abstraction is a subset of (_V X.k _V). (Contributed by SF, 13-Jan-2015.)
|- A = {x | E.yE.z(x = <<y, z>> /\ ph)}   =>   |- A C_ (_V X.k _V)
Theorem	xpkssvvk 4211	Any Kuratowski cross product is a subset of (_V X.k _V). (Contributed by SF, 13-Jan-2015.)
|- (A X.k B) C_ (_V X.k _V)
Theorem	ssrelk 4212*	Subset for Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
|- (A C_ (_V X.k _V) -> (A C_ B <-> A.xA.y(<<x, y>> e. A -> <<x, y>> e. B)))
Theorem	eqrelk 4213*	Equality for two Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
|- ((A C_ (_V X.k _V) /\ B C_ (_V X.k _V)) -> (A = B <-> A.xA.y(<<x, y>> e. A <-> <<x, y>> e. B)))
Theorem	eqrelkriiv 4214*	Equality for two Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
|- A C_ (_V X.k _V)   &   |- B C_ (_V X.k _V)   &   |- (<<x, y>> e. A <-> <<x, y>> e. B)   =>   |- A = B
Theorem	eqrelkrdv 4215*	Equality for two Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
|- A C_ (_V X.k _V)   &   |- B C_ (_V X.k _V)   &   |- (ph -> (<<x, y>> e. A <-> <<x, y>> e. B))   =>   |- (ph -> A = B)
Theorem	cnvkeq 4216	Equality theorem for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> `'kA = `'kB)
Theorem	cnvkeqi 4217	Equality inference for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
|- A = B   =>   |- `'kA = `'kB
Theorem	cnvkeqd 4218	Equality deduction for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
|- (ph -> A = B)   =>   |- (ph -> `'kA = `'kB)
Theorem	ins2keq 4219	Equality theorem for the Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> Ins2k A = Ins2k B)
Theorem	ins3keq 4220	Equality theorem for the Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> Ins3k A = Ins3k B)
Theorem	ins2keqi 4221	Equality inference for Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
|- A = B   =>   |- Ins2k A = Ins2k B
Theorem	ins3keqi 4222	Equality inference for Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
|- A = B   =>   |- Ins3k A = Ins3k B
Theorem	ins2keqd 4223	Equality deduction for Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
|- (ph -> A = B)   =>   |- (ph -> Ins2k A = Ins2k B)
Theorem	ins3keqd 4224	Equality deduction for Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
|- (ph -> A = B)   =>   |- (ph -> Ins3k A = Ins3k B)
Theorem	imakeq1 4225	Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> (A"kC) = (B"kC))
Theorem	imakeq2 4226	Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> (C"kA) = (C"kB))
Theorem	imakeq1i 4227	Equality theorem for image. (Contributed by SF, 12-Jan-2015.)
|- A = B   =>   |- (A"kC) = (B"kC)
Theorem	imakeq2i 4228	Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
|- A = B   =>   |- (C"kA) = (C"kB)
Theorem	imakeq1d 4229	Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
|- (ph -> A = B)   =>   |- (ph -> (A"kC) = (B"kC))
Theorem	imakeq2d 4230	Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
|- (ph -> A = B)   =>   |- (ph -> (C"kA) = (C"kB))
Theorem	cokeq1 4231	Equality theorem for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> (A o.k C) = (B o.k C))
Theorem	cokeq2 4232	Equality theorem for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> (C o.k A) = (C o.k B))
Theorem	cokeq1i 4233	Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
|- A = B   =>   |- (A o.k C) = (B o.k C)
Theorem	cokeq2i 4234	Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
|- A = B   =>   |- (C o.k A) = (C o.k B)
Theorem	cokeq1d 4235	Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
|- (ph -> A = B)   =>   |- (ph -> (A o.k C) = (B o.k C))
Theorem	cokeq2d 4236	Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
|- (ph -> A = B)   =>   |- (ph -> (C o.k A) = (C o.k B))
Theorem	cokeq12i 4237	Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
|- A = B   &   |- C = D   =>   |- (A o.k C) = (B o.k D)
Theorem	cokeq12d 4238	Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A o.k C) = (B o.k D))
Theorem	p6eq 4239	Equality theorem for P6 operation. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> P6 A = P6 B)
Theorem	p6eqi 4240	Equality inference for the P6 operation. (Contributed by SF, 12-Jan-2015.)
|- A = B   =>   |- P6 A = P6 B
Theorem	p6eqd 4241	Equality deduction for the P6 operation. (Contributed by SF, 12-Jan-2015.)
|- (ph -> A = B)   =>   |- (ph -> P6 A = P6 B)
Theorem	sikeq 4242	Equality theorem for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> SIk A = SIk B)
Theorem	sikeqi 4243	Equality inference for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
|- A = B   =>   |- SIk A = SIk B
Theorem	sikeqd 4244	Equality deduction for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
|- (ph -> A = B)   =>   |- (ph -> SIk A = SIk B)
Theorem	imagekeq 4245	Equality theorem for image operation. (Contributed by SF, 12-Jan-2015.)
|- (A = B -> ImagekA = ImagekB)
Theorem	opkelopkabg 4246*	Kuratowski ordered pair membership in an abstraction of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.)
|- A = {x | E.yE.z(x = <<y, z>> /\ ph)}   &   |- (y = B -> (ph <-> ps))   &   |- (z = C -> (ps <-> ch))   =>   |- ((B e. V /\ C e. W) -> (<<B, C>> e. A <-> ch))
Theorem	opkelopkab 4247*	Kuratowski ordered pair membership in an abstraction of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.)
|- A = {x | E.yE.z(x = <<y, z>> /\ ph)}   &   |- (y = B -> (ph <-> ps))   &   |- (z = C -> (ps <-> ch))   &   |- B e. _V   &   |- C e. _V   =>   |- (<<B, C>> e. A <-> ch)
Theorem	opkelxpkg 4248	Kuratowski ordered pair membership in a Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
|- ((A e. V /\ B e. W) -> (<<A, B>> e. (C X.k D) <-> (A e. C /\ B e. D)))
Theorem	opkelxpk 4249	Kuratowski ordered pair membership in a Kuratowski cross product. (Contributed by SF, 13-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<<A, B>> e. (C X.k D) <-> (A e. C /\ B e. D))
Theorem	opkelcnvkg 4250	Kuratowski ordered pair membership in a Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
|- ((A e. V /\ B e. W) -> (<<A, B>> e. `'kC <-> <<B, A>> e. C))
Theorem	opkelcnvk 4251	Kuratowski ordered pair membership in a Kuratowski converse. (Contributed by SF, 14-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<<A, B>> e. `'kC <-> <<B, A>> e. C)
Theorem	opkelins2kg 4252*	Kuratowski ordered pair membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
|- ((A e. V /\ B e. W) -> (<<A, B>> e. Ins2k C <-> E.xE.yE.z(A = {{x}} /\ B = <<y, z>> /\ <<x, z>> e. C)))
Theorem	opkelins3kg 4253*	Kuratowski ordered pair membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
|- ((A e. V /\ B e. W) -> (<<A, B>> e. Ins3k C <-> E.xE.yE.z(A = {{x}} /\ B = <<y, z>> /\ <<x, y>> e. C)))
Theorem	otkelins2kg 4254	Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
|- ((A e. V /\ B e. W /\ C e. T) -> (<<{{A}}, <<B, C>>>> e. Ins2k D <-> <<A, C>> e. D))
Theorem	otkelins3kg 4255	Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
|- ((A e. V /\ B e. W /\ C e. T) -> (<<{{A}}, <<B, C>>>> e. Ins3k D <-> <<A, B>> e. D))
Theorem	otkelins2k 4256	Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   =>   |- (<<{{A}}, <<B, C>>>> e. Ins2k D <-> <<A, C>> e. D)
Theorem	otkelins3k 4257	Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   =>   |- (<<{{A}}, <<B, C>>>> e. Ins3k D <-> <<A, B>> e. D)
Theorem	elimakg 4258*	Membership in a Kuratowski image. (Contributed by SF, 13-Jan-2015.)
|- (C e. V -> (C e. (A"kB) <-> E.y e. B <<y, C>> e. A))
Theorem	elimakvg 4259*	Membership in a Kuratowski image under _V. (Contributed by SF, 13-Jan-2015.)
|- (C e. V -> (C e. (A"k_V) <-> E.y<<y, C>> e. A))
Theorem	elimak 4260*	Membership in a Kuratowski image. (Contributed by SF, 13-Jan-2015.)
|- C e. _V   =>   |- (C e. (A"kB) <-> E.y e. B <<y, C>> e. A)
Theorem	elimakv 4261*	Membership in a Kuratowski image under _V. (Contributed by SF, 13-Jan-2015.)
|- C e. _V   =>   |- (C e. (A"k_V) <-> E.y<<y, C>> e. A)
Theorem	opkelcokg 4262*	Membership in a Kuratowski composition. (Contributed by SF, 13-Jan-2015.)
|- ((A e. V /\ B e. W) -> (<<A, B>> e. (C o.k D) <-> E.x(<<A, x>> e. D /\ <<x, B>> e. C)))
Theorem	opkelcok 4263*	Membership in a Kuratowski composition. (Contributed by SF, 13-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<<A, B>> e. (C o.k D) <-> E.x(<<A, x>> e. D /\ <<x, B>> e. C))
Theorem	elp6 4264*	Membership in the P6 operator. (Contributed by SF, 13-Jan-2015.)
|- (A e. V -> (A e. P6 B <-> A.x<<x, {A}>> e. B))
Theorem	opkelsikg 4265*	Membership in Kuratowski singleton image. (Contributed by SF, 13-Jan-2015.)
|- ((A e. V /\ B e. W) -> (<<A, B>> e. SIk C <-> E.xE.y(A = {x} /\ B = {y} /\ <<x, y>> e. C)))
Theorem	opksnelsik 4266	Membership of an ordered pair of singletons in a Kuratowski singleton image. (Contributed by SF, 13-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<<{A}, {B}>> e. SIk C <-> <<A, B>> e. C)
Theorem	sikssvvk 4267	A Kuratowski singleton image is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
|- SIk A C_ (_V X.k _V)
Theorem	sikss1c1c 4268	A Kuratowski singleton image is a subset of (1c X.k 1c). (Contributed by SF, 13-Jan-2015.)
|- SIk A C_ (1c X.k 1c)
Theorem	opkelssetkg 4269	Membership in the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
|- ((A e. V /\ B e. W) -> (<<A, B>> e. Sk <-> A C_ B))
Theorem	elssetkg 4270	Membership via the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
|- ((A e. V /\ B e. W) -> (<<{A}, B>> e. Sk <-> A e. B))
Theorem	elssetk 4271	Membership via the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<<{A}, B>> e. Sk <-> A e. B)
Theorem	opkelimagekg 4272	Membership in the Kuratowski image functor. (Contributed by SF, 13-Jan-2015.)
|- ((A e. V /\ B e. W) -> (<<A, B>> e. ImagekC <-> B = (C"kA)))
Theorem	opkelimagek 4273	Membership in the Kuratowski image functor. (Contributed by SF, 20-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<<A, B>> e. ImagekC <-> B = (C"kA))
Theorem	imagekrelk 4274	The Kuratowski image functor is a relationship. (Contributed by SF, 14-Jan-2015.)
|- ImagekA C_ (_V X.k _V)
Theorem	opkelidkg 4275	Membership in the Kuratowski identity relationship. (Contributed by SF, 13-Jan-2015.)
|- ((A e. V /\ B e. W) -> (<<A, B>> e. _I_kk <-> A = B))
Theorem	cnvkssvvk 4276	A Kuratowski converse is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
|- `'kA C_ (_V X.k _V)
Theorem	cnvkxpk 4277	The converse of a Kuratowski cross product. (Contributed by SF, 13-Jan-2015.)
|- `'k(A X.k B) = (B X.k A)
Theorem	inxpk 4278	The intersection of two Kuratowski cross products. (Contributed by SF, 13-Jan-2015.)
|- ((A X.k B) i^i (C X.k D)) = ((A i^i C) X.k (B i^i D))
Theorem	ssetkssvvk 4279	The Kuratowski subset relationship is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
|- Sk C_ (_V X.k _V)
Theorem	ins2kss 4280	Subset law for Ins2k A. (Contributed by SF, 14-Jan-2015.)
|- Ins2k A C_ (~P1 1c X.k (_V X.k _V))
Theorem	ins3kss 4281	Subset law for Ins3k A. (Contributed by SF, 14-Jan-2015.)
|- Ins3k A C_ (~P1 1c X.k (_V X.k _V))
Theorem	idkssvvk 4282	The Kuratowski identity relationship is a Kuratowski relationship. (Contributed by SF, 14-Jan-2015.)
|- _I_kk C_ (_V X.k _V)
Theorem	imacok 4283	Image under a composition. (Contributed by SF, 4-Feb-2015.)
|- ((A o.k B)"kC) = (A"k(B"kC))
Theorem	elimaksn 4284	Membership in a Kuratowski image of a singleton. (Contributed by SF, 4-Feb-2015.)
|- B e. _V   &   |- C e. _V   =>   |- (C e. (A"k{B}) <-> <<B, C>> e. A)
Theorem	cokrelk 4285	A Kuratowski composition is a Kuratowski relationship. (Contributed by SF, 4-Feb-2015.)
|- (A o.k B) C_ (_V X.k _V)
2.2.8  Kuratowski existence theorems
Theorem	xpkvexg 4286	The Kuratowski cross product of _V with a set is a set. (Contributed by SF, 13-Jan-2015.)
|- (A e. V -> (_V X.k A) e. _V)
Theorem	cnvkexg 4287	The Kuratowski converse of a set is a set. (Contributed by SF, 13-Jan-2015.)
|- (A e. V -> `'kA e. _V)
Theorem	cnvkex 4288	The Kuratowski converse of a set is a set. (Contributed by SF, 14-Jan-2015.)
|- A e. _V   =>   |- `'kA e. _V
Theorem	xpkexg 4289	The Kuratowski cross product of two sets is a set. (Contributed by SF, 13-Jan-2015.)
|- ((A e. V /\ B e. W) -> (A X.k B) e. _V)
Theorem	xpkex 4290	The Kuratowski cross product of two sets is a set. (Contributed by SF, 14-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (A X.k B) e. _V
Theorem	p6exg 4291	The P6 operator applied to a set yields a set. (Contributed by SF, 13-Jan-2015.)
|- (A e. V -> P6 A e. _V)
Theorem	dfuni12 4292	Alternate definition of unit union. (Contributed by SF, 15-Mar-2015.)
|- ⋃1A = P6 (_V X.k A)
Theorem	uni1exg 4293	The unit union operator preserves sethood. (Contributed by SF, 13-Jan-2015.)
|- (A e. V -> ⋃1A e. _V)
Theorem	uni1ex 4294	The unit union operator preserves sethood. (Contributed by SF, 14-Jan-2015.)
|- A e. _V   =>   |- ⋃1A e. _V
Theorem	ssetkex 4295	The Kuratowski subset relationship is a set. (Contributed by SF, 13-Jan-2015.)
|- Sk e. _V
Theorem	sikexlem 4296*	Lemma for sikexg 4297. Equality for two subsets of 1c squared . (Contributed by SF, 14-Jan-2015.)
|- A C_ (1c X.k 1c)   &   |- B C_ (1c X.k 1c)   =>   |- (A = B <-> A.xA.y(<<{x}, {y}>> e. A <-> <<{x}, {y}>> e. B))
Theorem	sikexg 4297	The Kuratowski singleton image of a set is a set. (Contributed by SF, 14-Jan-2015.)
|- (A e. V -> SIk A e. _V)
Theorem	sikex 4298	The Kuratowski singleton image of a set is a set. (Contributed by SF, 14-Jan-2015.)
|- A e. _V   =>   |- SIk A e. _V
Theorem	dfimak2 4299	Alternate definition of Kuratowski image. This is the first of a series of definitions throughout the file designed to prove existence of various operations. (Contributed by SF, 14-Jan-2015.)
|- (A"kB) = ∼ P6 ( ∼ (1c X.k _V) u. SIk ∼ (A i^i (B X.k _V)))
Theorem	imakexg 4300	The image of a set under a set is a set. (Contributed by SF, 14-Jan-2015.)
|- ((A e. V /\ B e. W) -> (A"kB) e. _V)