Home New Foundations ExplorerTheorem List (p. 32 of 56) < Previous  Next > Bad symbols? Use Firefox (or GIF version for IE).

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

Theoremint0el 3101 The intersection of a class containing the empty set is empty.
( AA = )

Theoremintun 3102 The class intersection of the union of two classes. Theorem 78 of [Suppes] p. 42.
(AB) = (AB)

Theoremintpr 3103 The intersection of a pair is the intersection of its members. Theorem 71 of [Suppes] p. 42.
A V    &   B V       {A, B} = (AB)

Theoremintprg 3104 The intersection of a pair is the intersection of its members. Closed form of intpr 3103. Theorem 71 of [Suppes] p. 42. (Contributed by FL, 27-Apr-2008.)
((A V B W) → {A, B} = (AB))

Theoremintsn 3105 The intersection of a singleton is its member. Theorem 70 of [Suppes] p. 41.
A V       {A} = A

Theoremuniintsn 3106* Two ways to express "A is a singleton."
(A = Ax A = {x})

Theoremintunsn 3107 Theorem joining a singleton to an intersection.
B V       (A ∪ {B}) = (AB)

2.1.16  "Weak deduction theorem" for set theory

Syntaxcif 3108 Extend class notation to include the conditional operator. See df-if 3109 for a description. (In older databases this was denoted "ded".)
class if(φ, A, B)

Definitiondf-if 3109* Define the conditional operator. Read if(φ, A, B) as "if φ then A else B." See iftrue 3114 and iffalse 3115 for its values. In mathematical literature, this operator is rarely defined formally but is implicit in informal definitions such as "let f(x)=0 if x=0 and 1/x otherwise." (In older versions of this database, this operator was denoted "ded" and called the "deduction class.")

An important use for us is in conjunction with the weak deduction theorem, which converts a hypothesis into an antecedent. In that role, A is a class variable in the hypothesis and B is a class (usually a constant) that makes the hypothesis true when it is substituted for A. See dedth 3146 for the main part of the weak deduction theorem, elimhyp 3153 to eliminate a hypothesis, and keephyp 3159 to keep a hypothesis. See the Deduction Theorem link on the Metamath Proof Explorer Home Page for a description of the weak deduction theorem.

if(φ, A, B) = {x ((x A φ) (x B ¬ φ))}

Theoremdfif2 3110* An alternate definition of the conditional operator df-if 3109 with one fewer connectives (but probably less intuitive to understand).
if(φ, A, B) = {x ((x Bφ) → (x A φ))}

Theoremdfif6 3111* An alternate definition of the conditional operator df-if 3109 as a simple class abstraction.
if(φ, A, B) = ({x A φ} ∪ {x B ¬ φ})

Theoremifeq1 3112 Equality theorem for conditional operator. (The proof was shortened by Andrew Salmon, 26-Jun-2011.)
(A = B → if(φ, A, C) = if(φ, B, C))

Theoremifeq2 3113 Equality theorem for conditional operator. (The proof was shortened by Andrew Salmon, 26-Jun-2011.)
(A = B → if(φ, C, A) = if(φ, C, B))

Theoremiftrue 3114 Value of the conditional operator when its first argument is true. (The proof was shortened by Andrew Salmon, 26-Jun-2011.)
(φ → if(φ, A, B) = A)

Theoremiffalse 3115 Value of the conditional operator when its first argument is false.
φ → if(φ, A, B) = B)

Theoremifsb 3116 Distribute a function over an if-clause. (Contributed by Mario Carneiro, 14-Aug-2013.)
( if(φ, A, B) = AC = D)    &   ( if(φ, A, B) = BC = E)       C = if(φ, D, E)

Theoremdfif3 3117* Alternate definition of the conditional operator df-if 3109. Note that φ is independent of x i.e. a constant true or false.
C = {x φ}        if(φ, A, B) = ((AC) ∪ (B ∩ (V C)))

Theoremdfif4 3118* Alternate definition of the conditional operator df-if 3109. Note that φ is independent of x i.e. a constant true or false.
C = {x φ}        if(φ, A, B) = ((AB) ∩ ((A ∪ (V C)) ∩ (BC)))

Theoremdfif5 3119* Alternate definition of the conditional operator df-if 3109. Note that φ is independent of x i.e. a constant true or false (see also abvor0 2744). (Contributed by Gérard Lang, 18-Aug-2013.)
C = {x φ}        if(φ, A, B) = ((AB) ∪ (((A B) ∩ C) ∪ ((B A) ∩ (V C))))

Theoremifeq12 3120 Equality theorem for conditional operators.
((A = B C = D) → if(φ, A, C) = if(φ, B, D))

Theoremifeq1d 3121 Equality deduction for conditional operator.
(φA = B)       (φ → if(ψ, A, C) = if(ψ, B, C))

Theoremifeq2d 3122 Equality deduction for conditional operator.
(φA = B)       (φ → if(ψ, C, A) = if(ψ, C, B))

Theoremifbi 3123 Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.)
((φψ) → if(φ, A, B) = if(ψ, A, B))

Theoremifbid 3124 Equivalence deduction for conditional operators.
(φ → (ψχ))       (φ → if(ψ, A, B) = if(χ, A, B))

Theoremifbieq2i 3125 Equivalence/equality inference for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)
(φψ)    &   A = B        if(φ, C, A) = if(ψ, C, B)

Theoremifbieq2d 3126 Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)
(φ → (ψχ))    &   (φA = B)       (φ → if(ψ, C, A) = if(χ, C, B))

Theoremifbieq12i 3127 Equivalence deduction for conditional operators.
(φψ)    &   A = C    &   B = D        if(φ, A, B) = if(ψ, C, D)

Theoremifbieq12d 3128 Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.)
(φ → (ψχ))    &   (φA = C)    &   (φB = D)       (φ → if(ψ, A, B) = if(χ, C, D))

Theoremhbif 3129* Bound-variable hypothesis builder for a conditional operator. (The proof was shortened by Andrew Salmon, 26-Jun-2011.)
(φxφ)    &   (y Ax y A)    &   (y Bx y B)       (y if(φ, A, B) → x y if(φ, A, B))

Theoremhbifd 3130* Deduction version of hbif 3129.
(φxφ)    &   (φ → (ψxψ))    &   (φ → (y Ax y A))    &   (φ → (y Bx y B))       (φ → (y if(ψ, A, B) → x y if(ψ, A, B)))

Theoremifeq1da 3131 Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)
((φ ψ) → A = B)       (φ → if(ψ, A, C) = if(ψ, B, C))

Theoremifeq2da 3132 Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)
((φ ¬ ψ) → A = B)       (φ → if(ψ, C, A) = if(ψ, C, B))

Theoremifclda 3133 Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.)
((φ ψ) → A C)    &   ((φ ¬ ψ) → B C)       (φ → if(ψ, A, B) C)

Theoremcsbifg 3134 Distribute proper substitution through the conditional operator.
(A V[A / x] if(φ, B, C) = if([A / x]φ, [A / x]B, [A / x]C))

Theoremelimif 3135 Elimination of a conditional operator contained in a wff ψ.
( if(φ, A, B) = A → (ψχ))    &   ( if(φ, A, B) = B → (ψθ))       (ψ ↔ ((φ χ) φ θ)))

Theoremifboth 3136 A wff θ containing a conditional operator is true when both of its cases are true.
(A = if(φ, A, B) → (ψθ))    &   (B = if(φ, A, B) → (χθ))       ((ψ χ) → θ)

Theoremifid 3137 Identical true and false arguments in the conditional operator.
if(φ, A, A) = A

Theoremeqif 3138 Expansion of an equality with a conditional operator.
(A = if(φ, B, C) ↔ ((φ A = B) φ A = C)))

Theoremelif 3139 Membership in a conditional operator.
(A if(φ, B, C) ↔ ((φ A B) φ A C)))

Theoremifel 3140 Membership of a conditional operator.
( if(φ, A, B) C ↔ ((φ A C) φ B C)))

Theoremifcl 3141 Membership (closure) of a conditional operator.
((A C B C) → if(φ, A, B) C)

Theoremifeqor 3142 The possible values of a conditional operator. (The proof was shortened by Andrew Salmon, 26-Jun-2011.)
( if(φ, A, B) = A if(φ, A, B) = B)

Theoremifnot 3143 Negating the first argument swaps the last two arguments of a conditional operator.
if(¬ φ, A, B) = if(φ, B, A)

Theoremifan 3144 Rewrite a conjunction in an if statement as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.)
if((φ ψ), A, B) = if(φ, if(ψ, A, B), B)

Theoremifor 3145 Rewrite a disjunction in an if statement as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.)
if((φ ψ), A, B) = if(φ, A, if(ψ, A, B))

Theoremdedth 3146 Weak deduction theorem that eliminates a hypothesis φ, making it become an antecedent. We assume that a proof exists for φ when the class variable A is replaced with a specific class B. The hypothesis χ should be assigned to the inference, and the inference's hypothesis eliminated with elimhyp 3153. If the inference has other hypotheses with class variable A, these can be kept by assigning keephyp 3159 to them. For more information, see the Deduction Theorem http://us.metamath.org/mpegif/mmdeduction.html.
(A = if(φ, A, B) → (ψχ))    &   χ       (φψ)

Theoremdedth2h 3147 Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 3150 but requires that each hypothesis has exactly one class variable. See also comments in dedth 3146.
(A = if(φ, A, C) → (χθ))    &   (B = if(ψ, B, D) → (θτ))    &   τ       ((φ ψ) → χ)

Theoremdedth3h 3148 Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 3147.
(A = if(φ, A, D) → (θτ))    &   (B = if(ψ, B, R) → (τη))    &   (C = if(χ, C, S) → (ηζ))    &   ζ       ((φ ψ χ) → θ)

Theoremdedth4h 3149 Weak deduction theorem eliminating four hypotheses. See comments in dedth2h 3147.
(A = if(φ, A, R) → (τη))    &   (B = if(ψ, B, S) → (ηζ))    &   (C = if(χ, C, F) → (ζσ))    &   (D = if(θ, D, G) → (σρ))    &   ρ       (((φ ψ) (χ θ)) → τ)

Theoremdedth2v 3150 Weak deduction theorem for eliminating a hypothesis with 2 class variables. Note: if the hypothesis can be separated into two hypotheses, each with one class variable, then dedth2h 3147 is simpler to use. See also comments in dedth 3146. (The proof was shortened by Eric Schmidt, 28-Jul-2009.)
(A = if(φ, A, C) → (ψχ))    &   (B = if(φ, B, D) → (χθ))    &   θ       (φψ)

Theoremdedth3v 3151 Weak deduction theorem for eliminating a hypothesis with 3 class variables. See comments in dedth2v 3150. (The proof was shortened by Eric Schmidt, 28-Jul-2009.)
(A = if(φ, A, D) → (ψχ))    &   (B = if(φ, B, R) → (χθ))    &   (C = if(φ, C, S) → (θτ))    &   τ       (φψ)

Theoremdedth4v 3152 Weak deduction theorem for eliminating a hypothesis with 4 class variables. See comments in dedth2v 3150. (The proof was shortened by Eric Schmidt, 28-Jul-2009.)
(A = if(φ, A, R) → (ψχ))    &   (B = if(φ, B, S) → (χθ))    &   (C = if(φ, C, T) → (θτ))    &   (D = if(φ, D, U) → (τη))    &   η       (φψ)

Theoremelimhyp 3153 Eliminate a hypothesis containing class variable A when it is known for a specific class B. For more information, see comments in dedth 3146.
(A = if(φ, A, B) → (φψ))    &   (B = if(φ, A, B) → (χψ))    &   χ       ψ

Theoremelimhyp2v 3154 Eliminate a hypothesis containing 2 class variables.
(A = if(φ, A, C) → (φχ))    &   (B = if(φ, B, D) → (χθ))    &   (C = if(φ, A, C) → (τη))    &   (D = if(φ, B, D) → (ηθ))    &   τ       θ

Theoremelimhyp3v 3155 Eliminate a hypothesis containing 3 class variables.
(A = if(φ, A, D) → (φχ))    &   (B = if(φ, B, R) → (χθ))    &   (C = if(φ, C, S) → (θτ))    &   (D = if(φ, A, D) → (ηζ))    &   (R = if(φ, B, R) → (ζσ))    &   (S = if(φ, C, S) → (στ))    &   η       τ

Theoremelimhyp4v 3156 Eliminate a hypothesis containing 4 class variables (for use with the weak deduction theorem dedth 3146).
(A = if(φ, A, D) → (φχ))    &   (B = if(φ, B, R) → (χθ))    &   (C = if(φ, C, S) → (θτ))    &   (F = if(φ, F, G) → (τψ))    &   (D = if(φ, A, D) → (ηζ))    &   (R = if(φ, B, R) → (ζσ))    &   (S = if(φ, C, S) → (σρ))    &   (G = if(φ, F, G) → (ρψ))    &   η       ψ

Theoremelimel 3157 Eliminate a membership hypothesis for weak deduction theorem, when special case B C is provable.
B C        if(A C, A, B) C

Theoremelimdhyp 3158 Version of elimhyp 3153 where the hypothesis is deduced from the final antecedent. (Contributed by Paul Chapman, 25-Mar-2008.)
(φψ)    &   (A = if(φ, A, B) → (ψχ))    &   (B = if(φ, A, B) → (θχ))    &   θ       χ

Theoremkeephyp 3159 Transform a hypothesis ψ that we want to keep (but contains the same class variable A used in the eliminated hypothesis) for use with the weak deduction theorem.
(A = if(φ, A, B) → (ψθ))    &   (B = if(φ, A, B) → (χθ))    &   ψ    &   χ       θ

Theoremkeephyp2v 3160 Keep a hypothesis containing 2 class variables (for use with the weak deduction theorem dedth 3146).
(A = if(φ, A, C) → (ψχ))    &   (B = if(φ, B, D) → (χθ))    &   (C = if(φ, A, C) → (τη))    &   (D = if(φ, B, D) → (ηθ))    &   ψ    &   τ       θ

Theoremkeephyp3v 3161 Keep a hypothesis containing 3 class variables.
(A = if(φ, A, D) → (ρχ))    &   (B = if(φ, B, R) → (χθ))    &   (C = if(φ, C, S) → (θτ))    &   (D = if(φ, A, D) → (ηζ))    &   (R = if(φ, B, R) → (ζσ))    &   (S = if(φ, C, S) → (στ))    &   ρ    &   η       τ

Theoremkeepel 3162 Keep a membership hypothesis for weak deduction theorem, when special case B C is provable.
A C    &   B C        if(φ, A, B) C

Theoremifex 3163 Conditional operator existence.
A V    &   B V        if(φ, A, B) V

Theoremifexg 3164 Conditional operator existence.
((A V B W) → if(φ, A, B) V)

2.1.17  Power classes

Syntaxcpw 3165 Extend class notation to include power class. (The tilde in the Metamath token is meant to suggest the calligraphic font of the P.)
class A

Theorempwjust 3166* Soundness justification theorem for df-pw 3167. (Contributed by Rodolfo Medina, 28-Apr-2010.) (The proof was shortened by Andrew Salmon, 29-Jun-2011.)
{x x A} = {y y A}

Definitiondf-pw 3167* Define power class. Definition 5.10 of [TakeutiZaring] p. 17, but we also let it apply to proper classes, i.e. those that are not members of V.
A = {x x A}

Theorempweq 3168 Equality theorem for power class.
(A = BA = B)

Theorempweqi 3169 Equality inference for power class.
A = B       A = B

Theorempweqd 3170 Equality deduction for power class.
(φA = B)       (φA = B)

Theoremelpw 3171 Membership in a power class. Theorem 86 of [Suppes] p. 47.
A V       (A BA B)

Theoremelpwg 3172 Membership in a power class. Theorem 86 of [Suppes] p. 47.
(A V → (A BA B))

Theoremelpwi 3173 Subset relation implied by membership in a power class.
(A BA B)

Theoremelelpwi 3174 If A belongs to a part of C then A belongs to C. (Contributed by FL, 3-Aug-2009.)
((A B B C) → A C)

Theoremhbpw 3175* Bound-variable hypothesis builder for power class.
(y Ax y A)       (y Ax y A)

Theorempwid 3176 A set is a member of its power class. Theorem 87 of [Suppes] p. 47.
A V       A A

Theorempwss 3177* Subclass relationship for power class.
(A Bx(x Ax B))

Theorempwsn 3178 The power set of a singleton.
{A} = {, {A}}

Theorempwv 3179 The power class of the universe is the universe.
V = V

2.2  NF Set Theory - add the Set Construction Axioms

2.2.1  Introduce the set construction axioms

Axiomax-nin 3180* State the axiom of anti-intersection. Axiom P1 of {{Hailperin}}. This axiom sets up boolean operations on sets.

Note on this and the following axioms: this axiom, ax-xp 3181, ax-cnv 3182, ax-1c 3183, ax-sset 3184, ax-si 3185, ax-ins2 3186, ax-ins3 3187, and ax-typlower 3188 are from {{Hailperin}}, and are designed to implement the Stratification Axiom from {{Quine2}}.

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.

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

Axiomax-xp 3181* State the axiom of cross product. This axiom guarantees the existence of the (Kuratowski) cross product of V with x. Axiom P5 of {{Hailperin}}.
yz(z ywt(z = ⟪w, t t x))

Axiomax-cnv 3182* State the axiom of converse. This axiom guarantees the existence of the Kuratowski converse of x. Axiom P7 of {{Hailperin}}.
yzw(⟪z, w y ↔ ⟪w, z x)

Axiomax-1c 3183* 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}}.
xy(y xzw(w yw = z))

Axiomax-sset 3184* 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}}.
xyz(⟪y, z xw(w yw z))

Axiomax-si 3185* 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}}.
yzw(⟪{z}, {w}⟫ y ↔ ⟪z, w x)

Axiomax-ins2 3186* 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}}.
yzwt(⟪{{z}}, ⟪w, t⟫⟫ y ↔ ⟪z, t x)

Axiomax-ins3 3187* 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}}.
yzwt(⟪{{z}}, ⟪w, t⟫⟫ y ↔ ⟪z, w x)

Axiomax-typlower 3188* 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}}.
yz(z yww, {z}⟫ x)

Axiomax-sn 3189* 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.
yz(z yz = x)

2.2.2  Primitive forms for some axioms

Theoremaxprimlem1 3190* Lemma for the primitive axioms. Primitive form of equality to a singleton.
(a = {B} ↔ c(c ac = B))

Theoremaxprimlem2 3191* Lemma for the primitive axioms. Primitive form of equality to a Kuratowski ordered pair.
(a = ⟪B, C⟫ ↔ d(d a ↔ (e(e de = B) f(f d ↔ (f = B f = C)))))

Theoremaxxpprim 3192* ax-xp 3181 presented without any set theory definitions.
yz(z ywt(a(a z ↔ (b(b ab = w) c(c a ↔ (c = w c = t)))) t x))

Theoremaxcnvprim 3193* ax-cnv 3182 presented without any set theory definitions.
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 3194* ax-sset 3184 presented without any set theory definitions.
xyz(a(b(b a ↔ (c(c bc = y) d(d b ↔ (d = y d = z)))) a x) ↔ e(e ye z))

Theoremaxsiprim 3195* ax-si 3185 presented without any set theory definitions.
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 3196* ax-typlower 3188 presented without any set theory definitions.
yz(z ywa(b(b a ↔ (c(c bc = w) d(d b ↔ (d = w e(e de = z))))) a x))

Theoremaxins2prim 3197* ax-ins2 3186 presented without any set theory definitions.
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 3198* ax-ins3 3187 presented without any set theory definitions.
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 3199 The anti-intersection of two sets is a set.
((A V B W) → (AB) V)

Theoremninex 3200 The anti-intersection of two sets is a set.
A V    &   B V       (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-5506
 Copyright terms: Public domain < Previous  Next >