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

Theoremdfiun2 4001* Alternate definition of indexed union when B is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 27-Jun-1998.) (Revised by David Abernethy, 19-Jun-2012.)
B V       x A B = {y x A y = B}

Theoremdfiin2 4002* Alternate definition of indexed intersection when B is a set. Definition 15(b) of [Suppes] p. 44. (Contributed by NM, 28-Jun-1998.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
B V       x A B = {y x A y = B}

Theoremcbviun 4003* Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.)
yB    &   xC    &   (x = yB = C)       x A B = y A C

Theoremcbviin 4004* Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.) (Revised by Mario Carneiro, 14-Oct-2016.)
yB    &   xC    &   (x = yB = C)       x A B = y A C

Theoremcbviunv 4005* Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 15-Sep-2003.)
(x = yB = C)       x A B = y A C

Theoremcbviinv 4006* Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009.)
(x = yB = C)       x A B = y A C

Theoremiunss 4007* Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(x A B Cx A B C)

Theoremssiun 4008* Subset implication for an indexed union. (Contributed by NM, 3-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(x A C BC x A B)

Theoremssiun2 4009 Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(x AB x A B)

Theoremssiun2s 4010* Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.)
(x = CB = D)       (C AD x A B)

Theoremiunss2 4011* A subclass condition on the members of two indexed classes C(x) and D(y) that implies a subclass relation on their indexed unions. Generalization of Proposition 8.6 of [TakeutiZaring] p. 59. Compare uniss2 3922. (Contributed by NM, 9-Dec-2004.)
(x A y B C Dx A C y B D)

Theoremiunab 4012* The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004.)
x A {y φ} = {y x A φ}

Theoremiunrab 4013* The indexed union of a restricted class abstraction. (Contributed by NM, 3-Jan-2004.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
x A {y B φ} = {y B x A φ}

Theoremiunxdif2 4014* Indexed union with a class difference as its index. (Contributed by NM, 10-Dec-2004.)
(x = yC = D)       (x A y (A B)C Dy (A B)D = x A C)

Theoremssiinf 4015 Subset theorem for an indexed intersection. (Contributed by FL, 15-Oct-2012.) (Proof shortened by Mario Carneiro, 14-Oct-2016.)
xC       (C x A Bx A C B)

Theoremssiin 4016* Subset theorem for an indexed intersection. (Contributed by NM, 15-Oct-2003.)
(C x A Bx A C B)

Theoremiinss 4017* Subset implication for an indexed intersection. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(x A B Cx A B C)

Theoremiinss2 4018 An indexed intersection is included in any of its members. (Contributed by FL, 15-Oct-2012.)
(x Ax A B B)

Theoremuniiun 4019* Class union in terms of indexed union. Definition in [Stoll] p. 43. (Contributed by NM, 28-Jun-1998.)
A = x A x

Theoremintiin 4020* Class intersection in terms of indexed intersection. Definition in [Stoll] p. 44. (Contributed by NM, 28-Jun-1998.)
A = x A x

Theoremiunid 4021* An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.)
x A {x} = A

Theoremiun0 4022 An indexed union of the empty set is empty. (Contributed by NM, 26-Mar-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
x A =

Theorem0iun 4023 An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
x A =

Theorem0iin 4024 An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005.)
x A = V

Theoremviin 4025* Indexed intersection with a universal index class. When A doesn't depend on x, this evaluates to A by 19.3 1785 and abid2 2470. When A = x, this evaluates to by intiin 4020 and intv in set.mm. (Contributed by NM, 11-Sep-2008.)
x V A = {y x y A}

Theoremiunn0 4026* There is a non-empty class in an indexed collection B(x) iff the indexed union of them is non-empty. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(x A Bx A B)

Theoremiinab 4027* Indexed intersection of a class builder. (Contributed by NM, 6-Dec-2011.)
x A {y φ} = {y x A φ}

Theoremiinrab 4028* Indexed intersection of a restricted class builder. (Contributed by NM, 6-Dec-2011.)
(Ax A {y B φ} = {y B x A φ})

Theoremiinrab2 4029* Indexed intersection of a restricted class builder. (Contributed by NM, 6-Dec-2011.)
(x A {y B φ} ∩ B) = {y B x A φ}

Theoremiunin2 4030* Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4019 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
x A (BC) = (Bx A C)

Theoremiunin1 4031* Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4019 to recover Enderton's theorem. (Contributed by Mario Carneiro, 30-Aug-2015.)
x A (CB) = (x A CB)

Theoremiinun2 4032* Indexed intersection of union. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4020 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.)
x A (BC) = (Bx A C)

Theoremiundif2 4033* Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use intiin 4020 to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004.)
x A (B C) = (B x A C)

Theorem2iunin 4034* Rearrange indexed unions over intersection. (Contributed by NM, 18-Dec-2008.)
x A y B (CD) = (x A Cy B D)

Theoremiindif2 4035* Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in [Enderton] p. 31. Use uniiun 4019 to recover Enderton's theorem. (Contributed by NM, 5-Oct-2006.)
(Ax A (B C) = (B x A C))

Theoremiinin2 4036* Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4020 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.)
(Ax A (BC) = (Bx A C))

Theoremiinin1 4037* Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use intiin 4020 to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015.)
(Ax A (CB) = (x A CB))

Theoremelriin 4038* Elementhood in a relative intersection. (Contributed by Mario Carneiro, 30-Dec-2016.)
(B (Ax X S) ↔ (B A x X B S))

Theoremriin0 4039* Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
(X = → (Ax X S) = A)

Theoremriinn0 4040* Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015.)
((x X S A X) → (Ax X S) = x X S)

Theoremriinrab 4041* Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015.)
(Ax X {y A φ}) = {y A x X φ}

Theoremiinxsng 4042* A singleton index picks out an instance of an indexed intersection's argument. (Contributed by NM, 15-Jan-2012.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
(x = AB = C)       (A Vx {A}B = C)

Theoremiinxprg 4043* Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012.)
(x = AC = D)    &   (x = BC = E)       ((A V B W) → x {A, B}C = (DE))

Theoremiunxsng 4044* A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016.)
(x = AB = C)       (A Vx {A}B = C)

Theoremiunxsn 4045* A singleton index picks out an instance of an indexed union's argument. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 25-Jun-2016.)
A V    &   (x = AB = C)       x {A}B = C

Theoremiunun 4046 Separate a union in an indexed union. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
x A (BC) = (x A Bx A C)

Theoremiunxun 4047 Separate a union in the index of an indexed union. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
x (AB)C = (x A Cx B C)

Theoremiunxiun 4048* Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016.)
x y A BC = y A x B C

Theoremiinuni 4049* A relationship involving union and indexed intersection. Exercise 23 of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
(AB) = x B (Ax)

Theoremiununi 4050* A relationship involving union and indexed union. Exercise 25 of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
((B = A = ) ↔ (AB) = x B (Ax))

Theoremsspwuni 4051 Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
(A BA B)

Theorempwssb 4052* Two ways to express a collection of subclasses. (Contributed by NM, 19-Jul-2006.)
(A Bx A x B)

Theoremelpwuni 4053 Relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
(B A → (A BA = B))

Theoremiinpw 4054* The power class of an intersection in terms of indexed intersection. Exercise 24(a) of [Enderton] p. 33. (Contributed by NM, 29-Nov-2003.)
A = x A x

Theoremiunpwss 4055* Inclusion of an indexed union of a power class in the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33. (Contributed by NM, 25-Nov-2003.)
x A x A

Theoremrintn0 4056 Relative intersection of a nonempty set. (Contributed by Stefan O'Rear, 3-Apr-2015.) (Revised by Mario Carneiro, 5-Jun-2015.)
((X A X) → (AX) = X)

2.1.20  The Kuratowski ordered pair

Syntaxcopk 4057 Extend class notation to include Kuratowski ordered pair.
class A, B

Definitiondf-opk 4058 Define the Kuratowski ordered pair. This ordered pair definition is standard for ZFC set theory, but we do not use it beyond establishing df-op 4566, since it is not type-level. We state this definition since it is a simple definition that can be used by the set construction axioms that follow this section. (Contributed by SF, 12-Jan-2015.)
A, B⟫ = {{A}, {A, B}}

Theoremopkeq1 4059 Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.)
(A = B → ⟪A, C⟫ = ⟪B, C⟫)

Theoremopkeq2 4060 Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.)
(A = B → ⟪C, A⟫ = ⟪C, B⟫)

Theoremopkeq12 4061 Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
((A = C B = D) → ⟪A, B⟫ = ⟪C, D⟫)

Theoremopkeq1i 4062 Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
A = B       A, C⟫ = ⟪B, C

Theoremopkeq2i 4063 Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
A = B       C, A⟫ = ⟪C, B

Theoremopkeq12i 4064 Equality inference for ordered pairs. (The proof was shortened by Eric Schmidt, 4-Apr-2007.) (Contributed by NM, 16-Dec-2006.)
A = B    &   C = D       A, C⟫ = ⟪B, D

Theoremopkeq1d 4065 Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
(φA = B)       (φ → ⟪A, C⟫ = ⟪B, C⟫)

Theoremopkeq2d 4066 Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
(φA = B)       (φ → ⟪C, A⟫ = ⟪C, B⟫)

Theoremopkeq12d 4067 Equality deduction for ordered pairs. (The proof was shortened by Andrew Salmon, 29-Jun-2011.) (Contributed by NM, 16-Dec-2006.)
(φA = B)    &   (φC = D)       (φ → ⟪A, C⟫ = ⟪B, D⟫)

Theoremnfopk 4068 Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.)
xA    &   xB       xA, B

2.1.21  More Boolean set operations

Theoremcompldif 4069 Complement in terms of difference. (Contributed by SF, 2-Jan-2018.)
A = (V A)

TheoremcomplV 4070 The complement of the universe is the empty set. (Contributed by SF, 2-Jan-2018.)
∼ V =

Theoremcompl0 4071 The complement of the empty set is the universe. (Contributed by SF, 2-Jan-2018.)
= V

Theoremnincompl 4072 Anti-intersection with complement. (Contributed by SF, 2-Jan-2018.)
(A ⩃ ∼ A) = V

Theoremincompl 4073 Intersection with complement. (Contributed by SF, 2-Jan-2018.)
(A ∩ ∼ A) =

Theoremuncompl 4074 Union with complement. (Contributed by SF, 2-Jan-2018.)
(A ∪ ∼ A) = V

Theoreminindif 4075 The intersection of an intersection and a difference is empty. (Contributed by set.mm contributors, 10-Mar-2015.)
((AB) ∩ (A B)) =

Theoremssofss 4076* Condition for subset when A is already known to be a subset. (Contributed by SF, 13-Jan-2015.)
(A C → (A Bx C (x Ax B)))

Theoremssofeq 4077* When A and B are subsets of C, equality depends only on the elements of C. (Contributed by SF, 13-Jan-2015.)
((A C B C) → (A = Bx C (x Ax B)))

2.2  NF Set Theory - add the Set Construction Axioms

2.2.1  Introduce the set construction axioms

Axiomax-nin 4078* State the axiom of anti-intersection. Axiom P1 of [Hailperin] p. 6. This axiom sets up boolean operations on sets.

Note on this and the following axioms: this axiom, ax-xp 4079, ax-cnv 4080, ax-1c 4081, ax-sset 4082, ax-si 4083, ax-ins2 4084, ax-ins3 4085, and ax-typlower 4086 are from Hailperin and are designed to implement the Stratification Axiom of Quine.

A well-formed formula using only propositional symbols, predicate symbols, and is "stratified" iff you can make a (metalogical) mapping from the variables to the natural numbers such that any formulas of the form x = y have the same number, and any formulas of the form x y have x as one less than y. Quine's stratification axiom states that there is a set corresponding to any stratified formula.

Since we cannot state stratification from within the logic, we use Hailperin's axioms and prove existence of stratified sets using Hailperin's algorithm. (Contributed by SF, 12-Jan-2015.)

zw(w z ↔ (w x w y))

Axiomax-xp 4079* State the axiom of cross product. This axiom guarantees the existence of the (Kuratowski) cross product of V with x. Axiom P5 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
yz(z ywt(z = ⟪w, t t x))

Axiomax-cnv 4080* State the axiom of converse. This axiom guarantees the existence of the Kuratowski converse of x. Axiom P7 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
yzw(⟪z, w y ↔ ⟪w, z x)

Axiomax-1c 4081* State the axiom of cardinal one. This axiom guarantees the existence of the set of all singletons, which will become cardinal one later in our development. Axiom P8 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
xy(y xzw(w yw = z))

Axiomax-sset 4082* State the axiom of the subset relationship. This axiom guarantees the existence of the Kuratowski relationship representing subset. Slight generalization of axiom P9 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
xyz(⟪y, z xw(w yw z))

Axiomax-si 4083* State the axiom of the singleton image. This axiom guarantees that guarantees the existence of a set that raises the "type" of another set when considered as a relationship. Axiom P2 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
yzw(⟪{z}, {w}⟫ y ↔ ⟪z, w x)

Axiomax-ins2 4084* State the insertion two axiom. This axiom sets up a set that inserts an extra variable at the second place of the relationship described by x. Axiom P3 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
yzwt(⟪{{z}}, ⟪w, t⟫⟫ y ↔ ⟪z, t x)

Axiomax-ins3 4085* State the insertion three axiom. This axiom sets up a set that inserts an extra variable at the third place of the relationship described by x. Axiom P4 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
yzwt(⟪{{z}}, ⟪w, t⟫⟫ y ↔ ⟪z, w x)

Axiomax-typlower 4086* The type lowering axiom. This axiom eventually sets up both the existence of the sum set and the existence of the range of a relationship. Axiom P6 of [Hailperin] p. 10. (Contributed by SF, 12-Jan-2015.)
yz(z yww, {z}⟫ x)

Axiomax-sn 4087* The singleton axiom. This axiom sets up the existence of a singleton set. This appears to have been an oversight on Hailperin's part, as it is needed to prove the properties of Kuratowski ordered pairs. (Contributed by SF, 12-Jan-2015.)
yz(z yz = x)

2.2.2  Primitive forms for some axioms

Theoremaxprimlem1 4088* Lemma for the primitive axioms. Primitive form of equality to a singleton. (Contributed by SF, 25-Mar-2015.)
(a = {B} ↔ c(c ac = B))

Theoremaxprimlem2 4089* Lemma for the primitive axioms. Primitive form of equality to a Kuratowski ordered pair. (Contributed by SF, 25-Mar-2015.)
(a = ⟪B, C⟫ ↔ d(d a ↔ (e(e de = B) f(f d ↔ (f = B f = C)))))

Theoremaxxpprim 4090* ax-xp 4079 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
yz(z ywt(a(a z ↔ (b(b ab = w) c(c a ↔ (c = w c = t)))) t x))

Theoremaxcnvprim 4091* ax-cnv 4080 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
yzw(a(b(b a ↔ (c(c bc = z) d(d b ↔ (d = z d = w)))) a y) ↔ e(f(f e ↔ (g(g fg = w) h(h f ↔ (h = w h = z)))) e x))

Theoremaxssetprim 4092* ax-sset 4082 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
xyz(a(b(b a ↔ (c(c bc = y) d(d b ↔ (d = y d = z)))) a x) ↔ e(e ye z))

Theoremaxsiprim 4093* ax-si 4083 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
yzw(a(b(b a ↔ (c(c bd(d cd = z)) e(e b ↔ (f(f ef = z) g(g eg = w))))) a y) ↔ h(i(i h ↔ (j(j ij = z) k(k i ↔ (k = z k = w)))) h x))

Theoremaxtyplowerprim 4094* ax-typlower 4086 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
yz(z ywa(b(b a ↔ (c(c bc = w) d(d b ↔ (d = w e(e de = z))))) a x))

Theoremaxins2prim 4095* ax-ins2 4084 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
yzwt(a(b(b a ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))) a y) ↔ k(l(l k ↔ (m(m lm = z) n(n l ↔ (n = z n = t)))) k x))

Theoremaxins3prim 4096* ax-ins3 4085 presented without any set theory definitions. (Contributed by SF, 25-Mar-2015.)
yzwt(a(b(b a ↔ (c(c bd(d ce(e de = z))) f(f b ↔ (g(g fe(e ge = z)) h(h f ↔ (i(i hi = w) j(j h ↔ (j = w j = t)))))))) a y) ↔ k(l(l k ↔ (m(m lm = z) n(n l ↔ (n = z n = w)))) k x))

2.2.3  Initial existence theorems

Theoremninexg 4097 The anti-intersection of two sets is a set. (Contributed by SF, 12-Jan-2015.)
((A V B W) → (AB) V)

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

Theoremcomplexg 4099 The complement of a set is a set. (Contributed by SF, 12-Jan-2015.)
(A V → ∼ A V)

Theoreminexg 4100 The intersection of two sets is a set. (Contributed by SF, 12-Jan-2015.)
((A V B W) → (AB) 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-6337
 Copyright terms: Public domain < Previous  Next >