Home | Intuitionistic Logic Explorer Theorem List (p. 58 of 133) | < 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 | fliftval 5701* | The value of the function . (Contributed by Mario Carneiro, 23-Dec-2016.) |
Theorem | isoeq1 5702 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
Theorem | isoeq2 5703 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
Theorem | isoeq3 5704 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
Theorem | isoeq4 5705 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
Theorem | isoeq5 5706 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
Theorem | nfiso 5707 | Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | isof1o 5708 | An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.) |
Theorem | isorel 5709 | An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.) |
Theorem | isoresbr 5710* | A consequence of isomorphism on two relations for a function's restriction. (Contributed by Jim Kingdon, 11-Jan-2019.) |
Theorem | isoid 5711 | Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) |
Theorem | isocnv 5712 | Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) |
Theorem | isocnv2 5713 | Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.) |
Theorem | isores2 5714 | An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.) |
Theorem | isores1 5715 | An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.) |
Theorem | isores3 5716 | Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
Theorem | isotr 5717 | Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) (Proof shortened by Mario Carneiro, 5-Dec-2016.) |
Theorem | iso0 5718 | The empty set is an isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.) |
Theorem | isoini 5719 | Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.) |
Theorem | isoini2 5720 | Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.) |
Theorem | isoselem 5721* | Lemma for isose 5722. (Contributed by Mario Carneiro, 23-Jun-2015.) |
Se Se | ||
Theorem | isose 5722 | An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015.) |
Se Se | ||
Theorem | isopolem 5723 | Lemma for isopo 5724. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
Theorem | isopo 5724 | An isomorphism preserves partial ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
Theorem | isosolem 5725 | Lemma for isoso 5726. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
Theorem | isoso 5726 | An isomorphism preserves strict ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
Theorem | f1oiso 5727* | Any one-to-one onto function determines an isomorphism with an induced relation . Proposition 6.33 of [TakeutiZaring] p. 34. (Contributed by NM, 30-Apr-2004.) |
Theorem | f1oiso2 5728* | Any one-to-one onto function determines an isomorphism with an induced relation . (Contributed by Mario Carneiro, 9-Mar-2013.) |
Syntax | crio 5729 | Extend class notation with restricted description binder. |
Definition | df-riota 5730 | Define restricted description binder. In case there is no unique such that holds, it evaluates to the empty set. See also comments for df-iota 5088. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.) |
Theorem | riotaeqdv 5731* | Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011.) |
Theorem | riotabidv 5732* | Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.) |
Theorem | riotaeqbidv 5733* | Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.) |
Theorem | riotaexg 5734* | Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.) |
Theorem | riotav 5735 | An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.) |
Theorem | riotauni 5736 | Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.) |
Theorem | nfriota1 5737* | 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 5738* | Deduction version of nfriota 5739. (Contributed by Jim Kingdon, 12-Jan-2019.) |
Theorem | nfriota 5739* | A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.) |
Theorem | cbvriota 5740* | Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | cbvriotav 5741* | Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | csbriotag 5742* | Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.) |
Theorem | riotacl2 5743 |
Membership law for "the unique element in such that ."
(Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
Theorem | riotacl 5744* | Closure of restricted iota. (Contributed by NM, 21-Aug-2011.) |
Theorem | riotasbc 5745 | Substitution law for descriptions. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
Theorem | riotabidva 5746* | Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 2674 analog.) (Contributed by NM, 17-Jan-2012.) |
Theorem | riotabiia 5747 | Equivalent wff's yield equal restricted iotas (inference form). (rabbiia 2671 analog.) (Contributed by NM, 16-Jan-2012.) |
Theorem | riota1 5748* | Property of restricted iota. Compare iota1 5102. (Contributed by Mario Carneiro, 15-Oct-2016.) |
Theorem | riota1a 5749 | Property of iota. (Contributed by NM, 23-Aug-2011.) |
Theorem | riota2df 5750* | A deduction version of riota2f 5751. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | riota2f 5751* | 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 5752* | 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 5753* | Properties of a restricted definite description operator. Todo (df-riota 5730 update): can some uses of riota2f 5751 be shortened with this? (Contributed by NM, 23-Nov-2013.) |
Theorem | riota5f 5754* | A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | riota5 5755* | A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.) |
Theorem | riotass2 5756* | Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.) |
Theorem | riotass 5757* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.) |
Theorem | moriotass 5758* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.) |
Theorem | snriota 5759 | A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.) |
Theorem | eusvobj2 5760* | 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 5761* | 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 5762* | There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.) |
Theorem | f1ocnvfv3 5763* | 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 5764* | 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 5765* | Lemma for acexmid 5773. (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmidlemb 5766* | Lemma for acexmid 5773. (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmidlemph 5767* | Lemma for acexmid 5773. (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmidlemab 5768* | Lemma for acexmid 5773. (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmidlemcase 5769* |
Lemma for acexmid 5773. 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 5125. 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 5770* | Lemma for acexmid 5773. List the cases identified in acexmidlemcase 5769 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.) |
Theorem | acexmidlem2 5771* |
Lemma for acexmid 5773. This builds on acexmidlem1 5770 by noting that every
element of is
inhabited.
(Note that is not quite a function in the df-fun 5125 sense because it uses ordered pairs as described in opthreg 4471 rather than df-op 3536). The set is also found in onsucelsucexmidlem 4444. (Contributed by Jim Kingdon, 5-Aug-2019.) |
Theorem | acexmidlemv 5772* |
Lemma for acexmid 5773.
This is acexmid 5773 with additional distinct variable constraints, most notably between and . (Contributed by Jim Kingdon, 6-Aug-2019.) |
Theorem | acexmid 5773* |
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). For this theorem stated using the df-ac 7062 and df-exmid 4119 syntaxes, see exmidac 7065. (Contributed by Jim Kingdon, 4-Aug-2019.) |
Syntax | co 5774 | 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 5775 | Extend class notation to include class abstraction (class builder) of nested ordered pairs. |
Syntax | cmpo 5776 | Extend the definition of a class to include maps-to notation for defining an operation via a rule. |
Definition | df-ov 5777 | 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 5807 and ovprc2 5808. 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 5778. (Contributed by NM, 28-Feb-1995.) |
Definition | df-oprab 5778* | 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 5777 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 ovmpo 5906. (Contributed by NM, 12-Mar-1995.) |
Definition | df-mpo 5779* | 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 3991 for two arguments. (Contributed by NM, 17-Feb-2008.) |
Theorem | oveq 5780 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq1 5781 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq2 5782 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq12 5783 | Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.) |
Theorem | oveq1i 5784 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq2i 5785 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq12i 5786 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | oveqi 5787 | Equality inference for operation value. (Contributed by NM, 24-Nov-2007.) |
Theorem | oveq123i 5788 | Equality inference for operation value. (Contributed by FL, 11-Jul-2010.) |
Theorem | oveq1d 5789 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
Theorem | oveq2d 5790 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
Theorem | oveqd 5791 | Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.) |
Theorem | oveq12d 5792 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | oveqan12d 5793 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
Theorem | oveqan12rd 5794 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
Theorem | oveq123d 5795 | Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.) |
Theorem | fvoveq1d 5796 | Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.) |
Theorem | fvoveq1 5797 | Equality theorem for nested function and operation value. Closed form of fvoveq1d 5796. (Contributed by AV, 23-Jul-2022.) |
Theorem | ovanraleqv 5798* | Equality theorem for a conjunction with an operation values within a restricted universal quantification. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.) |
Theorem | imbrov2fvoveq 5799 | Equality theorem for nested function and operation value in an implication for a binary relation. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 17-Aug-2022.) |
Theorem | nfovd 5800 | Deduction version of bound-variable hypothesis builder nfov 5801. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |