 Home New Foundations ExplorerTheorem List (p. 42 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 - 4101-4200   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremunexg 4101 The union of two sets is a set. (Contributed by SF, 12-Jan-2015.)
((A V B W) → (AB) V)

Theoremdifexg 4102 The difference of two sets is a set. (Contributed by SF, 12-Jan-2015.)
((A V B W) → (A B) V)

Theoremsymdifexg 4103 The symmetric difference of two sets is a set. (Contributed by SF, 12-Jan-2015.)
((A V B W) → (AB) V)

Theoremcomplex 4104 The complement of a set is a set. (Contributed by SF, 12-Jan-2015.)
A V       A V

Theoreminex 4105 The intersection of two sets is a set. (Contributed by SF, 12-Jan-2015.)
A V    &   B V       (AB) V

Theoremunex 4106 The union of two sets is a set. (Contributed by SF, 12-Jan-2015.)
A V    &   B V       (AB) V

Theoremdifex 4107 The difference of two sets is a set. (Contributed by SF, 12-Jan-2015.)
A V    &   B V       (A B) V

Theoremsymdifex 4108 The symmetric difference of two sets is a set. (Contributed by SF, 12-Jan-2015.)
A V    &   B V       (AB) V

Theoremvvex 4109 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 V

Theorem0ex 4110 The empty class exists. (Contributed by SF, 12-Jan-2015.)
V

Theoremsnex 4111 A singleton always exists. (Contributed by SF, 12-Jan-2015.)
{A} V

Theoremprex 4112 An unordered pair exists. (Contributed by SF, 12-Jan-2015.)
{A, B} V

Theoremopkex 4113 A Kuratowski ordered pair exists. (Contributed by SF, 12-Jan-2015.)
A, B V

Theoremsnelpwg 4114 A singleton of a set belongs to a power class of a set containing it. (Contributed by SF, 1-Feb-2015.)
(A V → ({A} BA B))

Theoremsnelpw 4115 A singleton of a set belongs to a power class of a set containing it. (Contributed by SF, 1-Feb-2015.)
A V       ({A} BA B)

Theoremsnelpwi 4116 A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.)
(A B → {A} B)

Theoremunipw 4117 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.)
A = A

Theoremsspwb 4118 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 BA B)

Theorempwadjoin 4119* Compute the power class of an adjoinment. (Contributed by SF, 30-Jan-2015.)
(A ∪ {X}) = (A ∪ {a b Aa = (b ∪ {X})})

2.2.4  Singletons and pairs (continued)

Theoremsnprss1 4120 A singleton is a subset of an unordered pair. (Contributed by SF, 12-Jan-2015.)
{A} {A, B}

Theoremsnprss2 4121 A singleton is a subset of an unordered pair. (Contributed by SF, 12-Jan-2015.)
{A} {B, A}

Theoremprprc2 4122 An unordered pair of a proper class. (Contributed by SF, 12-Jan-2015.)
A V → {B, A} = {B})

Theoremprprc1 4123 An unordered pair of a proper class. (Contributed by SF, 12-Jan-2015.)
A V → {A, B} = {B})

Theorempreqr1 4124 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 V    &   B V       ({A, C} = {B, C} → A = B)

Theorempreqr2 4125 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 V    &   B V       ({C, A} = {C, B} → A = B)

Theorempreqr2g 4126 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 V B W) → ({C, A} = {C, B} → A = B))

Theorempreq12b 4127 Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996.)
A V    &   B V    &   C V    &   D V       ({A, B} = {C, D} ↔ ((A = C B = D) (A = D B = C)))

Theorempreq12bg 4128 Closed form of preq12b 4127. (Contributed by Scott Fenton, 28-Mar-2014.)
(((A V B W) (C X D Y)) → ({A, B} = {C, D} ↔ ((A = C B = D) (A = D B = C))))

2.2.5  Kuratowski ordered pairs (continued)

Theoremelopk 4129 Membership in a Kuratowski ordered pair. (Contributed by SF, 12-Jan-2015.)
(A B, C⟫ ↔ (A = {B} A = {B, C}))

Theoremopkth1g 4130 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 V A, B⟫ = ⟪C, D⟫) → A = C)

Theoremopkthg 4131 Two Kuratowski ordered pairs are equal iff their components are equal. (Contributed by SF, 12-Jan-2015.)
((A V B W D T) → (⟪A, B⟫ = ⟪C, D⟫ ↔ (A = C B = D)))

Theoremopkth 4132 Two Kuratowski ordered pairs are equal iff their components are equal. (Contributed by SF, 12-Jan-2015.)
A V    &   B V    &   D V       (⟪A, B⟫ = ⟪C, D⟫ ↔ (A = C B = D))

2.2.6  Cardinal one, unit unions, and unit power classes

Syntaxcuni1 4133 Extend class notation to include the unit union of a class (read: 'unit union A')
class 1A

Syntaxc1c 4134 Extend the definition of a class to include cardinal one.
class 1c

Syntaxcpw1 4135 Extend class notation to include unit power class.
class 1A

Definitiondf-1c 4136* 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 y x = {y}}

Definitiondf-pw1 4137 Define unit power class. Definition from [Rosser] p. 252. (Contributed by SF, 12-Jan-2015.)
1A = (A ∩ 1c)

Definitiondf-uni1 4138 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 4173 for membership condition. (Contributed by SF, 12-Jan-2015.)
1A = (A ∩ 1c)

Theoremel1c 4139* Membership in cardinal one. (Contributed by SF, 12-Jan-2015.)
(A 1cx A = {x})

Theoremsnel1c 4140 A singleton is an element of cardinal one. (Contributed by SF, 13-Jan-2015.)
A V       {A} 1c

Theoremsnel1cg 4141 A singleton is an element of cardinal one. (Contributed by SF, 30-Jan-2015.)
(A V → {A} 1c)

Theorem1cex 4142 Cardinal one is a set. (Contributed by SF, 12-Jan-2015.)
1c V

Theorempw1eq 4143 Equality theorem for unit power class. (Contributed by SF, 12-Jan-2015.)
(A = B1A = 1B)

Theoremelpw1 4144* Membership in a unit power class. (Contributed by SF, 13-Jan-2015.)
(A 1Bx B A = {x})

Theoremelpw12 4145* Membership in a unit power class applied twice. (Contributed by SF, 15-Jan-2015.)
(A 11Bx B A = {{x}})

Theoremsnelpw1 4146 Membership of a singleton in a unit power class. (Contributed by SF, 13-Jan-2015.)
({A} 1BA B)

Theoremelpw11c 4147* Membership in 11c (Contributed by SF, 13-Jan-2015.)
(A 11cx A = {{x}})

Theoremelpw121c 4148* Membership in 111c (Contributed by SF, 13-Jan-2015.)
(A 111cx A = {{{x}}})

Theoremelpw131c 4149* Membership in 1111c (Contributed by SF, 14-Jan-2015.)
(A 1111cx A = {{{{x}}}})

Theoremelpw141c 4150* Membership in 11111c (Contributed by SF, 14-Jan-2015.)
(A 11111cx A = {{{{{x}}}}})

Theoremelpw151c 4151* Membership in 111111c (Contributed by SF, 14-Jan-2015.)
(A 111111cx A = {{{{{{x}}}}}})

Theoremelpw161c 4152* Membership in 1111111c (Contributed by SF, 14-Jan-2015.)
(A 1111111cx A = {{{{{{{x}}}}}}})

Theoremelpw171c 4153* Membership in 11111111c (Contributed by SF, 15-Jan-2015.)
(A 11111111cx A = {{{{{{{{x}}}}}}}})

Theoremelpw181c 4154* Membership in 111111111c (Contributed by SF, 15-Jan-2015.)
(A 111111111cx A = {{{{{{{{{x}}}}}}}}})

Theoremelpw191c 4155* Membership in 1111111111c (Contributed by SF, 24-Jan-2015.)
(A 1111111111cx A = {{{{{{{{{{x}}}}}}}}}})

Theoremelpw1101c 4156* Membership in 11111111111c (Contributed by SF, 24-Jan-2015.)
(A 11111111111cx A = {{{{{{{{{{{x}}}}}}}}}}})

Theoremelpw1111c 4157* Membership in 111111111111c (Contributed by SF, 24-Jan-2015.)
(A 111111111111cx A = {{{{{{{{{{{{x}}}}}}}}}}}})

Theorempw1ss1c 4158 A unit power class is a subset of 1c. (Contributed by SF, 22-Jan-2015.)
1A 1c

Theorem0nel1c 4159 The empty class is not a singleton. (Contributed by SF, 22-Jan-2015.)
¬ 1c

Theorempw0 4160 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.)
= {}

Theorempw10 4161 Compute the unit power class of (Contributed by SF, 22-Jan-2015.)
1 =

Theoremeqpw1 4162* A condition for equality to unit power class. (Contributed by SF, 21-Jan-2015.)
(A = 1B ↔ (A 1c x({x} Ax B)))

Theorempw1un 4163 Unit power class distributes over union. (Contributed by SF, 22-Jan-2015.)
1(AB) = (1A1B)

Theorempw1in 4164 Unit power class distributes over intersection. (Contributed by SF, 13-Feb-2015.)
1(AB) = (1A1B)

Theorempw1sn 4165 Compute the unit power class of a singleton. (Contributed by SF, 22-Jan-2015.)
A V       1{A} = {{A}}

Theorempw10b 4166 The unit power class of a class is empty iff the class itself is empty. (Contributed by SF, 22-Jan-2015.)
(1A = A = )

Theorempw1disj 4167 Two unit power classes are disjoint iff the classes themselves are disjoint. (Contributed by SF, 26-Jan-2015.)
((1A1B) = ↔ (AB) = )

Theoremdf1c2 4168 Cardinal one is the unit power class of the universe. (Contributed by SF, 29-Jan-2015.)
1c = 1V

Theorempw1ss 4169 Unit power set preserves subset. (Contributed by SF, 3-Feb-2015.)
(A B1A 1B)

Theorempw111 4170 The unit power class operation is one-to-one. (Contributed by SF, 26-Feb-2015.)
(1A = 1BA = B)

Theorempw1sspw 4171 A unit power class is a subset of a power class. (Contributed by SF, 10-Mar-2015.)
1A A

Theoremeluni1g 4172 Membership in a unit union. (Contributed by SF, 15-Mar-2015.)
(A V → (A 1B ↔ {A} B))

Theoremeluni1 4173 Membership in a unit union. (Contributed by SF, 15-Mar-2015.)
A V       (A 1B ↔ {A} B)

2.2.7  Kuratowski relationships

Syntaxcxpk 4174 Extend the definition of a class to include the Kuratowski cross product.
class (A ×k B)

Syntaxccnvk 4175 Extend the definition of a class to include the Kuratowski converse of a class.
class kA

Syntaxcins2k 4176 Extend the definition of a class to include the Kuratowski second insertion operator.
class Ins2k A

Syntaxcins3k 4177 Extend the definition of a class to include the Kuratowski third insertion operator.
class Ins3k A

Syntaxcp6 4178 Extend the definition of a class to include the P6 operator (the set guaranteed by ax-typlower 4086).
class P6 A

Syntaxcimak 4179 Extend the definition of a class to include the Kuratowski image of a class. (Read: The image of B under A.)
class (Ak B)

Syntaxccomk 4180 Extend the definition of a class to include the Kuratowski composition of two classes. (Read: The composition of A and B.)
class (A k B)

Syntaxcsik 4181 Extend the definition of a class to include the Kuratowski singleton image.
class SIk A

Syntaxcimagek 4182 Extend the definition of a class to include the Kuratowski image functor.
class ImagekA

Syntaxcssetk 4183 Extend the definition of a class to include the Kuratowski subset relationship.
class Sk

Syntaxcidk 4184 Extend the definition of a class to include the Kuratowski identity relationship.
class Ik

Definitiondf-xpk 4185* Define the Kuratowski cross product. This definition through df-idk 4195 set up the Kuratowski relationships. These are used mainly to prove the properties of df-op 4566, and are not used thereafter. (Contributed by SF, 12-Jan-2015.)
(A ×k B) = {x yz(x = ⟪y, z (y A z B))}

Definitiondf-cnvk 4186* Define the Kuratowski converse. (Contributed by SF, 12-Jan-2015.)
kA = {x yz(x = ⟪y, zz, y A)}

Definitiondf-ins2k 4187* Define the Kuratowski second insertion operator. (Contributed by SF, 12-Jan-2015.)
Ins2k A = {x yz(x = ⟪y, z tuv(y = {{t}} z = ⟪u, vt, v A))}

Definitiondf-ins3k 4188* Define the Kuratowski third insertion operator. (Contributed by SF, 12-Jan-2015.)
Ins3k A = {x yz(x = ⟪y, z tuv(y = {{t}} z = ⟪u, vt, u A))}

Definitiondf-imak 4189* Define the Kuratowski image operator. (Contributed by SF, 12-Jan-2015.)
(Ak B) = {x y By, x A}

Definitiondf-cok 4190 Define the Kuratowski composition operator. (Contributed by SF, 12-Jan-2015.)
(A k B) = (( Ins2k AIns3k kB) “k V)

Definitiondf-p6 4191* Define the P6 operator. This is the set guaranteed by ax-typlower 4086. (Contributed by SF, 12-Jan-2015.)
P6 A = {x (V ×k {{x}}) A}

Definitiondf-sik 4192* Define the Kuratowski singleton image operation. (Contributed by SF, 12-Jan-2015.)
SIk A = {x yz(x = ⟪y, z tu(y = {t} z = {u} t, u A))}

Definitiondf-ssetk 4193* Define the Kuratowski subset relationship. (Contributed by SF, 12-Jan-2015.)
Sk = {x yz(x = ⟪y, z y z)}

Definitiondf-imagek 4194 Define the Kuratowski image function. See opkelimagek 4272 for membership. (Contributed by SF, 12-Jan-2015.)
ImagekA = ((V ×k V) (( Ins2k SkIns3k ( Sk k k SIk A)) “k 111c))

Definitiondf-idk 4195* Define the Kuratowski identity relationship. (Contributed by SF, 12-Jan-2015.)
Ik = {x yz(x = ⟪y, z y = z)}

Theoremelxpk 4196* Membership in a Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
(A (B ×k C) ↔ xy(A = ⟪x, y (x B y C)))

Theoremelxpk2 4197* Membership in a cross product. (Contributed by SF, 12-Jan-2015.)
(A (B ×k C) ↔ x B y C A = ⟪x, y⟫)

Theoremxpkeq1 4198 Equality theorem for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
(A = B → (A ×k C) = (B ×k C))

Theoremxpkeq2 4199 Equality theorem for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
(A = B → (C ×k A) = (C ×k B))

Theoremxpkeq12 4200 Equality theorem for Kuratowski cross product. (Contributed by SF, 12-Jan-2015.)
((A = B C = D) → (A ×k C) = (B ×k D))

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-6337
 Copyright terms: Public domain < Previous  Next >