Home | Metamath
Proof Explorer Theorem List (p. 46 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfif5 4501* | Alternate definition of the conditional operator df-if 4486. Note that π is independent of π₯ i.e. a constant true or false (see also ab0orv 4337). (Contributed by GΓ©rard Lang, 18-Aug-2013.) |
β’ πΆ = {π₯ β£ π} β β’ if(π, π΄, π΅) = ((π΄ β© π΅) βͺ (((π΄ β π΅) β© πΆ) βͺ ((π΅ β π΄) β© (V β πΆ)))) | ||
Theorem | ifssun 4502 | A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.) |
β’ if(π, π΄, π΅) β (π΄ βͺ π΅) | ||
Theorem | ifeq12 4503 | Equality theorem for conditional operators. (Contributed by NM, 1-Sep-2004.) |
β’ ((π΄ = π΅ β§ πΆ = π·) β if(π, π΄, πΆ) = if(π, π΅, π·)) | ||
Theorem | ifeq1d 4504 | Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
β’ (π β π΄ = π΅) β β’ (π β if(π, π΄, πΆ) = if(π, π΅, πΆ)) | ||
Theorem | ifeq2d 4505 | Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
β’ (π β π΄ = π΅) β β’ (π β if(π, πΆ, π΄) = if(π, πΆ, π΅)) | ||
Theorem | ifeq12d 4506 | Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.) |
β’ (π β π΄ = π΅) & β’ (π β πΆ = π·) β β’ (π β if(π, π΄, πΆ) = if(π, π΅, π·)) | ||
Theorem | ifbi 4507 | Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.) |
β’ ((π β π) β if(π, π΄, π΅) = if(π, π΄, π΅)) | ||
Theorem | ifbid 4508 | Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.) |
β’ (π β (π β π)) β β’ (π β if(π, π΄, π΅) = if(π, π΄, π΅)) | ||
Theorem | ifbieq1d 4509 | Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.) |
β’ (π β (π β π)) & β’ (π β π΄ = π΅) β β’ (π β if(π, π΄, πΆ) = if(π, π΅, πΆ)) | ||
Theorem | ifbieq2i 4510 | Equivalence/equality inference for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ (π β π) & β’ π΄ = π΅ β β’ if(π, πΆ, π΄) = if(π, πΆ, π΅) | ||
Theorem | ifbieq2d 4511 | Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ (π β (π β π)) & β’ (π β π΄ = π΅) β β’ (π β if(π, πΆ, π΄) = if(π, πΆ, π΅)) | ||
Theorem | ifbieq12i 4512 | Equivalence deduction for conditional operators. (Contributed by NM, 18-Mar-2013.) |
β’ (π β π) & β’ π΄ = πΆ & β’ π΅ = π· β β’ if(π, π΄, π΅) = if(π, πΆ, π·) | ||
Theorem | ifbieq12d 4513 | Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π β (π β π)) & β’ (π β π΄ = πΆ) & β’ (π β π΅ = π·) β β’ (π β if(π, π΄, π΅) = if(π, πΆ, π·)) | ||
Theorem | nfifd 4514 | Deduction form of nfif 4515. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 13-Oct-2016.) |
β’ (π β β²π₯π) & β’ (π β β²π₯π΄) & β’ (π β β²π₯π΅) β β’ (π β β²π₯if(π, π΄, π΅)) | ||
Theorem | nfif 4515 | Bound-variable hypothesis builder for a conditional operator. (Contributed by NM, 16-Feb-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
β’ β²π₯π & β’ β²π₯π΄ & β’ β²π₯π΅ β β’ β²π₯if(π, π΄, π΅) | ||
Theorem | ifeq1da 4516 | Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π β§ π) β π΄ = π΅) β β’ (π β if(π, π΄, πΆ) = if(π, π΅, πΆ)) | ||
Theorem | ifeq2da 4517 | Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π β§ Β¬ π) β π΄ = π΅) β β’ (π β if(π, πΆ, π΄) = if(π, πΆ, π΅)) | ||
Theorem | ifeq12da 4518 | Equivalence deduction for conditional operators. (Contributed by Wolf Lammen, 24-Jun-2021.) |
β’ ((π β§ π) β π΄ = πΆ) & β’ ((π β§ Β¬ π) β π΅ = π·) β β’ (π β if(π, π΄, π΅) = if(π, πΆ, π·)) | ||
Theorem | ifbieq12d2 4519 | Equivalence deduction for conditional operators. (Contributed by Thierry Arnoux, 14-Feb-2017.) (Proof shortened by Wolf Lammen, 24-Jun-2021.) |
β’ (π β (π β π)) & β’ ((π β§ π) β π΄ = πΆ) & β’ ((π β§ Β¬ π) β π΅ = π·) β β’ (π β if(π, π΄, π΅) = if(π, πΆ, π·)) | ||
Theorem | ifclda 4520 | Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π β§ π) β π΄ β πΆ) & β’ ((π β§ Β¬ π) β π΅ β πΆ) β β’ (π β if(π, π΄, π΅) β πΆ) | ||
Theorem | ifeqda 4521 | Separation of the values of the conditional operator. (Contributed by Alexander van der Vekens, 13-Apr-2018.) |
β’ ((π β§ π) β π΄ = πΆ) & β’ ((π β§ Β¬ π) β π΅ = πΆ) β β’ (π β if(π, π΄, π΅) = πΆ) | ||
Theorem | elimif 4522 | Elimination of a conditional operator contained in a wff π. (Contributed by NM, 15-Feb-2005.) (Proof shortened by NM, 25-Apr-2019.) |
β’ (if(π, π΄, π΅) = π΄ β (π β π)) & β’ (if(π, π΄, π΅) = π΅ β (π β π)) β β’ (π β ((π β§ π) β¨ (Β¬ π β§ π))) | ||
Theorem | ifbothda 4523 | A wff π containing a conditional operator is true when both of its cases are true. (Contributed by NM, 15-Feb-2015.) |
β’ (π΄ = if(π, π΄, π΅) β (π β π)) & β’ (π΅ = if(π, π΄, π΅) β (π β π)) & β’ ((π β§ π) β π) & β’ ((π β§ Β¬ π) β π) β β’ (π β π) | ||
Theorem | ifboth 4524 | A wff π containing a conditional operator is true when both of its cases are true. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 15-Feb-2015.) |
β’ (π΄ = if(π, π΄, π΅) β (π β π)) & β’ (π΅ = if(π, π΄, π΅) β (π β π)) β β’ ((π β§ π) β π) | ||
Theorem | ifid 4525 | Identical true and false arguments in the conditional operator. (Contributed by NM, 18-Apr-2005.) |
β’ if(π, π΄, π΄) = π΄ | ||
Theorem | eqif 4526 | Expansion of an equality with a conditional operator. (Contributed by NM, 14-Feb-2005.) |
β’ (π΄ = if(π, π΅, πΆ) β ((π β§ π΄ = π΅) β¨ (Β¬ π β§ π΄ = πΆ))) | ||
Theorem | ifval 4527 | Another expression of the value of the if predicate, analogous to eqif 4526. See also the more specialized iftrue 4491 and iffalse 4494. (Contributed by BJ, 6-Apr-2019.) |
β’ (π΄ = if(π, π΅, πΆ) β ((π β π΄ = π΅) β§ (Β¬ π β π΄ = πΆ))) | ||
Theorem | elif 4528 | Membership in a conditional operator. (Contributed by NM, 14-Feb-2005.) |
β’ (π΄ β if(π, π΅, πΆ) β ((π β§ π΄ β π΅) β¨ (Β¬ π β§ π΄ β πΆ))) | ||
Theorem | ifel 4529 | Membership of a conditional operator. (Contributed by NM, 10-Sep-2005.) |
β’ (if(π, π΄, π΅) β πΆ β ((π β§ π΄ β πΆ) β¨ (Β¬ π β§ π΅ β πΆ))) | ||
Theorem | ifcl 4530 | Membership (closure) of a conditional operator. (Contributed by NM, 4-Apr-2005.) |
β’ ((π΄ β πΆ β§ π΅ β πΆ) β if(π, π΄, π΅) β πΆ) | ||
Theorem | ifcld 4531 | Membership (closure) of a conditional operator, deduction form. (Contributed by SO, 16-Jul-2018.) |
β’ (π β π΄ β πΆ) & β’ (π β π΅ β πΆ) β β’ (π β if(π, π΄, π΅) β πΆ) | ||
Theorem | ifcli 4532 | Inference associated with ifcl 4530. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4543 when the special case π΅ β πΆ is provable. (Contributed by NM, 14-Aug-1999.) (Proof shortened by BJ, 1-Sep-2022.) |
β’ π΄ β πΆ & β’ π΅ β πΆ β β’ if(π, π΄, π΅) β πΆ | ||
Theorem | ifexd 4533 | Existence of the conditional operator (deduction form). (Contributed by SN, 26-Jul-2024.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β if(π, π΄, π΅) β V) | ||
Theorem | ifexg 4534 | Existence of the conditional operator (closed form). (Contributed by NM, 21-Mar-2011.) (Proof shortened by BJ, 1-Sep-2022.) |
β’ ((π΄ β π β§ π΅ β π) β if(π, π΄, π΅) β V) | ||
Theorem | ifex 4535 | Existence of the conditional operator (inference form). (Contributed by NM, 2-Sep-2004.) |
β’ π΄ β V & β’ π΅ β V β β’ if(π, π΄, π΅) β V | ||
Theorem | ifeqor 4536 | The possible values of a conditional operator. (Contributed by NM, 17-Jun-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
β’ (if(π, π΄, π΅) = π΄ β¨ if(π, π΄, π΅) = π΅) | ||
Theorem | ifnot 4537 | Negating the first argument swaps the last two arguments of a conditional operator. (Contributed by NM, 21-Jun-2007.) |
β’ if(Β¬ π, π΄, π΅) = if(π, π΅, π΄) | ||
Theorem | ifan 4538 | Rewrite a conjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.) |
β’ if((π β§ π), π΄, π΅) = if(π, if(π, π΄, π΅), π΅) | ||
Theorem | ifor 4539 | Rewrite a disjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.) |
β’ if((π β¨ π), π΄, π΅) = if(π, π΄, if(π, π΄, π΅)) | ||
Theorem | 2if2 4540 | Resolve two nested conditionals. (Contributed by Alexander van der Vekens, 27-Mar-2018.) |
β’ ((π β§ π) β π· = π΄) & β’ ((π β§ Β¬ π β§ π) β π· = π΅) & β’ ((π β§ Β¬ π β§ Β¬ π) β π· = πΆ) β β’ (π β π· = if(π, π΄, if(π, π΅, πΆ))) | ||
Theorem | ifcomnan 4541 | Commute the conditions in two nested conditionals if both conditions are not simultaneously true. (Contributed by SO, 15-Jul-2018.) |
β’ (Β¬ (π β§ π) β if(π, π΄, if(π, π΅, πΆ)) = if(π, π΅, if(π, π΄, πΆ))) | ||
Theorem | csbif 4542 | Distribute proper substitution through the conditional operator. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 19-Aug-2018.) |
β’ β¦π΄ / π₯β¦if(π, π΅, πΆ) = if([π΄ / π₯]π, β¦π΄ / π₯β¦π΅, β¦π΄ / π₯β¦πΆ) | ||
This subsection contains a few results related to the weak deduction theorem in set theory. For the weak deduction theorem in propositional calculus, see the section beginning with elimh 1084. For more information on the weak deduction theorem, see the Weak Deduction Theorem page mmdeduction.html 1084. In a Hilbert system of logic (which consists of a set of axioms, modus ponens, and the generalization rule), converting a deduction to a proof using the Deduction Theorem (taught in introductory logic books) involves an exponential increase of the number of steps as hypotheses are successively eliminated. Here is a trick that is not as general as the Deduction Theorem but requires only a linear increase in the number of steps. The general problem: We want to convert a deduction P |- Q into a proof of the theorem |- P -> Q i.e., we want to eliminate the hypothesis P. Normally this is done using the Deduction (meta)Theorem, which looks at the microscopic steps of the deduction and usually doubles or triples the number of these microscopic steps for each hypothesis that is eliminated. We will look at a special case of this problem, without appealing to the Deduction Theorem. We assume ZF with class notation. A and B are arbitrary (possibly proper) classes. P, Q, R, S and T are wffs. We define the conditional operator, if(P, A, B), as follows: if(P, A, B) =def= { x | (x \in A & P) v (x \in B & -. P) } (where x does not occur in A, B, or P). Lemma 1. A = if(P, A, B) -> (P <-> R), B = if(P, A, B) -> (S <-> R), S |- R Proof: Logic and Axiom of Extensionality. Lemma 2. A = if(P, A, B) -> (Q <-> T), T |- P -> Q Proof: Logic and Axiom of Extensionality. Here is a simple example that illustrates how it works. Suppose we have a deduction Ord A |- Tr A which means, "Assume A is an ordinal class. Then A is a transitive class." Note that A is a class variable that may be substituted with any class expression, so this is really a deduction scheme. We want to convert this to a proof of the theorem (scheme) |- Ord A -> Tr A. The catch is that we must be able to prove "Ord A" for at least one object A (and this is what makes it weaker than the ordinary Deduction Theorem). However, it is easy to prove |- Ord 0 (the empty set is ordinal). (For a typical textbook "theorem", i.e., deduction, there is usually at least one object satisfying each hypothesis, otherwise the theorem would not be very useful. We can always go back to the standard Deduction Theorem for those hypotheses where this is not the case.) Continuing with the example: Equality axioms (and Extensionality) yield |- A = if(Ord A, A, 0) -> (Ord A <-> Ord if(Ord A, A, 0)) (1) |- 0 = if(Ord A, A, 0) -> (Ord 0 <-> Ord if(Ord A, A, 0)) (2) From (1), (2) and |- Ord 0, Lemma 1 yields |- Ord if(Ord A, A, 0) (3) From (3) and substituting if(Ord A, A, 0) for A in the original deduction, |- Tr if(Ord A, A, 0) (4) Equality axioms (and Extensionality) yield |- A = if(Ord A, A, 0) -> (Tr A <-> Tr if(Ord A, A, 0)) (5) From (4) and (5), Lemma 2 yields |- Ord A -> Tr A (Q.E.D.) | ||
Theorem | dedth 4543 | 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 hypothesis eliminated with elimhyp 4550. If the inference has other hypotheses with class variable π΄, these can be kept by assigning keephyp 4556 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html 4556. (Contributed by NM, 15-May-1999.) |
β’ (π΄ = if(π, π΄, π΅) β (π β π)) & β’ π β β’ (π β π) | ||
Theorem | dedth2h 4544 | Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 4547 but requires that each hypothesis have exactly one class variable. See also comments in dedth 4543. (Contributed by NM, 15-May-1999.) |
β’ (π΄ = if(π, π΄, πΆ) β (π β π)) & β’ (π΅ = if(π, π΅, π·) β (π β π)) & β’ π β β’ ((π β§ π) β π) | ||
Theorem | dedth3h 4545 | Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 4544. (Contributed by NM, 15-May-1999.) |
β’ (π΄ = if(π, π΄, π·) β (π β π)) & β’ (π΅ = if(π, π΅, π ) β (π β π)) & β’ (πΆ = if(π, πΆ, π) β (π β π)) & β’ π β β’ ((π β§ π β§ π) β π) | ||
Theorem | dedth4h 4546 | Weak deduction theorem eliminating four hypotheses. See comments in dedth2h 4544. (Contributed by NM, 16-May-1999.) |
β’ (π΄ = if(π, π΄, π ) β (π β π)) & β’ (π΅ = if(π, π΅, π) β (π β π)) & β’ (πΆ = if(π, πΆ, πΉ) β (π β π)) & β’ (π· = if(π, π·, πΊ) β (π β π)) & β’ π β β’ (((π β§ π) β§ (π β§ π)) β π) | ||
Theorem | dedth2v 4547 | 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 4544 is simpler to use. See also comments in dedth 4543. (Contributed by NM, 13-Aug-1999.) (Proof shortened by Eric Schmidt, 28-Jul-2009.) |
β’ (π΄ = if(π, π΄, πΆ) β (π β π)) & β’ (π΅ = if(π, π΅, π·) β (π β π)) & β’ π β β’ (π β π) | ||
Theorem | dedth3v 4548 | Weak deduction theorem for eliminating a hypothesis with 3 class variables. See comments in dedth2v 4547. (Contributed by NM, 13-Aug-1999.) (Proof shortened by Eric Schmidt, 28-Jul-2009.) |
β’ (π΄ = if(π, π΄, π·) β (π β π)) & β’ (π΅ = if(π, π΅, π ) β (π β π)) & β’ (πΆ = if(π, πΆ, π) β (π β π)) & β’ π β β’ (π β π) | ||
Theorem | dedth4v 4549 | Weak deduction theorem for eliminating a hypothesis with 4 class variables. See comments in dedth2v 4547. (Contributed by NM, 21-Apr-2007.) (Proof shortened by Eric Schmidt, 28-Jul-2009.) |
β’ (π΄ = if(π, π΄, π ) β (π β π)) & β’ (π΅ = if(π, π΅, π) β (π β π)) & β’ (πΆ = if(π, πΆ, π) β (π β π)) & β’ (π· = if(π, π·, π) β (π β π)) & β’ π β β’ (π β π) | ||
Theorem | elimhyp 4550 | Eliminate a hypothesis containing class variable π΄ when it is known for a specific class π΅. For more information, see comments in dedth 4543. (Contributed by NM, 15-May-1999.) |
β’ (π΄ = if(π, π΄, π΅) β (π β π)) & β’ (π΅ = if(π, π΄, π΅) β (π β π)) & β’ π β β’ π | ||
Theorem | elimhyp2v 4551 | Eliminate a hypothesis containing 2 class variables. (Contributed by NM, 14-Aug-1999.) |
β’ (π΄ = if(π, π΄, πΆ) β (π β π)) & β’ (π΅ = if(π, π΅, π·) β (π β π)) & β’ (πΆ = if(π, π΄, πΆ) β (π β π)) & β’ (π· = if(π, π΅, π·) β (π β π)) & β’ π β β’ π | ||
Theorem | elimhyp3v 4552 | Eliminate a hypothesis containing 3 class variables. (Contributed by NM, 14-Aug-1999.) |
β’ (π΄ = if(π, π΄, π·) β (π β π)) & β’ (π΅ = if(π, π΅, π ) β (π β π)) & β’ (πΆ = if(π, πΆ, π) β (π β π)) & β’ (π· = if(π, π΄, π·) β (π β π)) & β’ (π = if(π, π΅, π ) β (π β π)) & β’ (π = if(π, πΆ, π) β (π β π)) & β’ π β β’ π | ||
Theorem | elimhyp4v 4553 | Eliminate a hypothesis containing 4 class variables (for use with the weak deduction theorem dedth 4543). (Contributed by NM, 16-Apr-2005.) |
β’ (π΄ = if(π, π΄, π·) β (π β π)) & β’ (π΅ = if(π, π΅, π ) β (π β π)) & β’ (πΆ = if(π, πΆ, π) β (π β π)) & β’ (πΉ = if(π, πΉ, πΊ) β (π β π)) & β’ (π· = if(π, π΄, π·) β (π β π)) & β’ (π = if(π, π΅, π ) β (π β π)) & β’ (π = if(π, πΆ, π) β (π β π)) & β’ (πΊ = if(π, πΉ, πΊ) β (π β π)) & β’ π β β’ π | ||
Theorem | elimel 4554 | Eliminate a membership hypothesis for weak deduction theorem, when special case π΅ β πΆ is provable. (Contributed by NM, 15-May-1999.) |
β’ π΅ β πΆ β β’ if(π΄ β πΆ, π΄, π΅) β πΆ | ||
Theorem | elimdhyp 4555 | Version of elimhyp 4550 where the hypothesis is deduced from the final antecedent. See divalg 16220 for an example of its use. (Contributed by Paul Chapman, 25-Mar-2008.) |
β’ (π β π) & β’ (π΄ = if(π, π΄, π΅) β (π β π)) & β’ (π΅ = if(π, π΄, π΅) β (π β π)) & β’ π β β’ π | ||
Theorem | keephyp 4556 | 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. (Contributed by NM, 15-May-1999.) |
β’ (π΄ = if(π, π΄, π΅) β (π β π)) & β’ (π΅ = if(π, π΄, π΅) β (π β π)) & β’ π & β’ π β β’ π | ||
Theorem | keephyp2v 4557 | Keep a hypothesis containing 2 class variables (for use with the weak deduction theorem dedth 4543). (Contributed by NM, 16-Apr-2005.) |
β’ (π΄ = if(π, π΄, πΆ) β (π β π)) & β’ (π΅ = if(π, π΅, π·) β (π β π)) & β’ (πΆ = if(π, π΄, πΆ) β (π β π)) & β’ (π· = if(π, π΅, π·) β (π β π)) & β’ π & β’ π β β’ π | ||
Theorem | keephyp3v 4558 | Keep a hypothesis containing 3 class variables. (Contributed by NM, 27-Sep-1999.) |
β’ (π΄ = if(π, π΄, π·) β (π β π)) & β’ (π΅ = if(π, π΅, π ) β (π β π)) & β’ (πΆ = if(π, πΆ, π) β (π β π)) & β’ (π· = if(π, π΄, π·) β (π β π)) & β’ (π = if(π, π΅, π ) β (π β π)) & β’ (π = if(π, πΆ, π) β (π β π)) & β’ π & β’ π β β’ π | ||
Syntax | cpw 4559 | Extend class notation to include power class. (The tilde in the Metamath token is meant to suggest the calligraphic font of the P.) |
class π« π΄ | ||
Theorem | pwjust 4560* | Soundness justification theorem for df-pw 4561. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
β’ {π₯ β£ π₯ β π΄} = {π¦ β£ π¦ β π΄} | ||
Definition | df-pw 4561* | 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. When applied to a set, this produces its power set. A power set of S is the set of all subsets of S, including the empty set and S itself. For example, if π΄ = {3, 5, 7}, then π« π΄ = {β , {3}, {5}, {7}, {3, 5}, {3, 7}, {5, 7}, {3, 5, 7}} (ex-pw 29159). We will later introduce the Axiom of Power Sets ax-pow 5319, which can be expressed in class notation per pwexg 5332. Still later we will prove, in hashpw 14264, that the size of the power set of a finite set is 2 raised to the power of the size of the set. (Contributed by NM, 24-Jun-1993.) |
β’ π« π΄ = {π₯ β£ π₯ β π΄} | ||
Theorem | elpwg 4562 | Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5300. (Contributed by NM, 6-Aug-2000.) (Proof shortened by BJ, 31-Dec-2023.) |
β’ (π΄ β π β (π΄ β π« π΅ β π΄ β π΅)) | ||
Theorem | elpw 4563 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.) (Proof shortened by BJ, 31-Dec-2023.) |
β’ π΄ β V β β’ (π΄ β π« π΅ β π΄ β π΅) | ||
Theorem | velpw 4564 | Setvar variable membership in a power class. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ (π₯ β π« π΄ β π₯ β π΄) | ||
Theorem | elpwd 4565 | Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ (π β π΄ β π΅) β β’ (π β π΄ β π« π΅) | ||
Theorem | elpwi 4566 | Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.) |
β’ (π΄ β π« π΅ β π΄ β π΅) | ||
Theorem | elpwb 4567 | Characterization of the elements of a power class. (Contributed by BJ, 29-Apr-2021.) |
β’ (π΄ β π« π΅ β (π΄ β V β§ π΄ β π΅)) | ||
Theorem | elpwid 4568 | An element of a power class is a subclass. Deduction form of elpwi 4566. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β π« π΅) β β’ (π β π΄ β π΅) | ||
Theorem | elelpwi 4569 | If π΄ belongs to a part of πΆ, then π΄ belongs to πΆ. (Contributed by FL, 3-Aug-2009.) |
β’ ((π΄ β π΅ β§ π΅ β π« πΆ) β π΄ β πΆ) | ||
Theorem | sspw 4570 | The powerclass preserves inclusion. See sspwb 5405 for the biconditional version. (Contributed by NM, 13-Oct-1996.) Extract forward implication of sspwb 5405 since it requires fewer axioms. (Revised by BJ, 13-Apr-2024.) |
β’ (π΄ β π΅ β π« π΄ β π« π΅) | ||
Theorem | sspwi 4571 | The powerclass preserves inclusion (inference form). (Contributed by BJ, 13-Apr-2024.) |
β’ π΄ β π΅ β β’ π« π΄ β π« π΅ | ||
Theorem | sspwd 4572 | The powerclass preserves inclusion (deduction form). (Contributed by BJ, 13-Apr-2024.) |
β’ (π β π΄ β π΅) β β’ (π β π« π΄ β π« π΅) | ||
Theorem | pweq 4573 | Equality theorem for power class. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 13-Apr-2024.) |
β’ (π΄ = π΅ β π« π΄ = π« π΅) | ||
Theorem | pweqALT 4574 | Alternate proof of pweq 4573 directly from the definition. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ = π΅ β π« π΄ = π« π΅) | ||
Theorem | pweqi 4575 | Equality inference for power class. (Contributed by NM, 27-Nov-2013.) |
β’ π΄ = π΅ β β’ π« π΄ = π« π΅ | ||
Theorem | pweqd 4576 | Equality deduction for power class. (Contributed by NM, 27-Nov-2013.) |
β’ (π β π΄ = π΅) β β’ (π β π« π΄ = π« π΅) | ||
Theorem | pwunss 4577 | The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.) Remove use of ax-sep 5255, ax-nul 5262, ax-pr 5383 and shorten proof. (Revised by BJ, 13-Apr-2024.) |
β’ (π« π΄ βͺ π« π΅) β π« (π΄ βͺ π΅) | ||
Theorem | nfpw 4578 | Bound-variable hypothesis builder for power class. (Contributed by NM, 28-Oct-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) |
β’ β²π₯π΄ β β’ β²π₯π« π΄ | ||
Theorem | pwidg 4579 | A set is an element of its power set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (π΄ β π β π΄ β π« π΄) | ||
Theorem | pwidb 4580 | A class is an element of its powerclass if and only if it is a set. (Contributed by BJ, 31-Dec-2023.) |
β’ (π΄ β V β π΄ β π« π΄) | ||
Theorem | pwid 4581 | A set is a member of its power class. Theorem 87 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) |
β’ π΄ β V β β’ π΄ β π« π΄ | ||
Theorem | pwss 4582* | Subclass relationship for power class. (Contributed by NM, 21-Jun-2009.) |
β’ (π« π΄ β π΅ β βπ₯(π₯ β π΄ β π₯ β π΅)) | ||
Theorem | pwundif 4583 | Break up the power class of a union into a union of smaller classes. (Contributed by NM, 25-Mar-2007.) (Proof shortened by Thierry Arnoux, 20-Dec-2016.) Remove use of ax-sep 5255, ax-nul 5262, ax-pr 5383 and shorten proof. (Revised by BJ, 14-Apr-2024.) |
β’ π« (π΄ βͺ π΅) = ((π« (π΄ βͺ π΅) β π« π΄) βͺ π« π΄) | ||
Theorem | snjust 4584* | Soundness justification theorem for df-sn 4586. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
β’ {π₯ β£ π₯ = π΄} = {π¦ β£ π¦ = π΄} | ||
Syntax | csn 4585 | Extend class notation to include singleton. |
class {π΄} | ||
Definition | df-sn 4586* | Define the singleton of a class. Definition 7.1 of [Quine] p. 48. For convenience, it is well-defined for proper classes, i.e., those that are not elements of V, see snprc 4677. For an alternate definition see dfsn2 4598. (Contributed by NM, 21-Jun-1993.) |
β’ {π΄} = {π₯ β£ π₯ = π΄} | ||
Syntax | cpr 4587 | Extend class notation to include unordered pair. |
class {π΄, π΅} | ||
Definition | df-pr 4588 |
Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For
example, π΄ β {1, -1} β (π΄β2) = 1 (ex-pr 29160). They are
unordered, so {π΄, π΅} = {π΅, π΄} as proven by prcom 4692. For a more
traditional definition, but requiring a dummy variable, see dfpr2 4604.
{π΄,
π΄} is also an
unordered pair, but also a singleton because of
{π΄} =
{π΄, π΄} (see dfsn2 4598). Therefore, {π΄, π΅} is called
a proper (unordered) pair iff π΄ β π΅ and π΄ and π΅ are
sets.
Note: ordered pairs are a completely different object defined below in df-op 4592. When the term "pair" is used without qualifier, it generally means "unordered pair", and the context makes it clear which version is meant. (Contributed by NM, 21-Jun-1993.) |
β’ {π΄, π΅} = ({π΄} βͺ {π΅}) | ||
Syntax | ctp 4589 | Extend class notation to include unordered triple (sometimes called "unordered triplet"). |
class {π΄, π΅, πΆ} | ||
Definition | df-tp 4590 |
Define unordered triple of classes. Definition of [Enderton] p. 19.
Note: ordered triples are a completely different object defined below in df-ot 4594. As with all tuples, when the term "triple" is used without qualifier, it means "ordered triple". (Contributed by NM, 9-Apr-1994.) |
β’ {π΄, π΅, πΆ} = ({π΄, π΅} βͺ {πΆ}) | ||
Syntax | cop 4591 | Extend class notation to include ordered pair. |
class β¨π΄, π΅β© | ||
Definition | df-op 4592* |
Definition of an ordered pair, equivalent to Kuratowski's definition
{{π΄}, {π΄, π΅}} when the arguments are sets.
Since the
behavior of Kuratowski definition is not very useful for proper classes,
we define it to be empty in this case (see opprc1 4853, opprc2 4854, and
0nelop 5451). For Kuratowski's actual definition when
the arguments are
sets, see dfop 4828. For the justifying theorem (for sets) see
opth 5432.
See dfopif 4826 for an equivalent formulation using the if operation.
Definition 9.1 of [Quine] p. 58 defines an ordered pair unconditionally as β¨π΄, π΅β© = {{π΄}, {π΄, π΅}}, which has different behavior from our df-op 4592 when the arguments are proper classes. Ordinarily this difference is not important, since neither definition is meaningful in that case. Our df-op 4592 was chosen because it often makes proofs shorter by eliminating unnecessary sethood hypotheses. There are other ways to define ordered pairs. The basic requirement is that two ordered pairs are equal iff their respective members are equal. In 1914 Norbert Wiener gave the first successful definition β¨π΄, π΅β©2 = {{{π΄}, β }, {{π΅}}}, justified by opthwiener 5469. This was simplified by Kazimierz Kuratowski in 1921 to our present definition. An even simpler definition β¨π΄, π΅β©3 = {π΄, {π΄, π΅}} is justified by opthreg 9488, but it requires the Axiom of Regularity for its justification and is not commonly used. A definition that also works for proper classes is β¨π΄, π΅β©4 = ((π΄ Γ {β }) βͺ (π΅ Γ {{β }})), justified by opthprc 5693. Nearly at the same time as Norbert Wiener, Felix Hausdorff proposed the following definition in "GrundzΓΌge der Mengenlehre" ("Basics of Set Theory"), p. 32, in 1914: β¨π΄, π΅β©5 = {{π΄, π}, {π΅, π}}. Hausdorff used 1 and 2 instead of π and π, but actually any two different fixed sets will do (e.g., π = β and π = {β }, see 0nep0 5312). Furthermore, Hausdorff demanded that π and π are both different from π΄ as well as π΅, which is actually not necessary (at least not in full extent), see opthhausdorff0 5473 and opthhausdorff 5472. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opthi 14098. An ordered pair of real numbers can also be represented by a complex number as shown by cru 12079. Kuratowski's ordered pair definition is standard for ZFC set theory, but it is very inconvenient to use in New Foundations theory because it is not type-level; a common alternate definition in New Foundations is the definition from [Rosser] p. 281. Since there are other ways to define ordered pairs, we discourage direct use of this definition so that most theorems won't depend on this particular construction; theorems will instead rely on dfopif 4826. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
β’ β¨π΄, π΅β© = {π₯ β£ (π΄ β V β§ π΅ β V β§ π₯ β {{π΄}, {π΄, π΅}})} | ||
Syntax | cotp 4593 | Extend class notation to include ordered triple. |
class β¨π΄, π΅, πΆβ© | ||
Definition | df-ot 4594 | Define ordered triple of classes. Definition of ordered triple in [Stoll] p. 25. (Contributed by NM, 3-Apr-2015.) |
β’ β¨π΄, π΅, πΆβ© = β¨β¨π΄, π΅β©, πΆβ© | ||
Theorem | sneq 4595 | Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
β’ (π΄ = π΅ β {π΄} = {π΅}) | ||
Theorem | sneqi 4596 | Equality inference for singletons. (Contributed by NM, 22-Jan-2004.) |
β’ π΄ = π΅ β β’ {π΄} = {π΅} | ||
Theorem | sneqd 4597 | Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.) |
β’ (π β π΄ = π΅) β β’ (π β {π΄} = {π΅}) | ||
Theorem | dfsn2 4598 | Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
β’ {π΄} = {π΄, π΄} | ||
Theorem | elsng 4599 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15 (generalized). (Contributed by NM, 13-Sep-1995.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
β’ (π΄ β π β (π΄ β {π΅} β π΄ = π΅)) | ||
Theorem | elsn 4600 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
β’ π΄ β V β β’ (π΄ β {π΅} β π΄ = π΅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |