Type  Label  Description 
Statement 

Theorem  xpkeq1i 4201 
Equality inference for Kuratowski cross product. (Contributed by SF,
12Jan2015.)

_{k} _{k} 

Theorem  xpkeq2i 4202 
Equality inference for Kuratowski cross product. (Contributed by SF,
12Jan2015.)

_{k} _{k} 

Theorem  xpkeq12i 4203 
Equality inference for Kuratowski cross product. (Contributed by SF,
12Jan2015.)

_{k} _{k} 

Theorem  xpkeq1d 4204 
Equality deduction for Kuratowski cross product. (Contributed by SF,
12Jan2015.)

_{k}
_{k} 

Theorem  xpkeq2d 4205 
Equality deduction for Kuratowski cross product. (Contributed by SF,
12Jan2015.)

_{k}
_{k} 

Theorem  xpkeq12d 4206 
Equality deduction for Kuratowski cross product. (Contributed by SF,
12Jan2015.)

_{k}
_{k} 

Theorem  elvvk 4207* 
Membership in _{k} (Contributed by SF, 13Jan2015.)

_{k}


Theorem  opkabssvvk 4208* 
Any Kuratowski ordered pair abstraction is a subset of
_{k} . (Contributed by SF, 13Jan2015.)

_{k} 

Theorem  opkabssvvki 4209* 
Any Kuratowski ordered pair abstraction is a subset of
_{k} . (Contributed by SF, 13Jan2015.)

_{k} 

Theorem  xpkssvvk 4210 
Any Kuratowski cross product is a subset of _{k} .
(Contributed by SF, 13Jan2015.)

_{k} _{k} 

Theorem  ssrelk 4211* 
Subset for Kuratowski relationships. (Contributed by SF,
13Jan2015.)

_{k}


Theorem  eqrelk 4212* 
Equality for two Kuratowski relationships. (Contributed by SF,
13Jan2015.)

_{k}
_{k}


Theorem  eqrelkriiv 4213* 
Equality for two Kuratowski relationships. (Contributed by SF,
13Jan2015.)

_{k} _{k}


Theorem  eqrelkrdv 4214* 
Equality for two Kuratowski relationships. (Contributed by SF,
13Jan2015.)

_{k} _{k} 

Theorem  cnvkeq 4215 
Equality theorem for Kuratowski converse. (Contributed by SF,
12Jan2015.)

_{k} _{k} 

Theorem  cnvkeqi 4216 
Equality inference for Kuratowski converse. (Contributed by SF,
12Jan2015.)

_{k}
_{k} 

Theorem  cnvkeqd 4217 
Equality deduction for Kuratowski converse. (Contributed by SF,
12Jan2015.)

_{k} _{k} 

Theorem  ins2keq 4218 
Equality theorem for the Kuratowski insert two operator. (Contributed
by SF, 12Jan2015.)

Ins2_{k}
Ins2_{k} 

Theorem  ins3keq 4219 
Equality theorem for the Kuratowski insert three operator. (Contributed
by SF, 12Jan2015.)

Ins3_{k}
Ins3_{k} 

Theorem  ins2keqi 4220 
Equality inference for Kuratowski insert two operator. (Contributed by
SF, 12Jan2015.)

Ins2_{k} Ins2_{k} 

Theorem  ins3keqi 4221 
Equality inference for Kuratowski insert three operator. (Contributed
by SF, 12Jan2015.)

Ins3_{k} Ins3_{k} 

Theorem  ins2keqd 4222 
Equality deduction for Kuratowski insert two operator. (Contributed by
SF, 12Jan2015.)

Ins2_{k} Ins2_{k} 

Theorem  ins3keqd 4223 
Equality deduction for Kuratowski insert three operator. (Contributed
by SF, 12Jan2015.)

Ins3_{k} Ins3_{k} 

Theorem  imakeq1 4224 
Equality theorem for Kuratowski image. (Contributed by SF,
12Jan2015.)

_{k} _{k} 

Theorem  imakeq2 4225 
Equality theorem for Kuratowski image. (Contributed by SF,
12Jan2015.)

_{k} _{k} 

Theorem  imakeq1i 4226 
Equality theorem for image. (Contributed by SF, 12Jan2015.)

_{k} _{k} 

Theorem  imakeq2i 4227 
Equality theorem for Kuratowski image. (Contributed by SF,
12Jan2015.)

_{k} _{k} 

Theorem  imakeq1d 4228 
Equality theorem for Kuratowski image. (Contributed by SF,
12Jan2015.)

_{k} _{k} 

Theorem  imakeq2d 4229 
Equality theorem for Kuratowski image. (Contributed by SF,
12Jan2015.)

_{k} _{k} 

Theorem  cokeq1 4230 
Equality theorem for Kuratowski composition of two classes. (Contributed
by SF, 12Jan2015.)

_{k} _{k} 

Theorem  cokeq2 4231 
Equality theorem for Kuratowski composition of two classes. (Contributed
by SF, 12Jan2015.)

_{k} _{k} 

Theorem  cokeq1i 4232 
Equality inference for Kuratowski composition of two classes.
(Contributed by SF, 12Jan2015.)

_{k} _{k} 

Theorem  cokeq2i 4233 
Equality inference for Kuratowski composition of two classes.
(Contributed by SF, 12Jan2015.)

_{k} _{k} 

Theorem  cokeq1d 4234 
Equality deduction for Kuratowski composition of two classes.
(Contributed by SF, 12Jan2015.)

_{k} _{k} 

Theorem  cokeq2d 4235 
Equality deduction for Kuratowski composition of two classes.
(Contributed by SF, 12Jan2015.)

_{k} _{k} 

Theorem  cokeq12i 4236 
Equality inference for Kuratowski composition of two classes.
(Contributed by SF, 12Jan2015.)

_{k} _{k} 

Theorem  cokeq12d 4237 
Equality deduction for Kuratowski composition of two classes.
(Contributed by SF, 12Jan2015.)

_{k} _{k} 

Theorem  p6eq 4238 
Equality theorem for P6 operation. (Contributed by SF, 12Jan2015.)

P6 P6 

Theorem  p6eqi 4239 
Equality inference for the P6 operation. (Contributed by SF,
12Jan2015.)

P6 P6 

Theorem  p6eqd 4240 
Equality deduction for the P6 operation. (Contributed by SF,
12Jan2015.)

P6 P6 

Theorem  sikeq 4241 
Equality theorem for Kuratowski singleton image. (Contributed by SF,
12Jan2015.)

SI_{k}
SI_{k} 

Theorem  sikeqi 4242 
Equality inference for Kuratowski singleton image. (Contributed by SF,
12Jan2015.)

SI_{k} SI_{k} 

Theorem  sikeqd 4243 
Equality deduction for Kuratowski singleton image. (Contributed by SF,
12Jan2015.)

SI_{k} SI_{k} 

Theorem  imagekeq 4244 
Equality theorem for image operation. (Contributed by SF,
12Jan2015.)

Image_{k} Image_{k} 

Theorem  opkelopkabg 4245* 
Kuratowski ordered pair membership in an abstraction of Kuratowski
ordered pairs. (Contributed by SF, 12Jan2015.)



Theorem  opkelopkab 4246* 
Kuratowski ordered pair membership in an abstraction of Kuratowski
ordered pairs. (Contributed by SF, 12Jan2015.)



Theorem  opkelxpkg 4247 
Kuratowski ordered pair membership in a Kuratowski cross product.
(Contributed by SF, 12Jan2015.)

_{k}


Theorem  opkelxpk 4248 
Kuratowski ordered pair membership in a Kuratowski cross product.
(Contributed by SF, 13Jan2015.)

_{k}


Theorem  opkelcnvkg 4249 
Kuratowski ordered pair membership in a Kuratowski converse.
(Contributed by SF, 12Jan2015.)

_{k} 

Theorem  opkelcnvk 4250 
Kuratowski ordered pair membership in a Kuratowski converse.
(Contributed by SF, 14Jan2015.)

_{k} 

Theorem  opkelins2kg 4251* 
Kuratowski ordered pair membership in Kuratowski insertion operator.
(Contributed by SF, 12Jan2015.)

Ins2_{k}


Theorem  opkelins3kg 4252* 
Kuratowski ordered pair membership in Kuratowski insertion operator.
(Contributed by SF, 12Jan2015.)

Ins3_{k}


Theorem  otkelins2kg 4253 
Kuratowski ordered triple membership in Kuratowski insertion operator.
(Contributed by SF, 12Jan2015.)

Ins2_{k} 

Theorem  otkelins3kg 4254 
Kuratowski ordered triple membership in Kuratowski insertion operator.
(Contributed by SF, 12Jan2015.)

Ins3_{k} 

Theorem  otkelins2k 4255 
Kuratowski ordered triple membership in Kuratowski insertion operator.
(Contributed by SF, 12Jan2015.)

Ins2_{k} 

Theorem  otkelins3k 4256 
Kuratowski ordered triple membership in Kuratowski insertion operator.
(Contributed by SF, 12Jan2015.)

Ins3_{k} 

Theorem  elimakg 4257* 
Membership in a Kuratowski image. (Contributed by SF, 13Jan2015.)

_{k} 

Theorem  elimakvg 4258* 
Membership in a Kuratowski image under . (Contributed by SF,
13Jan2015.)

_{k} 

Theorem  elimak 4259* 
Membership in a Kuratowski image. (Contributed by SF, 13Jan2015.)

_{k} 

Theorem  elimakv 4260* 
Membership in a Kuratowski image under . (Contributed by SF,
13Jan2015.)

_{k} 

Theorem  opkelcokg 4261* 
Membership in a Kuratowski composition. (Contributed by SF,
13Jan2015.)

_{k}


Theorem  opkelcok 4262* 
Membership in a Kuratowski composition. (Contributed by SF,
13Jan2015.)

_{k} 

Theorem  elp6 4263* 
Membership in the P6 operator. (Contributed by SF, 13Jan2015.)

P6 

Theorem  opkelsikg 4264* 
Membership in Kuratowski singleton image. (Contributed by SF,
13Jan2015.)

SI_{k} 

Theorem  opksnelsik 4265 
Membership of an ordered pair of singletons in a Kuratowski singleton
image. (Contributed by SF, 13Jan2015.)

SI_{k} 

Theorem  sikssvvk 4266 
A Kuratowski singleton image is a Kuratowski relationship. (Contributed
by SF, 13Jan2015.)

SI_{k} _{k} 

Theorem  sikss1c1c 4267 
A Kuratowski singleton image is a subset of 1_{c} _{k} 1_{c}.
(Contributed by SF, 13Jan2015.)

SI_{k} 1_{c} _{k} 1_{c} 

Theorem  opkelssetkg 4268 
Membership in the Kuratowski subset relationship. (Contributed by SF,
13Jan2015.)

S_{k} 

Theorem  elssetkg 4269 
Membership via the Kuratowski subset relationship. (Contributed by SF,
13Jan2015.)

S_{k} 

Theorem  elssetk 4270 
Membership via the Kuratowski subset relationship. (Contributed by SF,
13Jan2015.)

S_{k} 

Theorem  opkelimagekg 4271 
Membership in the Kuratowski image functor. (Contributed by SF,
13Jan2015.)

Image_{k} _{k} 

Theorem  opkelimagek 4272 
Membership in the Kuratowski image functor. (Contributed by SF,
20Jan2015.)

Image_{k}
_{k} 

Theorem  imagekrelk 4273 
The Kuratowski image functor is a relationship. (Contributed by SF,
14Jan2015.)

Image_{k} _{k} 

Theorem  opkelidkg 4274 
Membership in the Kuratowski identity relationship. (Contributed by SF,
13Jan2015.)

_{k}


Theorem  cnvkssvvk 4275 
A Kuratowski converse is a Kuratowski relationship. (Contributed by SF,
13Jan2015.)

_{k} _{k} 

Theorem  cnvkxpk 4276 
The converse of a Kuratowski cross product. (Contributed by SF,
13Jan2015.)

_{k}
_{k}
_{k} 

Theorem  inxpk 4277 
The intersection of two Kuratowski cross products. (Contributed by SF,
13Jan2015.)

_{k} _{k}
_{k}


Theorem  ssetkssvvk 4278 
The Kuratowski subset relationship is a Kuratowski relationship.
(Contributed by SF, 13Jan2015.)

S_{k} _{k} 

Theorem  ins2kss 4279 
Subset law for Ins2_{k} . (Contributed by SF,
14Jan2015.)

Ins2_{k} _{1} 1_{c} _{k} _{k} 

Theorem  ins3kss 4280 
Subset law for Ins3_{k} . (Contributed by SF,
14Jan2015.)

Ins3_{k} _{1} 1_{c} _{k} _{k} 

Theorem  idkssvvk 4281 
The Kuratowski identity relationship is a Kuratowski relationship.
(Contributed by SF, 14Jan2015.)

_{k} _{k} 

Theorem  imacok 4282 
Image under a composition. (Contributed by SF, 4Feb2015.)

_{k} _{k} _{k}_{k} 

Theorem  elimaksn 4283 
Membership in a Kuratowski image of a singleton. (Contributed by SF,
4Feb2015.)

_{k} 

Theorem  cokrelk 4284 
A Kuratowski composition is a Kuratowski relationship. (Contributed by
SF, 4Feb2015.)

_{k} _{k} 

2.2.8 Kuratowski existence theorems


Theorem  xpkvexg 4285 
The Kuratowski cross product of with a set is a set.
(Contributed by SF, 13Jan2015.)

_{k} 

Theorem  cnvkexg 4286 
The Kuratowski converse of a set is a set. (Contributed by SF,
13Jan2015.)

_{k} 

Theorem  cnvkex 4287 
The Kuratowski converse of a set is a set. (Contributed by SF,
14Jan2015.)

_{k} 

Theorem  xpkexg 4288 
The Kuratowski cross product of two sets is a set. (Contributed by SF,
13Jan2015.)

_{k} 

Theorem  xpkex 4289 
The Kuratowski cross product of two sets is a set. (Contributed by SF,
14Jan2015.)

_{k} 

Theorem  p6exg 4290 
The P6 operator applied to a set yields a set. (Contributed by SF,
13Jan2015.)

P6 

Theorem  dfuni12 4291 
Alternate definition of unit union. (Contributed by SF,
15Mar2015.)

⋃_{1} P6 _{k} 

Theorem  uni1exg 4292 
The unit union operator preserves sethood. (Contributed by SF,
13Jan2015.)

⋃_{1} 

Theorem  uni1ex 4293 
The unit union operator preserves sethood. (Contributed by SF,
14Jan2015.)

⋃_{1} 

Theorem  ssetkex 4294 
The Kuratowski subset relationship is a set. (Contributed by SF,
13Jan2015.)

S_{k} 

Theorem  sikexlem 4295* 
Lemma for sikexg 4296. Equality for two subsets of
1_{c} squared .
(Contributed by SF, 14Jan2015.)

1_{c} _{k} 1_{c} 1_{c} _{k} 1_{c}


Theorem  sikexg 4296 
The Kuratowski singleton image of a set is a set. (Contributed by SF,
14Jan2015.)

SI_{k}


Theorem  sikex 4297 
The Kuratowski singleton image of a set is a set. (Contributed by SF,
14Jan2015.)

SI_{k} 

Theorem  dfimak2 4298 
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, 14Jan2015.)

_{k} ∼ P6 ∼ 1_{c} _{k}
SI_{k} ∼ _{k} 

Theorem  imakexg 4299 
The image of a set under a set is a set. (Contributed by SF,
14Jan2015.)

_{k} 

Theorem  imakex 4300 
The image of a set under a set is a set. (Contributed by SF,
14Jan2015.)

_{k} 