 Home Intuitionistic Logic ExplorerTheorem List (p. 63 of 100) < Previous  Next > Bad symbols? Try the GIF 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

Theoremecovicom 6201* Lemma used to transfer a commutative law via an equivalence relation. (Contributed by Jim Kingdon, 15-Sep-2019.)
𝐶 = ((𝑆 × 𝑆) / )    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆)) → ([⟨𝑥, 𝑦⟩] + [⟨𝑧, 𝑤⟩] ) = [⟨𝐷, 𝐺⟩] )    &   (((𝑧𝑆𝑤𝑆) ∧ (𝑥𝑆𝑦𝑆)) → ([⟨𝑧, 𝑤⟩] + [⟨𝑥, 𝑦⟩] ) = [⟨𝐻, 𝐽⟩] )    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆)) → 𝐷 = 𝐻)    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆)) → 𝐺 = 𝐽)       ((𝐴𝐶𝐵𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴))

Theoremecovass 6202* Lemma used to transfer an associative law via an equivalence relation. In most cases ecoviass 6203 will be more useful. (Contributed by NM, 31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
𝐷 = ((𝑆 × 𝑆) / )    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆)) → ([⟨𝑥, 𝑦⟩] + [⟨𝑧, 𝑤⟩] ) = [⟨𝐺, 𝐻⟩] )    &   (((𝑧𝑆𝑤𝑆) ∧ (𝑣𝑆𝑢𝑆)) → ([⟨𝑧, 𝑤⟩] + [⟨𝑣, 𝑢⟩] ) = [⟨𝑁, 𝑄⟩] )    &   (((𝐺𝑆𝐻𝑆) ∧ (𝑣𝑆𝑢𝑆)) → ([⟨𝐺, 𝐻⟩] + [⟨𝑣, 𝑢⟩] ) = [⟨𝐽, 𝐾⟩] )    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑁𝑆𝑄𝑆)) → ([⟨𝑥, 𝑦⟩] + [⟨𝑁, 𝑄⟩] ) = [⟨𝐿, 𝑀⟩] )    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆)) → (𝐺𝑆𝐻𝑆))    &   (((𝑧𝑆𝑤𝑆) ∧ (𝑣𝑆𝑢𝑆)) → (𝑁𝑆𝑄𝑆))    &   𝐽 = 𝐿    &   𝐾 = 𝑀       ((𝐴𝐷𝐵𝐷𝐶𝐷) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Theoremecoviass 6203* Lemma used to transfer an associative law via an equivalence relation. (Contributed by Jim Kingdon, 16-Sep-2019.)
𝐷 = ((𝑆 × 𝑆) / )    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆)) → ([⟨𝑥, 𝑦⟩] + [⟨𝑧, 𝑤⟩] ) = [⟨𝐺, 𝐻⟩] )    &   (((𝑧𝑆𝑤𝑆) ∧ (𝑣𝑆𝑢𝑆)) → ([⟨𝑧, 𝑤⟩] + [⟨𝑣, 𝑢⟩] ) = [⟨𝑁, 𝑄⟩] )    &   (((𝐺𝑆𝐻𝑆) ∧ (𝑣𝑆𝑢𝑆)) → ([⟨𝐺, 𝐻⟩] + [⟨𝑣, 𝑢⟩] ) = [⟨𝐽, 𝐾⟩] )    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑁𝑆𝑄𝑆)) → ([⟨𝑥, 𝑦⟩] + [⟨𝑁, 𝑄⟩] ) = [⟨𝐿, 𝑀⟩] )    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆)) → (𝐺𝑆𝐻𝑆))    &   (((𝑧𝑆𝑤𝑆) ∧ (𝑣𝑆𝑢𝑆)) → (𝑁𝑆𝑄𝑆))    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆) ∧ (𝑣𝑆𝑢𝑆)) → 𝐽 = 𝐿)    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆) ∧ (𝑣𝑆𝑢𝑆)) → 𝐾 = 𝑀)       ((𝐴𝐷𝐵𝐷𝐶𝐷) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Theoremecovdi 6204* Lemma used to transfer a distributive law via an equivalence relation. Most likely ecovidi 6205 will be more helpful. (Contributed by NM, 2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
𝐷 = ((𝑆 × 𝑆) / )    &   (((𝑧𝑆𝑤𝑆) ∧ (𝑣𝑆𝑢𝑆)) → ([⟨𝑧, 𝑤⟩] + [⟨𝑣, 𝑢⟩] ) = [⟨𝑀, 𝑁⟩] )    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑀𝑆𝑁𝑆)) → ([⟨𝑥, 𝑦⟩] · [⟨𝑀, 𝑁⟩] ) = [⟨𝐻, 𝐽⟩] )    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆)) → ([⟨𝑥, 𝑦⟩] · [⟨𝑧, 𝑤⟩] ) = [⟨𝑊, 𝑋⟩] )    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑣𝑆𝑢𝑆)) → ([⟨𝑥, 𝑦⟩] · [⟨𝑣, 𝑢⟩] ) = [⟨𝑌, 𝑍⟩] )    &   (((𝑊𝑆𝑋𝑆) ∧ (𝑌𝑆𝑍𝑆)) → ([⟨𝑊, 𝑋⟩] + [⟨𝑌, 𝑍⟩] ) = [⟨𝐾, 𝐿⟩] )    &   (((𝑧𝑆𝑤𝑆) ∧ (𝑣𝑆𝑢𝑆)) → (𝑀𝑆𝑁𝑆))    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆)) → (𝑊𝑆𝑋𝑆))    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑣𝑆𝑢𝑆)) → (𝑌𝑆𝑍𝑆))    &   𝐻 = 𝐾    &   𝐽 = 𝐿       ((𝐴𝐷𝐵𝐷𝐶𝐷) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Theoremecovidi 6205* Lemma used to transfer a distributive law via an equivalence relation. (Contributed by Jim Kingdon, 17-Sep-2019.)
𝐷 = ((𝑆 × 𝑆) / )    &   (((𝑧𝑆𝑤𝑆) ∧ (𝑣𝑆𝑢𝑆)) → ([⟨𝑧, 𝑤⟩] + [⟨𝑣, 𝑢⟩] ) = [⟨𝑀, 𝑁⟩] )    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑀𝑆𝑁𝑆)) → ([⟨𝑥, 𝑦⟩] · [⟨𝑀, 𝑁⟩] ) = [⟨𝐻, 𝐽⟩] )    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆)) → ([⟨𝑥, 𝑦⟩] · [⟨𝑧, 𝑤⟩] ) = [⟨𝑊, 𝑋⟩] )    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑣𝑆𝑢𝑆)) → ([⟨𝑥, 𝑦⟩] · [⟨𝑣, 𝑢⟩] ) = [⟨𝑌, 𝑍⟩] )    &   (((𝑊𝑆𝑋𝑆) ∧ (𝑌𝑆𝑍𝑆)) → ([⟨𝑊, 𝑋⟩] + [⟨𝑌, 𝑍⟩] ) = [⟨𝐾, 𝐿⟩] )    &   (((𝑧𝑆𝑤𝑆) ∧ (𝑣𝑆𝑢𝑆)) → (𝑀𝑆𝑁𝑆))    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆)) → (𝑊𝑆𝑋𝑆))    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑣𝑆𝑢𝑆)) → (𝑌𝑆𝑍𝑆))    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆) ∧ (𝑣𝑆𝑢𝑆)) → 𝐻 = 𝐾)    &   (((𝑥𝑆𝑦𝑆) ∧ (𝑧𝑆𝑤𝑆) ∧ (𝑣𝑆𝑢𝑆)) → 𝐽 = 𝐿)       ((𝐴𝐷𝐵𝐷𝐶𝐷) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

2.6.25  Equinumerosity

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

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

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

Definitiondf-en 6209* 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 6215. (Contributed by NM, 28-Mar-1998.)
≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1-onto𝑦}

Definitiondf-dom 6210* Define the dominance relation. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 6218 and domen 6219. (Contributed by NM, 28-Mar-1998.)
≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1𝑦}

Definitiondf-fin 6211* Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our "𝑎 ∈ Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 9974. (Contributed by NM, 22-Aug-2008.)
Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥𝑦}

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

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

Theoremencv 6214 If two classes are equinumerous, both classes are sets. (Contributed by AV, 21-Mar-2019.)
(𝐴𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))

Theorembren 6215* Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
(𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵)

Theorembrdomg 6216* Dominance relation. (Contributed by NM, 15-Jun-1998.)
(𝐵𝐶 → (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1𝐵))

Theorembrdomi 6217* Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)
(𝐴𝐵 → ∃𝑓 𝑓:𝐴1-1𝐵)

Theorembrdom 6218* Dominance relation. (Contributed by NM, 15-Jun-1998.)
𝐵 ∈ V       (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1𝐵)

Theoremdomen 6219* Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146. (Contributed by NM, 15-Jun-1998.)
𝐵 ∈ V       (𝐴𝐵 ↔ ∃𝑥(𝐴𝑥𝑥𝐵))

Theoremdomeng 6220* 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 6221 The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 6224 does not require the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro, 10-Sep-2015.)
((𝐹𝑉𝐹:𝐴1-1-onto𝐵) → 𝐴𝐵)

Theoremf1oen2g 6222 The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 6224 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.)
((𝐴𝑉𝐵𝑊𝐹:𝐴1-1-onto𝐵) → 𝐴𝐵)

Theoremf1dom2g 6223 The domain of a one-to-one function is dominated by its codomain. This variation of f1domg 6225 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
((𝐴𝑉𝐵𝑊𝐹:𝐴1-1𝐵) → 𝐴𝐵)

Theoremf1oeng 6224 The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)
((𝐴𝐶𝐹:𝐴1-1-onto𝐵) → 𝐴𝐵)

Theoremf1domg 6225 The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004.)
(𝐵𝐶 → (𝐹:𝐴1-1𝐵𝐴𝐵))

Theoremf1oen 6226 The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)
𝐴 ∈ V       (𝐹:𝐴1-1-onto𝐵𝐴𝐵)

Theoremf1dom 6227 The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 19-Jun-1998.)
𝐵 ∈ V       (𝐹:𝐴1-1𝐵𝐴𝐵)

Theoremisfi 6228* Express "𝐴 is finite." Definition 10.29 of [TakeutiZaring] p. 91 (whose "Fin " is a predicate instead of a class). (Contributed by NM, 22-Aug-2008.)
(𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)

Theoremenssdom 6229 Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
≈ ⊆ ≼

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

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

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

Theoremeqeng 6233 Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
(𝐴𝑉 → (𝐴 = 𝐵𝐴𝐵))

Theoremdomrefg 6234 Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
(𝐴𝑉𝐴𝐴)

Theoremen2d 6235* Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.)
(𝜑𝐴 ∈ V)    &   (𝜑𝐵 ∈ V)    &   (𝜑 → (𝑥𝐴𝐶 ∈ V))    &   (𝜑 → (𝑦𝐵𝐷 ∈ V))    &   (𝜑 → ((𝑥𝐴𝑦 = 𝐶) ↔ (𝑦𝐵𝑥 = 𝐷)))       (𝜑𝐴𝐵)

Theoremen3d 6236* Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.)
(𝜑𝐴 ∈ V)    &   (𝜑𝐵 ∈ V)    &   (𝜑 → (𝑥𝐴𝐶𝐵))    &   (𝜑 → (𝑦𝐵𝐷𝐴))    &   (𝜑 → ((𝑥𝐴𝑦𝐵) → (𝑥 = 𝐷𝑦 = 𝐶)))       (𝜑𝐴𝐵)

Theoremen2i 6237* Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 4-Jan-2004.)
𝐴 ∈ V    &   𝐵 ∈ V    &   (𝑥𝐴𝐶 ∈ V)    &   (𝑦𝐵𝐷 ∈ V)    &   ((𝑥𝐴𝑦 = 𝐶) ↔ (𝑦𝐵𝑥 = 𝐷))       𝐴𝐵

Theoremen3i 6238* Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 19-Jul-2004.)
𝐴 ∈ V    &   𝐵 ∈ V    &   (𝑥𝐴𝐶𝐵)    &   (𝑦𝐵𝐷𝐴)    &   ((𝑥𝐴𝑦𝐵) → (𝑥 = 𝐷𝑦 = 𝐶))       𝐴𝐵

Theoremdom2lem 6239* 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.)
(𝜑 → (𝑥𝐴𝐶𝐵))    &   (𝜑 → ((𝑥𝐴𝑦𝐴) → (𝐶 = 𝐷𝑥 = 𝑦)))       (𝜑 → (𝑥𝐴𝐶):𝐴1-1𝐵)

Theoremdom2d 6240* 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 6241* 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 6242* 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 6243* 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 6244 Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
I ⊆ ≈

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

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

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

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

Theoremensymd 6250 Symmetry of equinumerosity. Deduction form of ensym 6248. (Contributed by David Moews, 1-May-2017.)
(𝜑𝐴𝐵)       (𝜑𝐵𝐴)

Theorementr 6251 Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.)
((𝐴𝐵𝐵𝐶) → 𝐴𝐶)

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

Theorementri 6253 A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
𝐴𝐵    &   𝐵𝐶       𝐴𝐶

Theorementr2i 6254 A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
𝐴𝐵    &   𝐵𝐶       𝐶𝐴

Theorementr3i 6255 A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
𝐴𝐵    &   𝐴𝐶       𝐵𝐶

Theorementr4i 6256 A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
𝐴𝐵    &   𝐶𝐵       𝐴𝐶

Theoremendomtr 6257 Transitivity of equinumerosity and dominance. (Contributed by NM, 7-Jun-1998.)
((𝐴𝐵𝐵𝐶) → 𝐴𝐶)

Theoremdomentr 6258 Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.)
((𝐴𝐵𝐵𝐶) → 𝐴𝐶)

Theoremf1imaeng 6259 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.)
((𝐹:𝐴1-1𝐵𝐶𝐴𝐶𝑉) → (𝐹𝐶) ≈ 𝐶)

Theoremf1imaen2g 6260 A one-to-one function's image under a subset of its domain is equinumerous to the subset. (This version of f1imaen 6261 does not need ax-setind 4256.) (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.)
(((𝐹:𝐴1-1𝐵𝐵𝑉) ∧ (𝐶𝐴𝐶𝑉)) → (𝐹𝐶) ≈ 𝐶)

Theoremf1imaen 6261 A one-to-one function's image under a subset of its domain is equinumerous to the subset. (Contributed by NM, 30-Sep-2004.)
𝐶 ∈ V       ((𝐹:𝐴1-1𝐵𝐶𝐴) → (𝐹𝐶) ≈ 𝐶)

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

Theoremensn1 6263 A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.)
𝐴 ∈ V       {𝐴} ≈ 1𝑜

Theoremensn1g 6264 A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004.)
(𝐴𝑉 → {𝐴} ≈ 1𝑜)

Theoremenpr1g 6265 {𝐴, 𝐴} has only one element. (Contributed by FL, 15-Feb-2010.)
(𝐴𝑉 → {𝐴, 𝐴} ≈ 1𝑜)

Theoremen1 6266* A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004.)
(𝐴 ≈ 1𝑜 ↔ ∃𝑥 𝐴 = {𝑥})

Theoremen1bg 6267 A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Jim Kingdon, 13-Apr-2020.)
(𝐴𝑉 → (𝐴 ≈ 1𝑜𝐴 = { 𝐴}))

Theoremreuen1 6268* Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
(∃!𝑥𝐴 𝜑 ↔ {𝑥𝐴𝜑} ≈ 1𝑜)

Theoremeuen1 6269 Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
(∃!𝑥𝜑 ↔ {𝑥𝜑} ≈ 1𝑜)

Theoremeuen1b 6270* Two ways to express "𝐴 has a unique element". (Contributed by Mario Carneiro, 9-Apr-2015.)
(𝐴 ≈ 1𝑜 ↔ ∃!𝑥 𝑥𝐴)

Theoremen1uniel 6271 A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015.)
(𝑆 ≈ 1𝑜 𝑆𝑆)

Theorem2dom 6272* A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004.)
(2𝑜𝐴 → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 = 𝑦)

Theoremfundmen 6273 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.)
𝐹 ∈ V       (Fun 𝐹 → dom 𝐹𝐹)

Theoremfundmeng 6274 A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 17-Sep-2013.)
((𝐹𝑉 ∧ Fun 𝐹) → dom 𝐹𝐹)

Theoremcnven 6275 A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014.)
((Rel 𝐴𝐴𝑉) → 𝐴𝐴)

Theoremfndmeng 6276 A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.)
((𝐹 Fn 𝐴𝐴𝐶) → 𝐴𝐹)

Theoremen2sn 6277 Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.)
((𝐴𝐶𝐵𝐷) → {𝐴} ≈ {𝐵})

Theoremsnfig 6278 A singleton is finite. (Contributed by Jim Kingdon, 13-Apr-2020.)
(𝐴𝑉 → {𝐴} ∈ Fin)

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

Theoremunen 6280 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 6281* A set equinumerous to an inhabited set is inhabited. (Contributed by Jim Kingdon, 19-May-2020.)
((𝐴𝐵 ∧ ∃𝑥 𝑥𝐴) → ∃𝑦 𝑦𝐵)

Theoremxpsnen 6282 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.)
𝐴 ∈ V    &   𝐵 ∈ V       (𝐴 × {𝐵}) ≈ 𝐴

Theoremxpsneng 6283 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 6284 One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
(𝐴𝑉 → (𝐴 × 1𝑜) ≈ 𝐴)

Theoremendisj 6285* Any two sets are equinumerous to disjoint sets. Exercise 4.39 of [Mendelson] p. 255. (Contributed by NM, 16-Apr-2004.)
𝐴 ∈ V    &   𝐵 ∈ V       𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ (𝑥𝑦) = ∅)

Theoremxpcomf1o 6286* The canonical bijection from (𝐴 × 𝐵) to (𝐵 × 𝐴). (Contributed by Mario Carneiro, 23-Apr-2014.)
𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ {𝑥})       𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴)

Theoremxpcomco 6287* Composition with the bijection of xpcomf1o 6286 swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015.)
𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ {𝑥})    &   𝐺 = (𝑦𝐵, 𝑧𝐴𝐶)       (𝐺𝐹) = (𝑧𝐴, 𝑦𝐵𝐶)

Theoremxpcomen 6288 Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 5-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
𝐴 ∈ V    &   𝐵 ∈ V       (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)

Theoremxpcomeng 6289 Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 27-Mar-2006.)
((𝐴𝑉𝐵𝑊) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴))

Theoremxpsnen2g 6290 A set is equinumerous to its Cartesian product with a singleton on the left. (Contributed by Stefan O'Rear, 21-Nov-2014.)
((𝐴𝑉𝐵𝑊) → ({𝐴} × 𝐵) ≈ 𝐵)

Theoremxpassen 6291 Associative law for equinumerosity of Cartesian product. Proposition 4.22(e) of [Mendelson] p. 254. (Contributed by NM, 22-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V       ((𝐴 × 𝐵) × 𝐶) ≈ (𝐴 × (𝐵 × 𝐶))

Theoremxpdom2 6292 Dominance law for Cartesian product. Proposition 10.33(2) of [TakeutiZaring] p. 92. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
𝐶 ∈ V       (𝐴𝐵 → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))

Theoremxpdom2g 6293 Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by Mario Carneiro, 26-Apr-2015.)
((𝐶𝑉𝐴𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))

Theoremxpdom1g 6294 Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 25-Mar-2006.) (Revised by Mario Carneiro, 26-Apr-2015.)
((𝐶𝑉𝐴𝐵) → (𝐴 × 𝐶) ≼ (𝐵 × 𝐶))

Theoremxpdom3m 6295* A set is dominated by its Cartesian product with an inhabited set. Exercise 6 of [Suppes] p. 98. (Contributed by Jim Kingdon, 15-Apr-2020.)
((𝐴𝑉𝐵𝑊 ∧ ∃𝑥 𝑥𝐵) → 𝐴 ≼ (𝐴 × 𝐵))

Theoremxpdom1 6296 Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 28-Sep-2004.) (Revised by NM, 29-Mar-2006.) (Revised by Mario Carneiro, 7-May-2015.)
𝐶 ∈ V       (𝐴𝐵 → (𝐴 × 𝐶) ≼ (𝐵 × 𝐶))

Theoremfopwdom 6297 Covering implies injection on power sets. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.)
((𝐹 ∈ V ∧ 𝐹:𝐴onto𝐵) → 𝒫 𝐵 ≼ 𝒫 𝐴)

Theoremenen1 6298 Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.)
(𝐴𝐵 → (𝐴𝐶𝐵𝐶))

Theoremenen2 6299 Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.)
(𝐴𝐵 → (𝐶𝐴𝐶𝐵))

Theoremdomen1 6300 Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.)
(𝐴𝐵 → (𝐴𝐶𝐵𝐶))

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