Home | Intuitionistic Logic Explorer Theorem List (p. 57 of 114) | < 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 | f1ofveu 5601* | There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.) |
Theorem | f1ocnvfv3 5602* | 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 5603* | 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 5604* | Lemma for acexmid 5612. (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmidlemb 5605* | Lemma for acexmid 5612. (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmidlemph 5606* | Lemma for acexmid 5612. (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmidlemab 5607* | Lemma for acexmid 5612. (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmidlemcase 5608* |
Lemma for acexmid 5612. 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 4983. 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 5609* | Lemma for acexmid 5612. List the cases identified in acexmidlemcase 5608 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.) |
Theorem | acexmidlem2 5610* |
Lemma for acexmid 5612. This builds on acexmidlem1 5609 by noting that every
element of is
inhabited.
(Note that is not quite a function in the df-fun 4983 sense because it uses ordered pairs as described in opthreg 4345 rather than df-op 3440). The set is also found in onsucelsucexmidlem 4318. (Contributed by Jim Kingdon, 5-Aug-2019.) |
Theorem | acexmidlemv 5611* |
Lemma for acexmid 5612.
This is acexmid 5612 with additional distinct variable constraints, most notably between and . (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmid 5612* |
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 nonempty 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 5613 | 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 5614 | Extend class notation to include class abstraction (class builder) of nested ordered pairs. |
Syntax | cmpt2 5615 | Extend the definition of a class to include maps-to notation for defining an operation via a rule. |
Definition | df-ov 5616 | 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 5642 and ovprc2 5643. 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 5617. (Contributed by NM, 28-Feb-1995.) |
Definition | df-oprab 5617* | 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 5616 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 5737. (Contributed by NM, 12-Mar-1995.) |
Definition | df-mpt2 5618* | 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 3876 for two arguments. (Contributed by NM, 17-Feb-2008.) |
Theorem | oveq 5619 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq1 5620 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq2 5621 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq12 5622 | Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.) |
Theorem | oveq1i 5623 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq2i 5624 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq12i 5625 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | oveqi 5626 | Equality inference for operation value. (Contributed by NM, 24-Nov-2007.) |
Theorem | oveq123i 5627 | Equality inference for operation value. (Contributed by FL, 11-Jul-2010.) |
Theorem | oveq1d 5628 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
Theorem | oveq2d 5629 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
Theorem | oveqd 5630 | Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.) |
Theorem | oveq12d 5631 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | oveqan12d 5632 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
Theorem | oveqan12rd 5633 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
Theorem | oveq123d 5634 | Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.) |
Theorem | nfovd 5635 | Deduction version of bound-variable hypothesis builder nfov 5636. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | nfov 5636 | Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.) |
Theorem | oprabidlem 5637* | Slight elaboration of exdistrfor 1725. A lemma for oprabid 5638. (Contributed by Jim Kingdon, 15-Jan-2019.) |
Theorem | oprabid 5638 | 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 1442 to eliminate that constraint. (Contributed by Mario Carneiro, 20-Mar-2013.) |
Theorem | fnovex 5639 | The result of an operation is a set. (Contributed by Jim Kingdon, 15-Jan-2019.) |
Theorem | ovexg 5640 | Evaluating a set operation at two sets gives a set. (Contributed by Jim Kingdon, 19-Aug-2021.) |
Theorem | ovprc 5641 | 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 5642 | The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.) |
Theorem | ovprc2 5643 | The value of an operation when the second argument is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | csbov123g 5644 | 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 5645* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
Theorem | csbov1g 5646* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
Theorem | csbov2g 5647* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
Theorem | rspceov 5648* | A frequently used special case of rspc2ev 2728 for operation values. (Contributed by NM, 21-Mar-2007.) |
Theorem | fnotovb 5649 | Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5309. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | opabbrex 5650* | 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 5651 | The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
Theorem | brabvv 5652* | 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 5653* | Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.) |
Theorem | reloprab 5654* | An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.) |
Theorem | nfoprab1 5655 | 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 5656 | 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 5657 | The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.) |
Theorem | nfoprab 5658* | Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.) |
Theorem | oprabbid 5659* | 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 5660* | Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) |
Theorem | oprabbii 5661* | Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
Theorem | ssoprab2 5662 | Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 4076. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
Theorem | ssoprab2b 5663 | Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 4077. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
Theorem | eqoprab2b 5664 | Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 4080. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | mpt2eq123 5665* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.) |
Theorem | mpt2eq12 5666* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | mpt2eq123dva 5667* | An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
Theorem | mpt2eq123dv 5668* | An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011.) |
Theorem | mpt2eq123i 5669 | An equality inference for the maps-to notation. (Contributed by NM, 15-Jul-2013.) |
Theorem | mpt2eq3dva 5670* | Slightly more general equality inference for the maps-to notation. (Contributed by NM, 17-Oct-2013.) |
Theorem | mpt2eq3ia 5671 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
Theorem | nfmpt21 5672 | Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.) |
Theorem | nfmpt22 5673 | Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.) |
Theorem | nfmpt2 5674* | Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |
Theorem | mpt20 5675 | A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.) |
Theorem | oprab4 5676* | Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.) |
Theorem | cbvoprab1 5677* | Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008.) (Revised by Mario Carneiro, 5-Dec-2016.) |
Theorem | cbvoprab2 5678* | Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.) |
Theorem | cbvoprab12 5679* | Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | cbvoprab12v 5680* | Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.) |
Theorem | cbvoprab3 5681* | Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.) |
Theorem | cbvoprab3v 5682* | Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.) (Revised by David Abernethy, 19-Jun-2012.) |
Theorem | cbvmpt2x 5683* | Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 5684 allows to be a function of . (Contributed by NM, 29-Dec-2014.) |
Theorem | cbvmpt2 5684* | Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.) |
Theorem | cbvmpt2v 5685* | Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 3908, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.) |
Theorem | dmoprab 5686* | The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
Theorem | dmoprabss 5687* | The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995.) |
Theorem | rnoprab 5688* | The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.) |
Theorem | rnoprab2 5689* | The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.) |
Theorem | reldmoprab 5690* | The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.) |
Theorem | oprabss 5691* | Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.) |
Theorem | eloprabga 5692* | The law of concretion for operation class abstraction. Compare elopab 4059. (Contributed by NM, 14-Sep-1999.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.) |
Theorem | eloprabg 5693* | The law of concretion for operation class abstraction. Compare elopab 4059. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.) |
Theorem | ssoprab2i 5694* | Inference of operation class abstraction subclass from implication. (Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
Theorem | mpt2v 5695* | Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.) |
Theorem | mpt2mptx 5696* | Express a two-argument function as a one-argument function, or vice-versa. In this version is not assumed to be constant w.r.t . (Contributed by Mario Carneiro, 29-Dec-2014.) |
Theorem | mpt2mpt 5697* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by Mario Carneiro, 29-Dec-2014.) |
Theorem | resoprab 5698* | Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007.) |
Theorem | resoprab2 5699* | Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | resmpt2 5700* | Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |