Home | Intuitionistic Logic Explorer Theorem List (p. 56 of 106) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | riotav 5501 | An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.) |
Theorem | riotauni 5502 | Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.) |
Theorem | nfriota1 5503* | The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | nfriotadxy 5504* | Deduction version of nfriota 5505. (Contributed by Jim Kingdon, 12-Jan-2019.) |
Theorem | nfriota 5505* | A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.) |
Theorem | cbvriota 5506* | Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | cbvriotav 5507* | Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | csbriotag 5508* | Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.) |
Theorem | riotacl2 5509 |
Membership law for "the unique element in such that ."
(Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
Theorem | riotacl 5510* | Closure of restricted iota. (Contributed by NM, 21-Aug-2011.) |
Theorem | riotasbc 5511 | Substitution law for descriptions. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
Theorem | riotabidva 5512* | Equivalent wff's yield equal restricted class abstractions (deduction rule). (rabbidva 2565 analog.) (Contributed by NM, 17-Jan-2012.) |
Theorem | riotabiia 5513 | Equivalent wff's yield equal restricted iotas (inference rule). (rabbiia 2564 analog.) (Contributed by NM, 16-Jan-2012.) |
Theorem | riota1 5514* | Property of restricted iota. Compare iota1 4909. (Contributed by Mario Carneiro, 15-Oct-2016.) |
Theorem | riota1a 5515 | Property of iota. (Contributed by NM, 23-Aug-2011.) |
Theorem | riota2df 5516* | A deduction version of riota2f 5517. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | riota2f 5517* | This theorem shows a condition that allows us to represent a descriptor with a class expression . (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | riota2 5518* | This theorem shows a condition that allows us to represent a descriptor with a class expression . (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.) |
Theorem | riotaprop 5519* | Properties of a restricted definite description operator. Todo (df-riota 5496 update): can some uses of riota2f 5517 be shortened with this? (Contributed by NM, 23-Nov-2013.) |
Theorem | riota5f 5520* | A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | riota5 5521* | A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.) |
Theorem | riotass2 5522* | Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.) |
Theorem | riotass 5523* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.) |
Theorem | moriotass 5524* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.) |
Theorem | snriota 5525 | A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.) |
Theorem | eusvobj2 5526* | Specify the same property in two ways when class is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
Theorem | eusvobj1 5527* | Specify the same object in two ways when class is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
Theorem | f1ofveu 5528* | There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.) |
Theorem | f1ocnvfv3 5529* | Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
Theorem | riotaund 5530* | Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 13-Sep-2018.) |
Theorem | acexmidlema 5531* | Lemma for acexmid 5539. (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmidlemb 5532* | Lemma for acexmid 5539. (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmidlemph 5533* | Lemma for acexmid 5539. (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmidlemab 5534* | Lemma for acexmid 5539. (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmidlemcase 5535* |
Lemma for acexmid 5539. Here we divide the proof into cases (based
on the
disjunction implicit in an unordered pair, not the sort of case
elimination which relies on excluded middle).
The cases are (1) the choice function evaluated at equals , (2) the choice function evaluated at equals , and (3) the choice function evaluated at equals and the choice function evaluated at equals . Because of the way we represent the choice function , the choice function evaluated at is and the choice function evaluated at is . Other than the difference in notation these work just as and would if were a function as defined by df-fun 4932. Although it isn't exactly about the division into cases, it is also convenient for this lemma to also include the step that if the choice function evaluated at equals , then and likewise for . (Contributed by Jim Kingdon, 7-Aug-2019.) |
Theorem | acexmidlem1 5536* | Lemma for acexmid 5539. List the cases identified in acexmidlemcase 5535 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.) |
Theorem | acexmidlem2 5537* |
Lemma for acexmid 5539. This builds on acexmidlem1 5536 by noting that every
element of is
inhabited.
(Note that is not quite a function in the df-fun 4932 sense because it uses ordered pairs as described in opthreg 4308 rather than df-op 3412). The set is also found in onsucelsucexmidlem 4282. (Contributed by Jim Kingdon, 5-Aug-2019.) |
Theorem | acexmidlemv 5538* |
Lemma for acexmid 5539.
This is acexmid 5539 with additional distinct variable constraints, most notably between and . (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmid 5539* |
The axiom of choice implies excluded middle. Theorem 1.3 in [Bauer]
p. 483.
The statement of the axiom of choice given here is ac2 in the Metamath Proof Explorer (version of 3-Aug-2019). In particular, note that the choice function provides a value when is inhabited (as opposed to non-empty as in some statements of the axiom of choice). Essentially the same proof can also be found at "The axiom of choice implies instances of EM", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". Often referred to as Diaconescu's theorem, or Diaconescu-Goodman-Myhill theorem, after Radu Diaconescu who discovered it in 1975 in the framework of topos theory and N. D. Goodman and John Myhill in 1978 in the framework of set theory (although it already appeared as an exercise in Errett Bishop's book Foundations of Constructive Analysis from 1967). (Contributed by Jim Kingdon, 4-Aug-2019.) |
Syntax | co 5540 | Extend class notation to include the value of an operation (such as + ) for two arguments and . Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous. |
Syntax | coprab 5541 | Extend class notation to include class abstraction (class builder) of nested ordered pairs. |
Syntax | cmpt2 5542 | Extend the definition of a class to include maps-to notation for defining an operation via a rule. |
Definition | df-ov 5543 | Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation and its arguments and - will be useful for proving meaningful theorems. For example, if class is the operation + and arguments and are 3 and 2 , the expression ( 3 + 2 ) can be proved to equal 5 . This definition is well-defined, although not very meaningful, when classes and/or are proper classes (i.e. are not sets); see ovprc1 5569 and ovprc2 5570. On the other hand, we often find uses for this definition when is a proper class. is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5544. (Contributed by NM, 28-Feb-1995.) |
Definition | df-oprab 5544* | Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally , , and are distinct, although the definition doesn't strictly require it. See df-ov 5543 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ovmpt2 5664. (Contributed by NM, 12-Mar-1995.) |
Definition | df-mpt2 5545* | Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from (in ) to ." An extension of df-mpt 3848 for two arguments. (Contributed by NM, 17-Feb-2008.) |
Theorem | oveq 5546 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq1 5547 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq2 5548 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq12 5549 | Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.) |
Theorem | oveq1i 5550 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq2i 5551 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq12i 5552 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | oveqi 5553 | Equality inference for operation value. (Contributed by NM, 24-Nov-2007.) |
Theorem | oveq123i 5554 | Equality inference for operation value. (Contributed by FL, 11-Jul-2010.) |
Theorem | oveq1d 5555 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
Theorem | oveq2d 5556 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
Theorem | oveqd 5557 | Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.) |
Theorem | oveq12d 5558 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | oveqan12d 5559 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
Theorem | oveqan12rd 5560 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
Theorem | oveq123d 5561 | Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.) |
Theorem | nfovd 5562 | Deduction version of bound-variable hypothesis builder nfov 5563. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | nfov 5563 | Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.) |
Theorem | oprabidlem 5564* | Slight elaboration of exdistrfor 1697. A lemma for oprabid 5565. (Contributed by Jim Kingdon, 15-Jan-2019.) |
Theorem | oprabid 5565 | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Although this theorem would be useful with a distinct variable constraint between , , and , we use ax-bndl 1415 to eliminate that constraint. (Contributed by Mario Carneiro, 20-Mar-2013.) |
Theorem | fnovex 5566 | The result of an operation is a set. (Contributed by Jim Kingdon, 15-Jan-2019.) |
Theorem | ovexg 5567 | Evaluating a set operation at two sets gives a set. (Contributed by Jim Kingdon, 19-Aug-2021.) |
Theorem | ovprc 5568 | The value of an operation when the one of the arguments is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | ovprc1 5569 | The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.) |
Theorem | ovprc2 5570 | The value of an operation when the second argument is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | csbov123g 5571 | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Proof shortened by Mario Carneiro, 5-Dec-2016.) |
Theorem | csbov12g 5572* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
Theorem | csbov1g 5573* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
Theorem | csbov2g 5574* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
Theorem | rspceov 5575* | A frequently used special case of rspc2ev 2687 for operation values. (Contributed by NM, 21-Mar-2007.) |
Theorem | fnotovb 5576 | Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5243. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | opabbrex 5577* | A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) |
Theorem | 0neqopab 5578 | The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
Theorem | brabvv 5579* | If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Jim Kingdon, 16-Jan-2019.) |
Theorem | dfoprab2 5580* | Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.) |
Theorem | reloprab 5581* | An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.) |
Theorem | nfoprab1 5582 | The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
Theorem | nfoprab2 5583 | The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 30-Jul-2012.) |
Theorem | nfoprab3 5584 | The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.) |
Theorem | nfoprab 5585* | Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.) |
Theorem | oprabbid 5586* | Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2014.) |
Theorem | oprabbidv 5587* | Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) |
Theorem | oprabbii 5588* | Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
Theorem | ssoprab2 5589 | Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 4040. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
Theorem | ssoprab2b 5590 | Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 4041. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
Theorem | eqoprab2b 5591 | Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 4044. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | mpt2eq123 5592* | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.) |
Theorem | mpt2eq12 5593* | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpt2eq123dva 5594* | An equality deduction for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Theorem | mpt2eq123dv 5595* | An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.) |
Theorem | mpt2eq123i 5596 | An equality inference for the maps to notation. (Contributed by NM, 15-Jul-2013.) |
Theorem | mpt2eq3dva 5597* | Slightly more general equality inference for the maps to notation. (Contributed by NM, 17-Oct-2013.) |
Theorem | mpt2eq3ia 5598 | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | nfmpt21 5599 | Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.) |
Theorem | nfmpt22 5600 | Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |