Theorem List for New Foundations Explorer - 4201-4300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | xpkeq1i 4201 |
Equality inference for Kuratowski cross product. (Contributed by SF,
12-Jan-2015.)
|
 k   k   |
|
Theorem | xpkeq2i 4202 |
Equality inference for Kuratowski cross product. (Contributed by SF,
12-Jan-2015.)
|
 k   k   |
|
Theorem | xpkeq12i 4203 |
Equality inference for Kuratowski cross product. (Contributed by SF,
12-Jan-2015.)
|
 k   k   |
|
Theorem | xpkeq1d 4204 |
Equality deduction for Kuratowski cross product. (Contributed by SF,
12-Jan-2015.)
|
    k 
 k    |
|
Theorem | xpkeq2d 4205 |
Equality deduction for Kuratowski cross product. (Contributed by SF,
12-Jan-2015.)
|
    k 
 k    |
|
Theorem | xpkeq12d 4206 |
Equality deduction for Kuratowski cross product. (Contributed by SF,
12-Jan-2015.)
|
      k 
 k    |
|
Theorem | elvvk 4207* |
Membership in  k  (Contributed by SF, 13-Jan-2015.)
|
  k 
  
     |
|
Theorem | opkabssvvk 4208* |
Any Kuratowski ordered pair abstraction is a subset of
 k  . (Contributed by SF, 13-Jan-2015.)
|

           k   |
|
Theorem | opkabssvvki 4209* |
Any Kuratowski ordered pair abstraction is a subset of
 k  . (Contributed by SF, 13-Jan-2015.)
|
     
      k   |
|
Theorem | xpkssvvk 4210 |
Any Kuratowski cross product is a subset of  k  .
(Contributed by SF, 13-Jan-2015.)
|
 k   k   |
|
Theorem | ssrelk 4211* |
Subset for Kuratowski relationships. (Contributed by SF,
13-Jan-2015.)
|
  k 
                |
|
Theorem | eqrelk 4212* |
Equality for two Kuratowski relationships. (Contributed by SF,
13-Jan-2015.)
|
   k 
 k   
               |
|
Theorem | eqrelkriiv 4213* |
Equality for two Kuratowski relationships. (Contributed by SF,
13-Jan-2015.)
|
 k   k         
 |
|
Theorem | eqrelkrdv 4214* |
Equality for two Kuratowski relationships. (Contributed by SF,
13-Jan-2015.)
|
 k   k               |
|
Theorem | cnvkeq 4215 |
Equality theorem for Kuratowski converse. (Contributed by SF,
12-Jan-2015.)
|
 k k  |
|
Theorem | cnvkeqi 4216 |
Equality inference for Kuratowski converse. (Contributed by SF,
12-Jan-2015.)
|
k
k |
|
Theorem | cnvkeqd 4217 |
Equality deduction for Kuratowski converse. (Contributed by SF,
12-Jan-2015.)
|
   k k  |
|
Theorem | ins2keq 4218 |
Equality theorem for the Kuratowski insert two operator. (Contributed
by SF, 12-Jan-2015.)
|
 Ins2k
Ins2k   |
|
Theorem | ins3keq 4219 |
Equality theorem for the Kuratowski insert three operator. (Contributed
by SF, 12-Jan-2015.)
|
 Ins3k
Ins3k   |
|
Theorem | ins2keqi 4220 |
Equality inference for Kuratowski insert two operator. (Contributed by
SF, 12-Jan-2015.)
|
Ins2k Ins2k  |
|
Theorem | ins3keqi 4221 |
Equality inference for Kuratowski insert three operator. (Contributed
by SF, 12-Jan-2015.)
|
Ins3k Ins3k  |
|
Theorem | ins2keqd 4222 |
Equality deduction for Kuratowski insert two operator. (Contributed by
SF, 12-Jan-2015.)
|
   Ins2k Ins2k   |
|
Theorem | ins3keqd 4223 |
Equality deduction for Kuratowski insert three operator. (Contributed
by SF, 12-Jan-2015.)
|
   Ins3k Ins3k   |
|
Theorem | imakeq1 4224 |
Equality theorem for Kuratowski image. (Contributed by SF,
12-Jan-2015.)
|
   k   k   |
|
Theorem | imakeq2 4225 |
Equality theorem for Kuratowski image. (Contributed by SF,
12-Jan-2015.)
|
   k   k   |
|
Theorem | imakeq1i 4226 |
Equality theorem for image. (Contributed by SF, 12-Jan-2015.)
|
  k   k  |
|
Theorem | imakeq2i 4227 |
Equality theorem for Kuratowski image. (Contributed by SF,
12-Jan-2015.)
|
  k   k  |
|
Theorem | imakeq1d 4228 |
Equality theorem for Kuratowski image. (Contributed by SF,
12-Jan-2015.)
|
     k   k   |
|
Theorem | imakeq2d 4229 |
Equality theorem for Kuratowski image. (Contributed by SF,
12-Jan-2015.)
|
     k   k   |
|
Theorem | cokeq1 4230 |
Equality theorem for Kuratowski composition of two classes. (Contributed
by SF, 12-Jan-2015.)
|
  k   k    |
|
Theorem | cokeq2 4231 |
Equality theorem for Kuratowski composition of two classes. (Contributed
by SF, 12-Jan-2015.)
|
  k   k    |
|
Theorem | cokeq1i 4232 |
Equality inference for Kuratowski composition of two classes.
(Contributed by SF, 12-Jan-2015.)
|
 k   k   |
|
Theorem | cokeq2i 4233 |
Equality inference for Kuratowski composition of two classes.
(Contributed by SF, 12-Jan-2015.)
|
 k   k   |
|
Theorem | cokeq1d 4234 |
Equality deduction for Kuratowski composition of two classes.
(Contributed by SF, 12-Jan-2015.)
|
    k   k    |
|
Theorem | cokeq2d 4235 |
Equality deduction for Kuratowski composition of two classes.
(Contributed by SF, 12-Jan-2015.)
|
    k   k    |
|
Theorem | cokeq12i 4236 |
Equality inference for Kuratowski composition of two classes.
(Contributed by SF, 12-Jan-2015.)
|
 k   k   |
|
Theorem | cokeq12d 4237 |
Equality deduction for Kuratowski composition of two classes.
(Contributed by SF, 12-Jan-2015.)
|
      k   k    |
|
Theorem | p6eq 4238 |
Equality theorem for P6 operation. (Contributed by SF, 12-Jan-2015.)
|
 P6 P6   |
|
Theorem | p6eqi 4239 |
Equality inference for the P6 operation. (Contributed by SF,
12-Jan-2015.)
|
P6 P6  |
|
Theorem | p6eqd 4240 |
Equality deduction for the P6 operation. (Contributed by SF,
12-Jan-2015.)
|
   P6 P6   |
|
Theorem | sikeq 4241 |
Equality theorem for Kuratowski singleton image. (Contributed by SF,
12-Jan-2015.)
|
 SIk
SIk   |
|
Theorem | sikeqi 4242 |
Equality inference for Kuratowski singleton image. (Contributed by SF,
12-Jan-2015.)
|
SIk SIk  |
|
Theorem | sikeqd 4243 |
Equality deduction for Kuratowski singleton image. (Contributed by SF,
12-Jan-2015.)
|
   SIk SIk   |
|
Theorem | imagekeq 4244 |
Equality theorem for image operation. (Contributed by SF,
12-Jan-2015.)
|
 Imagek Imagek  |
|
Theorem | opkelopkabg 4245* |
Kuratowski ordered pair membership in an abstraction of Kuratowski
ordered pairs. (Contributed by SF, 12-Jan-2015.)
|
     
                       |
|
Theorem | opkelopkab 4246* |
Kuratowski ordered pair membership in an abstraction of Kuratowski
ordered pairs. (Contributed by SF, 12-Jan-2015.)
|
     
                   |
|
Theorem | opkelxpkg 4247 |
Kuratowski ordered pair membership in a Kuratowski cross product.
(Contributed by SF, 12-Jan-2015.)
|
        k 
     |
|
Theorem | opkelxpk 4248 |
Kuratowski ordered pair membership in a Kuratowski cross product.
(Contributed by SF, 13-Jan-2015.)
|
     k  
   |
|
Theorem | opkelcnvkg 4249 |
Kuratowski ordered pair membership in a Kuratowski converse.
(Contributed by SF, 12-Jan-2015.)
|
       k       |
|
Theorem | opkelcnvk 4250 |
Kuratowski ordered pair membership in a Kuratowski converse.
(Contributed by SF, 14-Jan-2015.)
|
    k      |
|
Theorem | opkelins2kg 4251* |
Kuratowski ordered pair membership in Kuratowski insertion operator.
(Contributed by SF, 12-Jan-2015.)
|
       Ins2k           
          |
|
Theorem | opkelins3kg 4252* |
Kuratowski ordered pair membership in Kuratowski insertion operator.
(Contributed by SF, 12-Jan-2015.)
|
       Ins3k           
          |
|
Theorem | otkelins2kg 4253 |
Kuratowski ordered triple membership in Kuratowski insertion operator.
(Contributed by SF, 12-Jan-2015.)
|
             
Ins2k       |
|
Theorem | otkelins3kg 4254 |
Kuratowski ordered triple membership in Kuratowski insertion operator.
(Contributed by SF, 12-Jan-2015.)
|
             
Ins3k       |
|
Theorem | otkelins2k 4255 |
Kuratowski ordered triple membership in Kuratowski insertion operator.
(Contributed by SF, 12-Jan-2015.)
|
          
Ins2k      |
|
Theorem | otkelins3k 4256 |
Kuratowski ordered triple membership in Kuratowski insertion operator.
(Contributed by SF, 12-Jan-2015.)
|
          
Ins3k      |
|
Theorem | elimakg 4257* |
Membership in a Kuratowski image. (Contributed by SF, 13-Jan-2015.)
|
    k        |
|
Theorem | elimakvg 4258* |
Membership in a Kuratowski image under . (Contributed by SF,
13-Jan-2015.)
|
    k         |
|
Theorem | elimak 4259* |
Membership in a Kuratowski image. (Contributed by SF, 13-Jan-2015.)
|
   k       |
|
Theorem | elimakv 4260* |
Membership in a Kuratowski image under . (Contributed by SF,
13-Jan-2015.)
|
   k        |
|
Theorem | opkelcokg 4261* |
Membership in a Kuratowski composition. (Contributed by SF,
13-Jan-2015.)
|
        k 
             |
|
Theorem | opkelcok 4262* |
Membership in a Kuratowski composition. (Contributed by SF,
13-Jan-2015.)
|
     k              |
|
Theorem | elp6 4263* |
Membership in the P6 operator. (Contributed by SF, 13-Jan-2015.)
|
  P6           |
|
Theorem | opkelsikg 4264* |
Membership in Kuratowski singleton image. (Contributed by SF,
13-Jan-2015.)
|
       SIk                 |
|
Theorem | opksnelsik 4265 |
Membership of an ordered pair of singletons in a Kuratowski singleton
image. (Contributed by SF, 13-Jan-2015.)
|
        SIk      |
|
Theorem | sikssvvk 4266 |
A Kuratowski singleton image is a Kuratowski relationship. (Contributed
by SF, 13-Jan-2015.)
|
SIk  k   |
|
Theorem | sikss1c1c 4267 |
A Kuratowski singleton image is a subset of 1c k 1c .
(Contributed by SF, 13-Jan-2015.)
|
SIk 1c k 1c |
|
Theorem | opkelssetkg 4268 |
Membership in the Kuratowski subset relationship. (Contributed by SF,
13-Jan-2015.)
|
       Sk    |
|
Theorem | elssetkg 4269 |
Membership via the Kuratowski subset relationship. (Contributed by SF,
13-Jan-2015.)
|
         Sk    |
|
Theorem | elssetk 4270 |
Membership via the Kuratowski subset relationship. (Contributed by SF,
13-Jan-2015.)
|
     
Sk   |
|
Theorem | opkelimagekg 4271 |
Membership in the Kuratowski image functor. (Contributed by SF,
13-Jan-2015.)
|
      
Imagek   k    |
|
Theorem | opkelimagek 4272 |
Membership in the Kuratowski image functor. (Contributed by SF,
20-Jan-2015.)
|
    Imagek
  k   |
|
Theorem | imagekrelk 4273 |
The Kuratowski image functor is a relationship. (Contributed by SF,
14-Jan-2015.)
|
Imagek  k   |
|
Theorem | opkelidkg 4274 |
Membership in the Kuratowski identity relationship. (Contributed by SF,
13-Jan-2015.)
|
       k
   |
|
Theorem | cnvkssvvk 4275 |
A Kuratowski converse is a Kuratowski relationship. (Contributed by SF,
13-Jan-2015.)
|
k  k   |
|
Theorem | cnvkxpk 4276 |
The converse of a Kuratowski cross product. (Contributed by SF,
13-Jan-2015.)
|
k
k
  k   |
|
Theorem | inxpk 4277 |
The intersection of two Kuratowski cross products. (Contributed by SF,
13-Jan-2015.)
|
  k   k  
 
 k 
   |
|
Theorem | ssetkssvvk 4278 |
The Kuratowski subset relationship is a Kuratowski relationship.
(Contributed by SF, 13-Jan-2015.)
|
Sk  k   |
|
Theorem | ins2kss 4279 |
Subset law for Ins2k . (Contributed by SF,
14-Jan-2015.)
|
Ins2k  1 1c k  k    |
|
Theorem | ins3kss 4280 |
Subset law for Ins3k . (Contributed by SF,
14-Jan-2015.)
|
Ins3k  1 1c k  k    |
|
Theorem | idkssvvk 4281 |
The Kuratowski identity relationship is a Kuratowski relationship.
(Contributed by SF, 14-Jan-2015.)
|
k  k   |
|
Theorem | imacok 4282 |
Image under a composition. (Contributed by SF, 4-Feb-2015.)
|
  k   k   k  k   |
|
Theorem | elimaksn 4283 |
Membership in a Kuratowski image of a singleton. (Contributed by SF,
4-Feb-2015.)
|
   k        |
|
Theorem | cokrelk 4284 |
A Kuratowski composition is a Kuratowski relationship. (Contributed by
SF, 4-Feb-2015.)
|
 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, 13-Jan-2015.)
|
  k    |
|
Theorem | cnvkexg 4286 |
The Kuratowski converse of a set is a set. (Contributed by SF,
13-Jan-2015.)
|
 k   |
|
Theorem | cnvkex 4287 |
The Kuratowski converse of a set is a set. (Contributed by SF,
14-Jan-2015.)
|
k  |
|
Theorem | xpkexg 4288 |
The Kuratowski cross product of two sets is a set. (Contributed by SF,
13-Jan-2015.)
|
    k    |
|
Theorem | xpkex 4289 |
The Kuratowski cross product of two sets is a set. (Contributed by SF,
14-Jan-2015.)
|
 k   |
|
Theorem | p6exg 4290 |
The P6 operator applied to a set yields a set. (Contributed by SF,
13-Jan-2015.)
|
 P6   |
|
Theorem | dfuni12 4291 |
Alternate definition of unit union. (Contributed by SF,
15-Mar-2015.)
|
⋃1 P6  k   |
|
Theorem | uni1exg 4292 |
The unit union operator preserves sethood. (Contributed by SF,
13-Jan-2015.)
|
 ⋃1   |
|
Theorem | uni1ex 4293 |
The unit union operator preserves sethood. (Contributed by SF,
14-Jan-2015.)
|
⋃1  |
|
Theorem | ssetkex 4294 |
The Kuratowski subset relationship is a set. (Contributed by SF,
13-Jan-2015.)
|
Sk  |
|
Theorem | sikexlem 4295* |
Lemma for sikexg 4296. Equality for two subsets of
1c squared .
(Contributed by SF, 14-Jan-2015.)
|
1c k 1c 1c k 1c 
                      |
|
Theorem | sikexg 4296 |
The Kuratowski singleton image of a set is a set. (Contributed by SF,
14-Jan-2015.)
|
 SIk
  |
|
Theorem | sikex 4297 |
The Kuratowski singleton image of a set is a set. (Contributed by SF,
14-Jan-2015.)
|
SIk  |
|
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, 14-Jan-2015.)
|
  k ∼ P6 ∼ 1c k 
SIk ∼   k     |
|
Theorem | imakexg 4299 |
The image of a set under a set is a set. (Contributed by SF,
14-Jan-2015.)
|
     k   |
|
Theorem | imakex 4300 |
The image of a set under a set is a set. (Contributed by SF,
14-Jan-2015.)
|
  k  |