 Home New Foundations ExplorerTheorem List (p. 43 of 64) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

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

Theoremxpkeq1i 4201 Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
A = B       (A ×k C) = (B ×k C)

Theoremxpkeq2i 4202 Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
A = B       (C ×k A) = (C ×k B)

Theoremxpkeq12i 4203 Equality inference for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
A = B    &   C = D       (A ×k C) = (B ×k D)

Theoremxpkeq1d 4204 Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φ → (A ×k C) = (B ×k C))

Theoremxpkeq2d 4205 Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φ → (C ×k A) = (C ×k B))

Theoremxpkeq12d 4206 Equality deduction for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
(φA = B)    &   (φC = D)       (φ → (A ×k C) = (B ×k D))

Theoremelvvk 4207* Membership in (V ×k V) (Contributed by SF, 13-Jan-2015.)
(A (V ×k V) ↔ xy A = ⟪x, y⟫)

Theoremopkabssvvk 4208* Any Kuratowski ordered pair abstraction is a subset of (V ×k V). (Contributed by SF, 13-Jan-2015.)
{x yz(x = ⟪y, z φ)} (V ×k V)

Theoremopkabssvvki 4209* Any Kuratowski ordered pair abstraction is a subset of (V ×k V). (Contributed by SF, 13-Jan-2015.)
A = {x yz(x = ⟪y, z φ)}       A (V ×k V)

Theoremxpkssvvk 4210 Any Kuratowski cross product is a subset of (V ×k V). (Contributed by SF, 13-Jan-2015.)
(A ×k B) (V ×k V)

Theoremssrelk 4211* Subset for Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
(A (V ×k V) → (A Bxy(⟪x, y A → ⟪x, y B)))

Theoremeqrelk 4212* Equality for two Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
((A (V ×k V) B (V ×k V)) → (A = Bxy(⟪x, y A ↔ ⟪x, y B)))

Theoremeqrelkriiv 4213* Equality for two Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
A (V ×k V)    &   B (V ×k V)    &   (⟪x, y A ↔ ⟪x, y B)       A = B

Theoremeqrelkrdv 4214* Equality for two Kuratowski relationships. (Contributed by SF, 13-Jan-2015.)
A (V ×k V)    &   B (V ×k V)    &   (φ → (⟪x, y A ↔ ⟪x, y B))       (φA = B)

Theoremcnvkeq 4215 Equality theorem for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
(A = BkA = kB)

Theoremcnvkeqi 4216 Equality inference for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
A = B       kA = kB

Theoremcnvkeqd 4217 Equality deduction for Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φkA = kB)

Theoremins2keq 4218 Equality theorem for the Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
(A = BIns2k A = Ins2k B)

Theoremins3keq 4219 Equality theorem for the Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
(A = BIns3k A = Ins3k B)

Theoremins2keqi 4220 Equality inference for Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
A = B        Ins2k A = Ins2k B

Theoremins3keqi 4221 Equality inference for Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
A = B        Ins3k A = Ins3k B

Theoremins2keqd 4222 Equality deduction for Kuratowski insert two operator. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φIns2k A = Ins2k B)

Theoremins3keqd 4223 Equality deduction for Kuratowski insert three operator. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φIns3k A = Ins3k B)

Theoremimakeq1 4224 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
(A = B → (Ak C) = (Bk C))

Theoremimakeq2 4225 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
(A = B → (Ck A) = (Ck B))

Theoremimakeq1i 4226 Equality theorem for image. (Contributed by SF, 12-Jan-2015.)
A = B       (Ak C) = (Bk C)

Theoremimakeq2i 4227 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
A = B       (Ck A) = (Ck B)

Theoremimakeq1d 4228 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φ → (Ak C) = (Bk C))

Theoremimakeq2d 4229 Equality theorem for Kuratowski image. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φ → (Ck A) = (Ck B))

Theoremcokeq1 4230 Equality theorem for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
(A = B → (A k C) = (B k C))

Theoremcokeq2 4231 Equality theorem for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
(A = B → (C k A) = (C k B))

Theoremcokeq1i 4232 Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
A = B       (A k C) = (B k C)

Theoremcokeq2i 4233 Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
A = B       (C k A) = (C k B)

Theoremcokeq1d 4234 Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φ → (A k C) = (B k C))

Theoremcokeq2d 4235 Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φ → (C k A) = (C k B))

Theoremcokeq12i 4236 Equality inference for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
A = B    &   C = D       (A k C) = (B k D)

Theoremcokeq12d 4237 Equality deduction for Kuratowski composition of two classes. (Contributed by SF, 12-Jan-2015.)
(φA = B)    &   (φC = D)       (φ → (A k C) = (B k D))

Theoremp6eq 4238 Equality theorem for P6 operation. (Contributed by SF, 12-Jan-2015.)
(A = BP6 A = P6 B)

Theoremp6eqi 4239 Equality inference for the P6 operation. (Contributed by SF, 12-Jan-2015.)
A = B        P6 A = P6 B

Theoremp6eqd 4240 Equality deduction for the P6 operation. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φP6 A = P6 B)

Theoremsikeq 4241 Equality theorem for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
(A = BSIk A = SIk B)

Theoremsikeqi 4242 Equality inference for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
A = B        SIk A = SIk B

Theoremsikeqd 4243 Equality deduction for Kuratowski singleton image. (Contributed by SF, 12-Jan-2015.)
(φA = B)       (φSIk A = SIk B)

Theoremimagekeq 4244 Equality theorem for image operation. (Contributed by SF, 12-Jan-2015.)
(A = B → ImagekA = ImagekB)

Theoremopkelopkabg 4245* Kuratowski ordered pair membership in an abstraction of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.)
A = {x yz(x = ⟪y, z φ)}    &   (y = B → (φψ))    &   (z = C → (ψχ))       ((B V C W) → (⟪B, C Aχ))

Theoremopkelopkab 4246* Kuratowski ordered pair membership in an abstraction of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.)
A = {x yz(x = ⟪y, z φ)}    &   (y = B → (φψ))    &   (z = C → (ψχ))    &   B V    &   C V       (⟪B, C Aχ)

Theoremopkelxpkg 4247 Kuratowski ordered pair membership in a Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
((A V B W) → (⟪A, B (C ×k D) ↔ (A C B D)))

Theoremopkelxpk 4248 Kuratowski ordered pair membership in a Kuratowski cross product. (Contributed by SF, 13-Jan-2015.)
A V    &   B V       (⟪A, B (C ×k D) ↔ (A C B D))

Theoremopkelcnvkg 4249 Kuratowski ordered pair membership in a Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
((A V B W) → (⟪A, B kC ↔ ⟪B, A C))

Theoremopkelcnvk 4250 Kuratowski ordered pair membership in a Kuratowski converse. (Contributed by SF, 14-Jan-2015.)
A V    &   B V       (⟪A, B kC ↔ ⟪B, A C)

Theoremopkelins2kg 4251* Kuratowski ordered pair membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
((A V B W) → (⟪A, B Ins2k Cxyz(A = {{x}} B = ⟪y, zx, z C)))

Theoremopkelins3kg 4252* Kuratowski ordered pair membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
((A V B W) → (⟪A, B Ins3k Cxyz(A = {{x}} B = ⟪y, zx, y C)))

Theoremotkelins2kg 4253 Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
((A V B W C T) → (⟪{{A}}, ⟪B, C⟫⟫ Ins2k D ↔ ⟪A, C D))

Theoremotkelins3kg 4254 Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
((A V B W C T) → (⟪{{A}}, ⟪B, C⟫⟫ Ins3k D ↔ ⟪A, B D))

Theoremotkelins2k 4255 Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
A V    &   B V    &   C V       (⟪{{A}}, ⟪B, C⟫⟫ Ins2k D ↔ ⟪A, C D)

Theoremotkelins3k 4256 Kuratowski ordered triple membership in Kuratowski insertion operator. (Contributed by SF, 12-Jan-2015.)
A V    &   B V    &   C V       (⟪{{A}}, ⟪B, C⟫⟫ Ins3k D ↔ ⟪A, B D)

Theoremelimakg 4257* Membership in a Kuratowski image. (Contributed by SF, 13-Jan-2015.)
(C V → (C (Ak B) ↔ y By, C A))

Theoremelimakvg 4258* Membership in a Kuratowski image under V. (Contributed by SF, 13-Jan-2015.)
(C V → (C (Ak V) ↔ yy, C A))

Theoremelimak 4259* Membership in a Kuratowski image. (Contributed by SF, 13-Jan-2015.)
C V       (C (Ak B) ↔ y By, C A)

Theoremelimakv 4260* Membership in a Kuratowski image under V. (Contributed by SF, 13-Jan-2015.)
C V       (C (Ak V) ↔ yy, C A)

Theoremopkelcokg 4261* Membership in a Kuratowski composition. (Contributed by SF, 13-Jan-2015.)
((A V B W) → (⟪A, B (C k D) ↔ x(⟪A, x D x, B C)))

Theoremopkelcok 4262* Membership in a Kuratowski composition. (Contributed by SF, 13-Jan-2015.)
A V    &   B V       (⟪A, B (C k D) ↔ x(⟪A, x D x, B C))

Theoremelp6 4263* Membership in the P6 operator. (Contributed by SF, 13-Jan-2015.)
(A V → (A P6 Bxx, {A}⟫ B))

Theoremopkelsikg 4264* Membership in Kuratowski singleton image. (Contributed by SF, 13-Jan-2015.)
((A V B W) → (⟪A, B SIk Cxy(A = {x} B = {y} x, y C)))

Theoremopksnelsik 4265 Membership of an ordered pair of singletons in a Kuratowski singleton image. (Contributed by SF, 13-Jan-2015.)
A V    &   B V       (⟪{A}, {B}⟫ SIk C ↔ ⟪A, B C)

Theoremsikssvvk 4266 A Kuratowski singleton image is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
SIk A (V ×k V)

Theoremsikss1c1c 4267 A Kuratowski singleton image is a subset of (1c ×k 1c). (Contributed by SF, 13-Jan-2015.)
SIk A (1c ×k 1c)

Theoremopkelssetkg 4268 Membership in the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
((A V B W) → (⟪A, B SkA B))

Theoremelssetkg 4269 Membership via the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
((A V B W) → (⟪{A}, B SkA B))

Theoremelssetk 4270 Membership via the Kuratowski subset relationship. (Contributed by SF, 13-Jan-2015.)
A V    &   B V       (⟪{A}, B SkA B)

Theoremopkelimagekg 4271 Membership in the Kuratowski image functor. (Contributed by SF, 13-Jan-2015.)
((A V B W) → (⟪A, B ImagekCB = (Ck A)))

Theoremopkelimagek 4272 Membership in the Kuratowski image functor. (Contributed by SF, 20-Jan-2015.)
A V    &   B V       (⟪A, B ImagekCB = (Ck A))

Theoremimagekrelk 4273 The Kuratowski image functor is a relationship. (Contributed by SF, 14-Jan-2015.)
ImagekA (V ×k V)

Theoremopkelidkg 4274 Membership in the Kuratowski identity relationship. (Contributed by SF, 13-Jan-2015.)
((A V B W) → (⟪A, B IkA = B))

Theoremcnvkssvvk 4275 A Kuratowski converse is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
kA (V ×k V)

Theoremcnvkxpk 4276 The converse of a Kuratowski cross product. (Contributed by SF, 13-Jan-2015.)
k(A ×k B) = (B ×k A)

Theoreminxpk 4277 The intersection of two Kuratowski cross products. (Contributed by SF, 13-Jan-2015.)
((A ×k B) ∩ (C ×k D)) = ((AC) ×k (BD))

Theoremssetkssvvk 4278 The Kuratowski subset relationship is a Kuratowski relationship. (Contributed by SF, 13-Jan-2015.)
Sk (V ×k V)

Theoremins2kss 4279 Subset law for Ins2k A. (Contributed by SF, 14-Jan-2015.)
Ins2k A (11c ×k (V ×k V))

Theoremins3kss 4280 Subset law for Ins3k A. (Contributed by SF, 14-Jan-2015.)
Ins3k A (11c ×k (V ×k V))

Theoremidkssvvk 4281 The Kuratowski identity relationship is a Kuratowski relationship. (Contributed by SF, 14-Jan-2015.)
Ik (V ×k V)

Theoremimacok 4282 Image under a composition. (Contributed by SF, 4-Feb-2015.)
((A k B) “k C) = (Ak (Bk C))

Theoremelimaksn 4283 Membership in a Kuratowski image of a singleton. (Contributed by SF, 4-Feb-2015.)
B V    &   C V       (C (Ak {B}) ↔ ⟪B, C A)

Theoremcokrelk 4284 A Kuratowski composition is a Kuratowski relationship. (Contributed by SF, 4-Feb-2015.)
(A k B) (V ×k V)

2.2.8  Kuratowski existence theorems

Theoremxpkvexg 4285 The Kuratowski cross product of V with a set is a set. (Contributed by SF, 13-Jan-2015.)
(A V → (V ×k A) V)

Theoremcnvkexg 4286 The Kuratowski converse of a set is a set. (Contributed by SF, 13-Jan-2015.)
(A VkA V)

Theoremcnvkex 4287 The Kuratowski converse of a set is a set. (Contributed by SF, 14-Jan-2015.)
A V       kA V

Theoremxpkexg 4288 The Kuratowski cross product of two sets is a set. (Contributed by SF, 13-Jan-2015.)
((A V B W) → (A ×k B) V)

Theoremxpkex 4289 The Kuratowski cross product of two sets is a set. (Contributed by SF, 14-Jan-2015.)
A V    &   B V       (A ×k B) V

Theoremp6exg 4290 The P6 operator applied to a set yields a set. (Contributed by SF, 13-Jan-2015.)
(A VP6 A V)

Theoremdfuni12 4291 Alternate definition of unit union. (Contributed by SF, 15-Mar-2015.)
1A = P6 (V ×k A)

Theoremuni1exg 4292 The unit union operator preserves sethood. (Contributed by SF, 13-Jan-2015.)
(A V → ⋃1A V)

Theoremuni1ex 4293 The unit union operator preserves sethood. (Contributed by SF, 14-Jan-2015.)
A V       1A V

Theoremssetkex 4294 The Kuratowski subset relationship is a set. (Contributed by SF, 13-Jan-2015.)
Sk V

Theoremsikexlem 4295* Lemma for sikexg 4296. Equality for two subsets of 1c squared . (Contributed by SF, 14-Jan-2015.)
A (1c ×k 1c)    &   B (1c ×k 1c)       (A = Bxy(⟪{x}, {y}⟫ A ↔ ⟪{x}, {y}⟫ B))

Theoremsikexg 4296 The Kuratowski singleton image of a set is a set. (Contributed by SF, 14-Jan-2015.)
(A VSIk A V)

Theoremsikex 4297 The Kuratowski singleton image of a set is a set. (Contributed by SF, 14-Jan-2015.)
A V        SIk A V

Theoremdfimak2 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.)
(Ak B) = ∼ P6 ( ∼ (1c ×k V) ∪ SIk ∼ (A ∩ (B ×k V)))

Theoremimakexg 4299 The image of a set under a set is a set. (Contributed by SF, 14-Jan-2015.)
((A V B W) → (Ak B) V)

Theoremimakex 4300 The image of a set under a set is a set. (Contributed by SF, 14-Jan-2015.)
A V    &   B V       (Ak B) V

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6336
 Copyright terms: Public domain < Previous  Next >