Home Intuitionistic Logic ExplorerTheorem List (p. 63 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

Theorem List for Intuitionistic Logic Explorer - 6201-6300   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremecidg 6201 A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by Jim Kingdon, 8-Jan-2020.)

Theoremqsid 6202 A set is equal to its quotient set mod converse epsilon. (Note: converse epsilon is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)

Theoremectocld 6203* Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.)

Theoremectocl 6204* Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)

Theoremelqsn0m 6205* An element of a quotient set is inhabited. (Contributed by Jim Kingdon, 21-Aug-2019.)

Theoremelqsn0 6206 A quotient set doesn't contain the empty set. (Contributed by NM, 24-Aug-1995.)

Theoremecelqsdm 6207 Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995.)

Theoremxpiderm 6208* A square Cartesian product is an equivalence relation (in general it's not a poset). (Contributed by Jim Kingdon, 22-Aug-2019.)

Theoremiinerm 6209* The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)

Theoremriinerm 6210* The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)

Theoremerinxp 6211 A restricted equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario Carneiro, 12-Aug-2015.)

Theoremecinxp 6212 Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015.)

Theoremqsinxp 6213 Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)

Theoremqsel 6214 If an element of a quotient set contains a given element, it is equal to the equivalence class of the element. (Contributed by Mario Carneiro, 12-Aug-2015.)

Theoremqliftlem 6215* , a function lift, is a subset of . (Contributed by Mario Carneiro, 23-Dec-2016.)

Theoremqliftrel 6216* , a function lift, is a subset of . (Contributed by Mario Carneiro, 23-Dec-2016.)

Theoremqliftel 6217* Elementhood in the relation . (Contributed by Mario Carneiro, 23-Dec-2016.)

Theoremqliftel1 6218* Elementhood in the relation . (Contributed by Mario Carneiro, 23-Dec-2016.)

Theoremqliftfun 6219* The function is the unique function defined by , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)

Theoremqliftfund 6220* The function is the unique function defined by , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)

Theoremqliftfuns 6221* The function is the unique function defined by , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)

Theoremqliftf 6222* The domain and range of the function . (Contributed by Mario Carneiro, 23-Dec-2016.)

Theoremqliftval 6223* The value of the function . (Contributed by Mario Carneiro, 23-Dec-2016.)

Theoremecoptocl 6224* Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995.)

Theorem2ecoptocl 6225* Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995.)

Theorem3ecoptocl 6226* Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995.)

Theorembrecop 6227* Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.)

Theoremeroveu 6228* Lemma for eroprf 6230. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)

Theoremerovlem 6229* Lemma for eroprf 6230. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.)

Theoremeroprf 6230* Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.)

Theoremeroprf2 6231* Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.)

Theoremecopoveq 6232* This is the first of several theorems about equivalence relations of the kind used in construction of fractions and signed reals, involving operations on equivalent classes of ordered pairs. This theorem expresses the relation (specified by the hypothesis) in terms of its operation . (Contributed by NM, 16-Aug-1995.)

Theoremecopovsym 6233* Assuming the operation is commutative, show that the relation , specified by the first hypothesis, is symmetric. (Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro, 26-Apr-2015.)

Theoremecopovtrn 6234* Assuming that operation is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation , specified by the first hypothesis, is transitive. (Contributed by NM, 11-Feb-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)

Theoremecopover 6235* Assuming that operation is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation , specified by the first hypothesis, is an equivalence relation. (Contributed by NM, 16-Feb-1996.) (Revised by Mario Carneiro, 12-Aug-2015.)

Theoremecopovsymg 6236* Assuming the operation is commutative, show that the relation , specified by the first hypothesis, is symmetric. (Contributed by Jim Kingdon, 1-Sep-2019.)

Theoremecopovtrng 6237* Assuming that operation is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation , specified by the first hypothesis, is transitive. (Contributed by Jim Kingdon, 1-Sep-2019.)

Theoremecopoverg 6238* Assuming that operation is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation , specified by the first hypothesis, is an equivalence relation. (Contributed by Jim Kingdon, 1-Sep-2019.)

Theoremth3qlem1 6239* Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The third hypothesis is the compatibility assumption. (Contributed by NM, 3-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)

Theoremth3qlem2 6240* Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. The fourth hypothesis is the compatibility assumption. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)

Theoremth3qcor 6241* Corollary of Theorem 3Q of [Enderton] p. 60. (Contributed by NM, 12-Nov-1995.) (Revised by David Abernethy, 4-Jun-2013.)

Theoremth3q 6242* Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)

Theoremoviec 6243* Express an operation on equivalence classes of ordered pairs in terms of equivalence class of operations on ordered pairs. See iset.mm for additional comments describing the hypotheses. (Unnecessary distinct variable restrictions were removed by David Abernethy, 4-Jun-2013.) (Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro, 4-Jun-2013.)

Theoremecovcom 6244* Lemma used to transfer a commutative law via an equivalence relation. Most uses will want ecovicom 6245 instead. (Contributed by NM, 29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)

Theoremecovicom 6245* Lemma used to transfer a commutative law via an equivalence relation. (Contributed by Jim Kingdon, 15-Sep-2019.)

Theoremecovass 6246* Lemma used to transfer an associative law via an equivalence relation. In most cases ecoviass 6247 will be more useful. (Contributed by NM, 31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)

Theoremecoviass 6247* Lemma used to transfer an associative law via an equivalence relation. (Contributed by Jim Kingdon, 16-Sep-2019.)

Theoremecovdi 6248* Lemma used to transfer a distributive law via an equivalence relation. Most likely ecovidi 6249 will be more helpful. (Contributed by NM, 2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)

Theoremecovidi 6249* Lemma used to transfer a distributive law via an equivalence relation. (Contributed by Jim Kingdon, 17-Sep-2019.)

2.6.25  Equinumerosity

Syntaxcen 6250 Extend class definition to include the equinumerosity relation ("approximately equals" symbol)

Syntaxcdom 6251 Extend class definition to include the dominance relation (curly less-than-or-equal)

Syntaxcfn 6252 Extend class definition to include the class of all finite sets.

Definitiondf-en 6253* Define the equinumerosity relation. Definition of [Enderton] p. 129. We define to be a binary relation rather than a connective, so its arguments must be sets to be meaningful. This is acceptable because we do not consider equinumerosity for proper classes. We derive the usual definition as bren 6259. (Contributed by NM, 28-Mar-1998.)

Definitiondf-dom 6254* Define the dominance relation. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 6262 and domen 6263. (Contributed by NM, 28-Mar-1998.)

Definitiondf-fin 6255* Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our " ". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 10488. (Contributed by NM, 22-Aug-2008.)

Theoremrelen 6256 Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)

Theoremreldom 6257 Dominance is a relation. (Contributed by NM, 28-Mar-1998.)

Theoremencv 6258 If two classes are equinumerous, both classes are sets. (Contributed by AV, 21-Mar-2019.)

Theorembren 6259* Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)

Theorembrdomg 6260* Dominance relation. (Contributed by NM, 15-Jun-1998.)

Theorembrdomi 6261* Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)

Theorembrdom 6262* Dominance relation. (Contributed by NM, 15-Jun-1998.)

Theoremdomen 6263* Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146. (Contributed by NM, 15-Jun-1998.)

Theoremdomeng 6264* Dominance in terms of equinumerosity, with the sethood requirement expressed as an antecedent. Example 1 of [Enderton] p. 146. (Contributed by NM, 24-Apr-2004.)

Theoremf1oen3g 6265 The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 6268 does not require the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro, 10-Sep-2015.)

Theoremf1oen2g 6266 The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 6268 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.)

Theoremf1dom2g 6267 The domain of a one-to-one function is dominated by its codomain. This variation of f1domg 6269 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)

Theoremf1oeng 6268 The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)

Theoremf1domg 6269 The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004.)

Theoremf1oen 6270 The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)

Theoremf1dom 6271 The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 19-Jun-1998.)

Theoremisfi 6272* Express " is finite." Definition 10.29 of [TakeutiZaring] p. 91 (whose " " is a predicate instead of a class). (Contributed by NM, 22-Aug-2008.)

Theoremenssdom 6273 Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)

Theoremendom 6274 Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.)

Theoremenrefg 6275 Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)

Theoremenref 6276 Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)

Theoremeqeng 6277 Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)

Theoremdomrefg 6278 Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)

Theoremen2d 6279* Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.)

Theoremen3d 6280* Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.)

Theoremen2i 6281* Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 4-Jan-2004.)

Theoremen3i 6282* Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 19-Jul-2004.)

Theoremdom2lem 6283* A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004.)

Theoremdom2d 6284* A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 20-May-2013.)

Theoremdom3d 6285* A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by Mario Carneiro, 20-May-2013.)

Theoremdom2 6286* A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. and can be read and , as can be inferred from their distinct variable conditions. (Contributed by NM, 26-Oct-2003.)

Theoremdom3 6287* A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. and can be read and , as can be inferred from their distinct variable conditions. (Contributed by Mario Carneiro, 20-May-2013.)

Theoremidssen 6288 Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)

Theoremssdomg 6289 A set dominates its subsets. Theorem 16 of [Suppes] p. 94. (Contributed by NM, 19-Jun-1998.) (Revised by Mario Carneiro, 24-Jun-2015.)

Theoremener 6290 Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)

Theoremensymb 6291 Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by Mario Carneiro, 26-Apr-2015.)

Theoremensym 6292 Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)

Theoremensymi 6293 Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)

Theoremensymd 6294 Symmetry of equinumerosity. Deduction form of ensym 6292. (Contributed by David Moews, 1-May-2017.)

Theorementr 6295 Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.)

Theoremdomtr 6296 Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94. (Contributed by NM, 4-Jun-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)

Theorementri 6297 A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)

Theorementr2i 6298 A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)

Theorementr3i 6299 A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)

Theorementr4i 6300 A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10511
 Copyright terms: Public domain < Previous  Next >