Home | New
Foundations ExplorerTheorem
List (p. 32 of 56)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > NFE Home Page > Theorem List Contents

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | int0el 3101 | The intersection of a class containing the empty set is empty. |

Theorem | intun 3102 | The class intersection of the union of two classes. Theorem 78 of [Suppes] p. 42. |

Theorem | intpr 3103 | The intersection of a pair is the intersection of its members. Theorem 71 of [Suppes] p. 42. |

Theorem | intprg 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.) |

Theorem | intsn 3105 | The intersection of a singleton is its member. Theorem 70 of [Suppes] p. 41. |

Theorem | uniintsn 3106* | Two ways to express " is a singleton." |

Theorem | intunsn 3107 | Theorem joining a singleton to an intersection. |

2.1.16 "Weak deduction theorem" for set
theory | ||

Syntax | cif 3108 | Extend class notation to include the conditional operator. See df-if 3109 for a description. (In older databases this was denoted "ded".) |

Definition | df-if 3109* |
Define the conditional operator. Read as "if
then
else ." 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, is a class variable in the hypothesis and is a class (usually a constant) that makes the hypothesis true when it is substituted for . 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. |

Theorem | dfif2 3110* | An alternate definition of the conditional operator df-if 3109 with one fewer connectives (but probably less intuitive to understand). |

Theorem | dfif6 3111* | An alternate definition of the conditional operator df-if 3109 as a simple class abstraction. |

Theorem | ifeq1 3112 | Equality theorem for conditional operator. (The proof was shortened by Andrew Salmon, 26-Jun-2011.) |

Theorem | ifeq2 3113 | Equality theorem for conditional operator. (The proof was shortened by Andrew Salmon, 26-Jun-2011.) |

Theorem | iftrue 3114 | Value of the conditional operator when its first argument is true. (The proof was shortened by Andrew Salmon, 26-Jun-2011.) |

Theorem | iffalse 3115 | Value of the conditional operator when its first argument is false. |

Theorem | ifsb 3116 | Distribute a function over an if-clause. (Contributed by Mario Carneiro, 14-Aug-2013.) |

Theorem | dfif3 3117* | Alternate definition of the conditional operator df-if 3109. Note that is independent of i.e. a constant true or false. |

Theorem | dfif4 3118* | Alternate definition of the conditional operator df-if 3109. Note that is independent of i.e. a constant true or false. |

Theorem | dfif5 3119* | Alternate definition of the conditional operator df-if 3109. Note that is independent of i.e. a constant true or false (see also abvor0 2744). (Contributed by Gérard Lang, 18-Aug-2013.) |

Theorem | ifeq12 3120 | Equality theorem for conditional operators. |

Theorem | ifeq1d 3121 | Equality deduction for conditional operator. |

Theorem | ifeq2d 3122 | Equality deduction for conditional operator. |

Theorem | ifbi 3123 | Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.) |

Theorem | ifbid 3124 | Equivalence deduction for conditional operators. |

Theorem | ifbieq2i 3125 | Equivalence/equality inference for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.) |

Theorem | ifbieq2d 3126 | Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.) |

Theorem | ifbieq12i 3127 | Equivalence deduction for conditional operators. |

Theorem | ifbieq12d 3128 | Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | hbif 3129* | Bound-variable hypothesis builder for a conditional operator. (The proof was shortened by Andrew Salmon, 26-Jun-2011.) |

Theorem | hbifd 3130* | Deduction version of hbif 3129. |

Theorem | ifeq1da 3131 | Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | ifeq2da 3132 | Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | ifclda 3133 | Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | csbifg 3134 | Distribute proper substitution through the conditional operator. |

Theorem | elimif 3135 | Elimination of a conditional operator contained in a wff . |

Theorem | ifboth 3136 | A wff containing a conditional operator is true when both of its cases are true. |

Theorem | ifid 3137 | Identical true and false arguments in the conditional operator. |

Theorem | eqif 3138 | Expansion of an equality with a conditional operator. |

Theorem | elif 3139 | Membership in a conditional operator. |

Theorem | ifel 3140 | Membership of a conditional operator. |

Theorem | ifcl 3141 | Membership (closure) of a conditional operator. |

Theorem | ifeqor 3142 | The possible values of a conditional operator. (The proof was shortened by Andrew Salmon, 26-Jun-2011.) |

Theorem | ifnot 3143 | Negating the first argument swaps the last two arguments of a conditional operator. |

Theorem | ifan 3144 | Rewrite a conjunction in an if statement as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.) |

Theorem | ifor 3145 | Rewrite a disjunction in an if statement as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.) |

Theorem | dedth 3146 | Weak deduction theorem that eliminates a hypothesis , making it become an antecedent. We assume that a proof exists for when the class variable is replaced with a specific class . 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 , these can be kept by assigning keephyp 3159 to them. For more information, see the Deduction Theorem http://us.metamath.org/mpegif/mmdeduction.html. |

Theorem | dedth2h 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. |

Theorem | dedth3h 3148 | Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 3147. |

Theorem | dedth4h 3149 | Weak deduction theorem eliminating four hypotheses. See comments in dedth2h 3147. |

Theorem | dedth2v 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.) |

Theorem | dedth3v 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.) |

Theorem | dedth4v 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.) |

Theorem | elimhyp 3153 | Eliminate a hypothesis containing class variable when it is known for a specific class . For more information, see comments in dedth 3146. |

Theorem | elimhyp2v 3154 | Eliminate a hypothesis containing 2 class variables. |

Theorem | elimhyp3v 3155 | Eliminate a hypothesis containing 3 class variables. |

Theorem | elimhyp4v 3156 | Eliminate a hypothesis containing 4 class variables (for use with the weak deduction theorem dedth 3146). |

Theorem | elimel 3157 | Eliminate a membership hypothesis for weak deduction theorem, when special case is provable. |

Theorem | elimdhyp 3158 | Version of elimhyp 3153 where the hypothesis is deduced from the final antecedent. (Contributed by Paul Chapman, 25-Mar-2008.) |

Theorem | keephyp 3159 | Transform a hypothesis that we want to keep (but contains the same class variable used in the eliminated hypothesis) for use with the weak deduction theorem. |

Theorem | keephyp2v 3160 | Keep a hypothesis containing 2 class variables (for use with the weak deduction theorem dedth 3146). |

Theorem | keephyp3v 3161 | Keep a hypothesis containing 3 class variables. |

Theorem | keepel 3162 | Keep a membership hypothesis for weak deduction theorem, when special case is provable. |

Theorem | ifex 3163 | Conditional operator existence. |

Theorem | ifexg 3164 | Conditional operator existence. |

2.1.17 Power classes | ||

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

Theorem | pwjust 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.) |

Definition | df-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 . |

Theorem | pweq 3168 | Equality theorem for power class. |

Theorem | pweqi 3169 | Equality inference for power class. |

Theorem | pweqd 3170 | Equality deduction for power class. |

Theorem | elpw 3171 | Membership in a power class. Theorem 86 of [Suppes] p. 47. |

Theorem | elpwg 3172 | Membership in a power class. Theorem 86 of [Suppes] p. 47. |

Theorem | elpwi 3173 | Subset relation implied by membership in a power class. |

Theorem | elelpwi 3174 | If belongs to a part of then belongs to . (Contributed by FL, 3-Aug-2009.) |

Theorem | hbpw 3175* | Bound-variable hypothesis builder for power class. |

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

Theorem | pwss 3177* | Subclass relationship for power class. |

Theorem | pwsn 3178 | The power set of a singleton. |

Theorem | pwv 3179 | The power class of the universe is the universe. |

2.2 NF Set Theory - add the Set Construction
Axioms | ||

2.2.1 Introduce the set construction
axioms | ||

Axiom | ax-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 have the same number, and any formulas of the form have as one less than . 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. |

Axiom | ax-xp 3181* | State the axiom of cross product. This axiom guarantees the existence of the (Kuratowski) cross product of with . Axiom P5 of {{Hailperin}}. |

Axiom | ax-cnv 3182* | State the axiom of converse. This axiom guarantees the existence of the Kuratowski converse of . Axiom P7 of {{Hailperin}}. |

Axiom | ax-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}}. |

Axiom | ax-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}}. |

Axiom | ax-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}}. |

Axiom | ax-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 . Axiom P3 of {{Hailperin}}. |

Axiom | ax-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 . Axiom P4 of {{Hailperin}}. |

Axiom | ax-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}}. |

Axiom | ax-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. |

2.2.2 Primitive forms for some
axioms | ||

Theorem | axprimlem1 3190* | Lemma for the primitive axioms. Primitive form of equality to a singleton. |

Theorem | axprimlem2 3191* | Lemma for the primitive axioms. Primitive form of equality to a Kuratowski ordered pair. |

Theorem | axxpprim 3192* | ax-xp 3181 presented without any set theory definitions. |

Theorem | axcnvprim 3193* | ax-cnv 3182 presented without any set theory definitions. |

Theorem | axssetprim 3194* | ax-sset 3184 presented without any set theory definitions. |

Theorem | axsiprim 3195* | ax-si 3185 presented without any set theory definitions. |

Theorem | axtyplowerprim 3196* | ax-typlower 3188 presented without any set theory definitions. |

Theorem | axins2prim 3197* | ax-ins2 3186 presented without any set theory definitions. |

Theorem | axins3prim 3198* | ax-ins3 3187 presented without any set theory definitions. |

2.2.3 Initial existence theorems | ||

Theorem | ninexg 3199 | The anti-intersection of two sets is a set. |

&ncap | ||

Theorem | ninex 3200 | The anti-intersection of two sets is a set. |

&ncap |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |