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

Theoremecopoveq 6201* 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 6202* 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 6203* 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 6204* 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 6205* Assuming the operation is commutative, show that the relation , specified by the first hypothesis, is symmetric. (Contributed by Jim Kingdon, 1-Sep-2019.)

Theoremecopovtrng 6206* 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 6207* 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 6208* 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 6209* 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 6210* Corollary of Theorem 3Q of [Enderton] p. 60. (Contributed by NM, 12-Nov-1995.) (Revised by David Abernethy, 4-Jun-2013.)

Theoremth3q 6211* 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 6212* 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 6213* Lemma used to transfer a commutative law via an equivalence relation. Most uses will want ecovicom 6214 instead. (Contributed by NM, 29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)

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

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

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

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

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

2.6.25  Equinumerosity

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

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

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

Definitiondf-en 6222* 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 6228. (Contributed by NM, 28-Mar-1998.)

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

Definitiondf-fin 6224* 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 10101. (Contributed by NM, 22-Aug-2008.)

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

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

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

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

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

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

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

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

Theoremdomeng 6233* 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 6234 The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 6237 does not require the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro, 10-Sep-2015.)

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

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

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

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

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

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

Theoremisfi 6241* 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 6242 Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)

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

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

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

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

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

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

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

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

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

Theoremdom2lem 6252* 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 6253* 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 6254* 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 6255* 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 6256* 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 6257 Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)

Theoremssdomg 6258 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 6259 Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)

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

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

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

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

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

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

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

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

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

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

Theoremendomtr 6270 Transitivity of equinumerosity and dominance. (Contributed by NM, 7-Jun-1998.)

Theoremdomentr 6271 Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.)

Theoremf1imaeng 6272 A one-to-one function's image under a subset of its domain is equinumerous to the subset. (Contributed by Mario Carneiro, 15-May-2015.)

Theoremf1imaen2g 6273 A one-to-one function's image under a subset of its domain is equinumerous to the subset. (This version of f1imaen 6274 does not need ax-setind 4262.) (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.)

Theoremf1imaen 6274 A one-to-one function's image under a subset of its domain is equinumerous to the subset. (Contributed by NM, 30-Sep-2004.)

Theoremen0 6275 The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.)

Theoremensn1 6276 A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.)

Theoremensn1g 6277 A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004.)

Theoremenpr1g 6278 has only one element. (Contributed by FL, 15-Feb-2010.)

Theoremen1 6279* A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004.)

Theoremen1bg 6280 A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Jim Kingdon, 13-Apr-2020.)

Theoremreuen1 6281* Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)

Theoremeuen1 6282 Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)

Theoremeuen1b 6283* Two ways to express " has a unique element". (Contributed by Mario Carneiro, 9-Apr-2015.)

Theoremen1uniel 6284 A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015.)

Theorem2dom 6285* A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004.)

Theoremfundmen 6286 A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 28-Jul-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)

Theoremfundmeng 6287 A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 17-Sep-2013.)

Theoremcnven 6288 A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014.)

Theoremfndmeng 6289 A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.)

Theoremen2sn 6290 Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.)

Theoremsnfig 6291 A singleton is finite. (Contributed by Jim Kingdon, 13-Apr-2020.)

Theoremfiprc 6292 The class of finite sets is a proper class. (Contributed by Jeff Hankins, 3-Oct-2008.)

Theoremunen 6293 Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)

Theoremenm 6294* A set equinumerous to an inhabited set is inhabited. (Contributed by Jim Kingdon, 19-May-2020.)

Theoremxpsnen 6295 A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254. (Contributed by NM, 4-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)

Theoremxpsneng 6296 A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254. (Contributed by NM, 22-Oct-2004.)

Theoremxp1en 6297 One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)

Theoremendisj 6298* Any two sets are equinumerous to disjoint sets. Exercise 4.39 of [Mendelson] p. 255. (Contributed by NM, 16-Apr-2004.)

Theoremxpcomf1o 6299* The canonical bijection from to . (Contributed by Mario Carneiro, 23-Apr-2014.)

Theoremxpcomco 6300* Composition with the bijection of xpcomf1o 6299 swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015.)

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-10124
 Copyright terms: Public domain < Previous  Next >