![]() |
Intuitionistic Logic Explorer Theorem List (p. 59 of 149) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fliftval 5801* | The value of the function ๐น. (Contributed by Mario Carneiro, 23-Dec-2016.) |
โข ๐น = ran (๐ฅ โ ๐ โฆ โจ๐ด, ๐ตโฉ) & โข ((๐ โง ๐ฅ โ ๐) โ ๐ด โ ๐ ) & โข ((๐ โง ๐ฅ โ ๐) โ ๐ต โ ๐) & โข (๐ฅ = ๐ โ ๐ด = ๐ถ) & โข (๐ฅ = ๐ โ ๐ต = ๐ท) & โข (๐ โ Fun ๐น) โ โข ((๐ โง ๐ โ ๐) โ (๐นโ๐ถ) = ๐ท) | ||
Theorem | isoeq1 5802 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
โข (๐ป = ๐บ โ (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ ๐บ Isom ๐ , ๐ (๐ด, ๐ต))) | ||
Theorem | isoeq2 5803 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
โข (๐ = ๐ โ (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ ๐ป Isom ๐, ๐ (๐ด, ๐ต))) | ||
Theorem | isoeq3 5804 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
โข (๐ = ๐ โ (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ ๐ป Isom ๐ , ๐ (๐ด, ๐ต))) | ||
Theorem | isoeq4 5805 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
โข (๐ด = ๐ถ โ (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ ๐ป Isom ๐ , ๐ (๐ถ, ๐ต))) | ||
Theorem | isoeq5 5806 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
โข (๐ต = ๐ถ โ (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ ๐ป Isom ๐ , ๐ (๐ด, ๐ถ))) | ||
Theorem | nfiso 5807 | Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
โข โฒ๐ฅ๐ป & โข โฒ๐ฅ๐ & โข โฒ๐ฅ๐ & โข โฒ๐ฅ๐ด & โข โฒ๐ฅ๐ต โ โข โฒ๐ฅ ๐ป Isom ๐ , ๐ (๐ด, ๐ต) | ||
Theorem | isof1o 5808 | An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.) |
โข (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ ๐ป:๐ดโ1-1-ontoโ๐ต) | ||
Theorem | isorel 5809 | An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.) |
โข ((๐ป Isom ๐ , ๐ (๐ด, ๐ต) โง (๐ถ โ ๐ด โง ๐ท โ ๐ด)) โ (๐ถ๐ ๐ท โ (๐ปโ๐ถ)๐(๐ปโ๐ท))) | ||
Theorem | isoresbr 5810* | A consequence of isomorphism on two relations for a function's restriction. (Contributed by Jim Kingdon, 11-Jan-2019.) |
โข ((๐น โพ ๐ด) Isom ๐ , ๐ (๐ด, (๐น โ ๐ด)) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ๐ ๐ฆ โ (๐นโ๐ฅ)๐(๐นโ๐ฆ))) | ||
Theorem | isoid 5811 | Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) |
โข ( I โพ ๐ด) Isom ๐ , ๐ (๐ด, ๐ด) | ||
Theorem | isocnv 5812 | Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) |
โข (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ โก๐ป Isom ๐, ๐ (๐ต, ๐ด)) | ||
Theorem | isocnv2 5813 | Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.) |
โข (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ ๐ป Isom โก๐ , โก๐(๐ด, ๐ต)) | ||
Theorem | isores2 5814 | An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.) |
โข (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ ๐ป Isom ๐ , (๐ โฉ (๐ต ร ๐ต))(๐ด, ๐ต)) | ||
Theorem | isores1 5815 | An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.) |
โข (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ ๐ป Isom (๐ โฉ (๐ด ร ๐ด)), ๐(๐ด, ๐ต)) | ||
Theorem | isores3 5816 | Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
โข ((๐ป Isom ๐ , ๐ (๐ด, ๐ต) โง ๐พ โ ๐ด โง ๐ = (๐ป โ ๐พ)) โ (๐ป โพ ๐พ) Isom ๐ , ๐ (๐พ, ๐)) | ||
Theorem | isotr 5817 | 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.) |
โข ((๐ป Isom ๐ , ๐ (๐ด, ๐ต) โง ๐บ Isom ๐, ๐ (๐ต, ๐ถ)) โ (๐บ โ ๐ป) Isom ๐ , ๐ (๐ด, ๐ถ)) | ||
Theorem | iso0 5818 | The empty set is an ๐ , ๐ isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.) |
โข โ Isom ๐ , ๐ (โ , โ ) | ||
Theorem | isoini 5819 | Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.) |
โข ((๐ป Isom ๐ , ๐ (๐ด, ๐ต) โง ๐ท โ ๐ด) โ (๐ป โ (๐ด โฉ (โก๐ โ {๐ท}))) = (๐ต โฉ (โก๐ โ {(๐ปโ๐ท)}))) | ||
Theorem | isoini2 5820 | Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.) |
โข ๐ถ = (๐ด โฉ (โก๐ โ {๐})) & โข ๐ท = (๐ต โฉ (โก๐ โ {(๐ปโ๐)})) โ โข ((๐ป Isom ๐ , ๐ (๐ด, ๐ต) โง ๐ โ ๐ด) โ (๐ป โพ ๐ถ) Isom ๐ , ๐ (๐ถ, ๐ท)) | ||
Theorem | isoselem 5821* | Lemma for isose 5822. (Contributed by Mario Carneiro, 23-Jun-2015.) |
โข (๐ โ ๐ป Isom ๐ , ๐ (๐ด, ๐ต)) & โข (๐ โ (๐ป โ ๐ฅ) โ V) โ โข (๐ โ (๐ Se ๐ด โ ๐ Se ๐ต)) | ||
Theorem | isose 5822 | An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015.) |
โข (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ (๐ Se ๐ด โ ๐ Se ๐ต)) | ||
Theorem | isopolem 5823 | Lemma for isopo 5824. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
โข (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ (๐ Po ๐ต โ ๐ Po ๐ด)) | ||
Theorem | isopo 5824 | An isomorphism preserves partial ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
โข (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ (๐ Po ๐ด โ ๐ Po ๐ต)) | ||
Theorem | isosolem 5825 | Lemma for isoso 5826. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
โข (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ (๐ Or ๐ต โ ๐ Or ๐ด)) | ||
Theorem | isoso 5826 | An isomorphism preserves strict ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
โข (๐ป Isom ๐ , ๐ (๐ด, ๐ต) โ (๐ Or ๐ด โ ๐ Or ๐ต)) | ||
Theorem | f1oiso 5827* | 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.) |
โข ((๐ป:๐ดโ1-1-ontoโ๐ต โง ๐ = {โจ๐ง, ๐คโฉ โฃ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด ((๐ง = (๐ปโ๐ฅ) โง ๐ค = (๐ปโ๐ฆ)) โง ๐ฅ๐ ๐ฆ)}) โ ๐ป Isom ๐ , ๐ (๐ด, ๐ต)) | ||
Theorem | f1oiso2 5828* | Any one-to-one onto function determines an isomorphism with an induced relation ๐. (Contributed by Mario Carneiro, 9-Mar-2013.) |
โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง (โก๐ปโ๐ฅ)๐ (โก๐ปโ๐ฆ))} โ โข (๐ป:๐ดโ1-1-ontoโ๐ต โ ๐ป Isom ๐ , ๐ (๐ด, ๐ต)) | ||
Theorem | canth 5829 | No set ๐ด is equinumerous to its power set (Cantor's theorem), i.e., no function can map ๐ด onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. (Use nex 1500 if you want the form ยฌ โ๐๐:๐ดโontoโ๐ซ ๐ด.) (Contributed by NM, 7-Aug-1994.) (Revised by Noah R Kingdon, 23-Jul-2024.) |
โข ๐ด โ V โ โข ยฌ ๐น:๐ดโontoโ๐ซ ๐ด | ||
Syntax | crio 5830 | Extend class notation with restricted description binder. |
class (โฉ๐ฅ โ ๐ด ๐) | ||
Definition | df-riota 5831 | 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 5179. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.) |
โข (โฉ๐ฅ โ ๐ด ๐) = (โฉ๐ฅ(๐ฅ โ ๐ด โง ๐)) | ||
Theorem | riotaeqdv 5832* | Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011.) |
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (โฉ๐ฅ โ ๐ด ๐) = (โฉ๐ฅ โ ๐ต ๐)) | ||
Theorem | riotabidv 5833* | Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.) |
โข (๐ โ (๐ โ ๐)) โ โข (๐ โ (โฉ๐ฅ โ ๐ด ๐) = (โฉ๐ฅ โ ๐ด ๐)) | ||
Theorem | riotaeqbidv 5834* | Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.) |
โข (๐ โ ๐ด = ๐ต) & โข (๐ โ (๐ โ ๐)) โ โข (๐ โ (โฉ๐ฅ โ ๐ด ๐) = (โฉ๐ฅ โ ๐ต ๐)) | ||
Theorem | riotaexg 5835* | Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.) |
โข (๐ด โ ๐ โ (โฉ๐ฅ โ ๐ด ๐) โ V) | ||
Theorem | riotav 5836 | An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.) |
โข (โฉ๐ฅ โ V ๐) = (โฉ๐ฅ๐) | ||
Theorem | riotauni 5837 | Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.) |
โข (โ!๐ฅ โ ๐ด ๐ โ (โฉ๐ฅ โ ๐ด ๐) = โช {๐ฅ โ ๐ด โฃ ๐}) | ||
Theorem | nfriota1 5838* | 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 5839* | Deduction version of nfriota 5840. (Contributed by Jim Kingdon, 12-Jan-2019.) |
โข โฒ๐ฆ๐ & โข (๐ โ โฒ๐ฅ๐) & โข (๐ โ โฒ๐ฅ๐ด) โ โข (๐ โ โฒ๐ฅ(โฉ๐ฆ โ ๐ด ๐)) | ||
Theorem | nfriota 5840* | A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.) |
โข โฒ๐ฅ๐ & โข โฒ๐ฅ๐ด โ โข โฒ๐ฅ(โฉ๐ฆ โ ๐ด ๐) | ||
Theorem | cbvriota 5841* | Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
โข โฒ๐ฆ๐ & โข โฒ๐ฅ๐ & โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) โ โข (โฉ๐ฅ โ ๐ด ๐) = (โฉ๐ฆ โ ๐ด ๐) | ||
Theorem | cbvriotav 5842* | Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) โ โข (โฉ๐ฅ โ ๐ด ๐) = (โฉ๐ฆ โ ๐ด ๐) | ||
Theorem | csbriotag 5843* | Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.) |
โข (๐ด โ ๐ โ โฆ๐ด / ๐ฅโฆ(โฉ๐ฆ โ ๐ต ๐) = (โฉ๐ฆ โ ๐ต [๐ด / ๐ฅ]๐)) | ||
Theorem | riotacl2 5844 |
Membership law for "the unique element in ๐ด such that ๐."
(Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
โข (โ!๐ฅ โ ๐ด ๐ โ (โฉ๐ฅ โ ๐ด ๐) โ {๐ฅ โ ๐ด โฃ ๐}) | ||
Theorem | riotacl 5845* | Closure of restricted iota. (Contributed by NM, 21-Aug-2011.) |
โข (โ!๐ฅ โ ๐ด ๐ โ (โฉ๐ฅ โ ๐ด ๐) โ ๐ด) | ||
Theorem | riotasbc 5846 | Substitution law for descriptions. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
โข (โ!๐ฅ โ ๐ด ๐ โ [(โฉ๐ฅ โ ๐ด ๐) / ๐ฅ]๐) | ||
Theorem | riotabidva 5847* | Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 2726 analog.) (Contributed by NM, 17-Jan-2012.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ (๐ โ ๐)) โ โข (๐ โ (โฉ๐ฅ โ ๐ด ๐) = (โฉ๐ฅ โ ๐ด ๐)) | ||
Theorem | riotabiia 5848 | Equivalent wff's yield equal restricted iotas (inference form). (rabbiia 2723 analog.) (Contributed by NM, 16-Jan-2012.) |
โข (๐ฅ โ ๐ด โ (๐ โ ๐)) โ โข (โฉ๐ฅ โ ๐ด ๐) = (โฉ๐ฅ โ ๐ด ๐) | ||
Theorem | riota1 5849* | Property of restricted iota. Compare iota1 5193. (Contributed by Mario Carneiro, 15-Oct-2016.) |
โข (โ!๐ฅ โ ๐ด ๐ โ ((๐ฅ โ ๐ด โง ๐) โ (โฉ๐ฅ โ ๐ด ๐) = ๐ฅ)) | ||
Theorem | riota1a 5850 | Property of iota. (Contributed by NM, 23-Aug-2011.) |
โข ((๐ฅ โ ๐ด โง โ!๐ฅ โ ๐ด ๐) โ (๐ โ (โฉ๐ฅ(๐ฅ โ ๐ด โง ๐)) = ๐ฅ)) | ||
Theorem | riota2df 5851* | A deduction version of riota2f 5852. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
โข โฒ๐ฅ๐ & โข (๐ โ โฒ๐ฅ๐ต) & โข (๐ โ โฒ๐ฅ๐) & โข (๐ โ ๐ต โ ๐ด) & โข ((๐ โง ๐ฅ = ๐ต) โ (๐ โ ๐)) โ โข ((๐ โง โ!๐ฅ โ ๐ด ๐) โ (๐ โ (โฉ๐ฅ โ ๐ด ๐) = ๐ต)) | ||
Theorem | riota2f 5852* | 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 5853* | 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 5854* | Properties of a restricted definite description operator. Todo (df-riota 5831 update): can some uses of riota2f 5852 be shortened with this? (Contributed by NM, 23-Nov-2013.) |
โข โฒ๐ฅ๐ & โข ๐ต = (โฉ๐ฅ โ ๐ด ๐) & โข (๐ฅ = ๐ต โ (๐ โ ๐)) โ โข (โ!๐ฅ โ ๐ด ๐ โ (๐ต โ ๐ด โง ๐)) | ||
Theorem | riota5f 5855* | A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
โข (๐ โ โฒ๐ฅ๐ต) & โข (๐ โ ๐ต โ ๐ด) & โข ((๐ โง ๐ฅ โ ๐ด) โ (๐ โ ๐ฅ = ๐ต)) โ โข (๐ โ (โฉ๐ฅ โ ๐ด ๐) = ๐ต) | ||
Theorem | riota5 5856* | A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.) |
โข (๐ โ ๐ต โ ๐ด) & โข ((๐ โง ๐ฅ โ ๐ด) โ (๐ โ ๐ฅ = ๐ต)) โ โข (๐ โ (โฉ๐ฅ โ ๐ด ๐) = ๐ต) | ||
Theorem | riotass2 5857* | Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.) |
โข (((๐ด โ ๐ต โง โ๐ฅ โ ๐ด (๐ โ ๐)) โง (โ๐ฅ โ ๐ด ๐ โง โ!๐ฅ โ ๐ต ๐)) โ (โฉ๐ฅ โ ๐ด ๐) = (โฉ๐ฅ โ ๐ต ๐)) | ||
Theorem | riotass 5858* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.) |
โข ((๐ด โ ๐ต โง โ๐ฅ โ ๐ด ๐ โง โ!๐ฅ โ ๐ต ๐) โ (โฉ๐ฅ โ ๐ด ๐) = (โฉ๐ฅ โ ๐ต ๐)) | ||
Theorem | moriotass 5859* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.) |
โข ((๐ด โ ๐ต โง โ๐ฅ โ ๐ด ๐ โง โ*๐ฅ โ ๐ต ๐) โ (โฉ๐ฅ โ ๐ด ๐) = (โฉ๐ฅ โ ๐ต ๐)) | ||
Theorem | snriota 5860 | A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.) |
โข (โ!๐ฅ โ ๐ด ๐ โ {๐ฅ โ ๐ด โฃ ๐} = {(โฉ๐ฅ โ ๐ด ๐)}) | ||
Theorem | eusvobj2 5861* | 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.) |
โข ๐ต โ V โ โข (โ!๐ฅโ๐ฆ โ ๐ด ๐ฅ = ๐ต โ (โ๐ฆ โ ๐ด ๐ฅ = ๐ต โ โ๐ฆ โ ๐ด ๐ฅ = ๐ต)) | ||
Theorem | eusvobj1 5862* | 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.) |
โข ๐ต โ V โ โข (โ!๐ฅโ๐ฆ โ ๐ด ๐ฅ = ๐ต โ (โฉ๐ฅโ๐ฆ โ ๐ด ๐ฅ = ๐ต) = (โฉ๐ฅโ๐ฆ โ ๐ด ๐ฅ = ๐ต)) | ||
Theorem | f1ofveu 5863* | There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.) |
โข ((๐น:๐ดโ1-1-ontoโ๐ต โง ๐ถ โ ๐ต) โ โ!๐ฅ โ ๐ด (๐นโ๐ฅ) = ๐ถ) | ||
Theorem | f1ocnvfv3 5864* | 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.) |
โข ((๐น:๐ดโ1-1-ontoโ๐ต โง ๐ถ โ ๐ต) โ (โก๐นโ๐ถ) = (โฉ๐ฅ โ ๐ด (๐นโ๐ฅ) = ๐ถ)) | ||
Theorem | riotaund 5865* | 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 5866* | Lemma for acexmid 5874. (Contributed by Jim Kingdon, 6-Aug-2019.) |
โข ๐ด = {๐ฅ โ {โ , {โ }} โฃ (๐ฅ = โ โจ ๐)} & โข ๐ต = {๐ฅ โ {โ , {โ }} โฃ (๐ฅ = {โ } โจ ๐)} & โข ๐ถ = {๐ด, ๐ต} โ โข ({โ } โ ๐ด โ ๐) | ||
Theorem | acexmidlemb 5867* | Lemma for acexmid 5874. (Contributed by Jim Kingdon, 6-Aug-2019.) |
โข ๐ด = {๐ฅ โ {โ , {โ }} โฃ (๐ฅ = โ โจ ๐)} & โข ๐ต = {๐ฅ โ {โ , {โ }} โฃ (๐ฅ = {โ } โจ ๐)} & โข ๐ถ = {๐ด, ๐ต} โ โข (โ โ ๐ต โ ๐) | ||
Theorem | acexmidlemph 5868* | Lemma for acexmid 5874. (Contributed by Jim Kingdon, 6-Aug-2019.) |
โข ๐ด = {๐ฅ โ {โ , {โ }} โฃ (๐ฅ = โ โจ ๐)} & โข ๐ต = {๐ฅ โ {โ , {โ }} โฃ (๐ฅ = {โ } โจ ๐)} & โข ๐ถ = {๐ด, ๐ต} โ โข (๐ โ ๐ด = ๐ต) | ||
Theorem | acexmidlemab 5869* | Lemma for acexmid 5874. (Contributed by Jim Kingdon, 6-Aug-2019.) |
โข ๐ด = {๐ฅ โ {โ , {โ }} โฃ (๐ฅ = โ โจ ๐)} & โข ๐ต = {๐ฅ โ {โ , {โ }} โฃ (๐ฅ = {โ } โจ ๐)} & โข ๐ถ = {๐ด, ๐ต} โ โข (((โฉ๐ฃ โ ๐ด โ๐ข โ ๐ฆ (๐ด โ ๐ข โง ๐ฃ โ ๐ข)) = โ โง (โฉ๐ฃ โ ๐ต โ๐ข โ ๐ฆ (๐ต โ ๐ข โง ๐ฃ โ ๐ข)) = {โ }) โ ยฌ ๐) | ||
Theorem | acexmidlemcase 5870* |
Lemma for acexmid 5874. 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 5219. 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 5871* | Lemma for acexmid 5874. List the cases identified in acexmidlemcase 5870 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.) |
โข ๐ด = {๐ฅ โ {โ , {โ }} โฃ (๐ฅ = โ โจ ๐)} & โข ๐ต = {๐ฅ โ {โ , {โ }} โฃ (๐ฅ = {โ } โจ ๐)} & โข ๐ถ = {๐ด, ๐ต} โ โข (โ๐ง โ ๐ถ โ!๐ฃ โ ๐ง โ๐ข โ ๐ฆ (๐ง โ ๐ข โง ๐ฃ โ ๐ข) โ (๐ โจ ยฌ ๐)) | ||
Theorem | acexmidlem2 5872* |
Lemma for acexmid 5874. This builds on acexmidlem1 5871 by noting that every
element of ๐ถ is inhabited.
(Note that ๐ฆ is not quite a function in the df-fun 5219 sense because it uses ordered pairs as described in opthreg 4556 rather than df-op 3602). The set ๐ด is also found in onsucelsucexmidlem 4529. (Contributed by Jim Kingdon, 5-Aug-2019.) |
โข ๐ด = {๐ฅ โ {โ , {โ }} โฃ (๐ฅ = โ โจ ๐)} & โข ๐ต = {๐ฅ โ {โ , {โ }} โฃ (๐ฅ = {โ } โจ ๐)} & โข ๐ถ = {๐ด, ๐ต} โ โข (โ๐ง โ ๐ถ โ๐ค โ ๐ง โ!๐ฃ โ ๐ง โ๐ข โ ๐ฆ (๐ง โ ๐ข โง ๐ฃ โ ๐ข) โ (๐ โจ ยฌ ๐)) | ||
Theorem | acexmidlemv 5873* |
Lemma for acexmid 5874.
This is acexmid 5874 with additional disjoint variable conditions, most notably between ๐ and ๐ฅ. (Contributed by Jim Kingdon, 6-Aug-2019.) |
โข โ๐ฆโ๐ง โ ๐ฅ โ๐ค โ ๐ง โ!๐ฃ โ ๐ง โ๐ข โ ๐ฆ (๐ง โ ๐ข โง ๐ฃ โ ๐ข) โ โข (๐ โจ ยฌ ๐) | ||
Theorem | acexmid 5874* |
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 7205 and df-exmid 4196 syntaxes, see exmidac 7208. (Contributed by Jim Kingdon, 4-Aug-2019.) |
โข โ๐ฆโ๐ง โ ๐ฅ โ๐ค โ ๐ง โ!๐ฃ โ ๐ง โ๐ข โ ๐ฆ (๐ง โ ๐ข โง ๐ฃ โ ๐ข) โ โข (๐ โจ ยฌ ๐) | ||
Syntax | co 5875 | 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. |
class (๐ด๐น๐ต) | ||
Syntax | coprab 5876 | Extend class notation to include class abstraction (class builder) of nested ordered pairs. |
class {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} | ||
Syntax | cmpo 5877 | Extend the definition of a class to include maps-to notation for defining an operation via a rule. |
class (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) | ||
Definition | df-ov 5878 | 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 5911 and ovprc2 5912. 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 5879. (Contributed by NM, 28-Feb-1995.) |
โข (๐ด๐น๐ต) = (๐นโโจ๐ด, ๐ตโฉ) | ||
Definition | df-oprab 5879* | 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 5878 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 6010. (Contributed by NM, 12-Mar-1995.) |
โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {๐ค โฃ โ๐ฅโ๐ฆโ๐ง(๐ค = โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โง ๐)} | ||
Definition | df-mpo 5880* | 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 4067 for two arguments. (Contributed by NM, 17-Feb-2008.) |
โข (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โง ๐ง = ๐ถ)} | ||
Theorem | oveq 5881 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
โข (๐น = ๐บ โ (๐ด๐น๐ต) = (๐ด๐บ๐ต)) | ||
Theorem | oveq1 5882 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
โข (๐ด = ๐ต โ (๐ด๐น๐ถ) = (๐ต๐น๐ถ)) | ||
Theorem | oveq2 5883 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
โข (๐ด = ๐ต โ (๐ถ๐น๐ด) = (๐ถ๐น๐ต)) | ||
Theorem | oveq12 5884 | Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.) |
โข ((๐ด = ๐ต โง ๐ถ = ๐ท) โ (๐ด๐น๐ถ) = (๐ต๐น๐ท)) | ||
Theorem | oveq1i 5885 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
โข ๐ด = ๐ต โ โข (๐ด๐น๐ถ) = (๐ต๐น๐ถ) | ||
Theorem | oveq2i 5886 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
โข ๐ด = ๐ต โ โข (๐ถ๐น๐ด) = (๐ถ๐น๐ต) | ||
Theorem | oveq12i 5887 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
โข ๐ด = ๐ต & โข ๐ถ = ๐ท โ โข (๐ด๐น๐ถ) = (๐ต๐น๐ท) | ||
Theorem | oveqi 5888 | Equality inference for operation value. (Contributed by NM, 24-Nov-2007.) |
โข ๐ด = ๐ต โ โข (๐ถ๐ด๐ท) = (๐ถ๐ต๐ท) | ||
Theorem | oveq123i 5889 | Equality inference for operation value. (Contributed by FL, 11-Jul-2010.) |
โข ๐ด = ๐ถ & โข ๐ต = ๐ท & โข ๐น = ๐บ โ โข (๐ด๐น๐ต) = (๐ถ๐บ๐ท) | ||
Theorem | oveq1d 5890 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ด๐น๐ถ) = (๐ต๐น๐ถ)) | ||
Theorem | oveq2d 5891 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ถ๐น๐ด) = (๐ถ๐น๐ต)) | ||
Theorem | oveqd 5892 | Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.) |
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ถ๐ด๐ท) = (๐ถ๐ต๐ท)) | ||
Theorem | oveq12d 5893 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
โข (๐ โ ๐ด = ๐ต) & โข (๐ โ ๐ถ = ๐ท) โ โข (๐ โ (๐ด๐น๐ถ) = (๐ต๐น๐ท)) | ||
Theorem | oveqan12d 5894 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
โข (๐ โ ๐ด = ๐ต) & โข (๐ โ ๐ถ = ๐ท) โ โข ((๐ โง ๐) โ (๐ด๐น๐ถ) = (๐ต๐น๐ท)) | ||
Theorem | oveqan12rd 5895 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
โข (๐ โ ๐ด = ๐ต) & โข (๐ โ ๐ถ = ๐ท) โ โข ((๐ โง ๐) โ (๐ด๐น๐ถ) = (๐ต๐น๐ท)) | ||
Theorem | oveq123d 5896 | Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.) |
โข (๐ โ ๐น = ๐บ) & โข (๐ โ ๐ด = ๐ต) & โข (๐ โ ๐ถ = ๐ท) โ โข (๐ โ (๐ด๐น๐ถ) = (๐ต๐บ๐ท)) | ||
Theorem | fvoveq1d 5897 | Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.) |
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐นโ(๐ด๐๐ถ)) = (๐นโ(๐ต๐๐ถ))) | ||
Theorem | fvoveq1 5898 | Equality theorem for nested function and operation value. Closed form of fvoveq1d 5897. (Contributed by AV, 23-Jul-2022.) |
โข (๐ด = ๐ต โ (๐นโ(๐ด๐๐ถ)) = (๐นโ(๐ต๐๐ถ))) | ||
Theorem | ovanraleqv 5899* | 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 5900 | 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.) |
โข (๐ = ๐ โ (๐ โ ๐)) โ โข (๐ = ๐ โ ((๐ โ (๐นโ((๐บโ๐) ยท ๐))๐ ๐ด) โ (๐ โ (๐นโ((๐บโ๐) ยท ๐))๐ ๐ด))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |