Theorem List for Intuitionistic Logic Explorer - 6601-6700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Syntax | cdom 6601 |
Extend class definition to include the dominance relation (curly
less-than-or-equal)
|
class ≼ |
|
Syntax | cfn 6602 |
Extend class definition to include the class of all finite sets.
|
class Fin |
|
Definition | df-en 6603* |
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 6609. (Contributed by NM, 28-Mar-1998.)
|
⊢ ≈ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦} |
|
Definition | df-dom 6604* |
Define the dominance relation. Compare Definition of [Enderton] p. 145.
Typical textbook definitions are derived as brdom 6612 and domen 6613.
(Contributed by NM, 28-Mar-1998.)
|
⊢ ≼ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} |
|
Definition | df-fin 6605* |
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 13101. (Contributed by NM,
22-Aug-2008.)
|
⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦} |
|
Theorem | relen 6606 |
Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
|
⊢ Rel ≈ |
|
Theorem | reldom 6607 |
Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
|
⊢ Rel ≼ |
|
Theorem | encv 6608 |
If two classes are equinumerous, both classes are sets. (Contributed by
AV, 21-Mar-2019.)
|
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
|
Theorem | bren 6609* |
Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
|
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
|
Theorem | brdomg 6610* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) |
|
Theorem | brdomi 6611* |
Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
|
Theorem | brdom 6612* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵) |
|
Theorem | domen 6613* |
Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146.
(Contributed by NM, 15-Jun-1998.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) |
|
Theorem | domeng 6614* |
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.)
|
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) |
|
Theorem | ctex 6615 |
A class dominated by ω is a set. See also ctfoex 6971 which says that
a countable class is a set. (Contributed by Thierry Arnoux, 29-Dec-2016.)
(Proof shortened by Jim Kingdon, 13-Mar-2023.)
|
⊢ (𝐴 ≼ ω → 𝐴 ∈ V) |
|
Theorem | f1oen3g 6616 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6619 does not require the Axiom of Replacement.
(Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro,
10-Sep-2015.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
|
Theorem | f1oen2g 6617 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6619 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 10-Sep-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
|
Theorem | f1dom2g 6618 |
The domain of a one-to-one function is dominated by its codomain. This
variation of f1domg 6620 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 24-Jun-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) |
|
Theorem | f1oeng 6619 |
The domain and range of a one-to-one, onto function are equinumerous.
(Contributed by NM, 19-Jun-1998.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
|
Theorem | f1domg 6620 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 4-Sep-2004.)
|
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵)) |
|
Theorem | f1oen 6621 |
The domain and range of a one-to-one, onto function are equinumerous.
(Contributed by NM, 19-Jun-1998.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐴 ≈ 𝐵) |
|
Theorem | f1dom 6622 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 19-Jun-1998.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵) |
|
Theorem | isfi 6623* |
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 ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) |
|
Theorem | enssdom 6624 |
Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
|
⊢ ≈ ⊆ ≼ |
|
Theorem | endom 6625 |
Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94.
(Contributed by NM, 28-May-1998.)
|
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵) |
|
Theorem | enrefg 6626 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴) |
|
Theorem | enref 6627 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ≈ 𝐴 |
|
Theorem | eqeng 6628 |
Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) |
|
Theorem | domrefg 6629 |
Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
|
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≼ 𝐴) |
|
Theorem | en2d 6630* |
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)) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → 𝐴 ≈ 𝐵) |
|
Theorem | en3d 6631* |
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) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)) & ⊢ (𝜑 → (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴)) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶))) ⇒ ⊢ (𝜑 → 𝐴 ≈ 𝐵) |
|
Theorem | en2i 6632* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 4-Jan-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ V) & ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ V) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷)) ⇒ ⊢ 𝐴 ≈ 𝐵 |
|
Theorem | en3i 6633* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 19-Jul-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)
& ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴)
& ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ 𝐴 ≈ 𝐵 |
|
Theorem | dom2lem 6634* |
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→𝐵) |
|
Theorem | dom2d 6635* |
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.)
|
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦))) ⇒ ⊢ (𝜑 → (𝐵 ∈ 𝑅 → 𝐴 ≼ 𝐵)) |
|
Theorem | dom3d 6636* |
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.)
|
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐴 ≼ 𝐵) |
|
Theorem | dom2 6637* |
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.)
|
⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)
& ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦)) ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐴 ≼ 𝐵) |
|
Theorem | dom3 6638* |
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.)
|
⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)
& ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ≼ 𝐵) |
|
Theorem | idssen 6639 |
Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ I ⊆ ≈ |
|
Theorem | ssdomg 6640 |
A set dominates its subsets. Theorem 16 of [Suppes] p. 94. (Contributed
by NM, 19-Jun-1998.) (Revised by Mario Carneiro, 24-Jun-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵)) |
|
Theorem | ener 6641 |
Equinumerosity is an equivalence relation. (Contributed by NM,
19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ≈ Er V |
|
Theorem | ensymb 6642 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴) |
|
Theorem | ensym 6643 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
|
Theorem | ensymi 6644 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵 ⇒ ⊢ 𝐵 ≈ 𝐴 |
|
Theorem | ensymd 6645 |
Symmetry of equinumerosity. Deduction form of ensym 6643. (Contributed
by David Moews, 1-May-2017.)
|
⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≈ 𝐴) |
|
Theorem | entr 6646 |
Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
(Contributed by NM, 9-Jun-1998.)
|
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) |
|
Theorem | domtr 6647 |
Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
(Contributed by NM, 4-Jun-1998.) (Revised by Mario Carneiro,
15-Nov-2014.)
|
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) |
|
Theorem | entri 6648 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐵 ≈ 𝐶 ⇒ ⊢ 𝐴 ≈ 𝐶 |
|
Theorem | entr2i 6649 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐵 ≈ 𝐶 ⇒ ⊢ 𝐶 ≈ 𝐴 |
|
Theorem | entr3i 6650 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐴 ≈ 𝐶 ⇒ ⊢ 𝐵 ≈ 𝐶 |
|
Theorem | entr4i 6651 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐶 ≈ 𝐵 ⇒ ⊢ 𝐴 ≈ 𝐶 |
|
Theorem | endomtr 6652 |
Transitivity of equinumerosity and dominance. (Contributed by NM,
7-Jun-1998.)
|
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) |
|
Theorem | domentr 6653 |
Transitivity of dominance and equinumerosity. (Contributed by NM,
7-Jun-1998.)
|
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶) |
|
Theorem | f1imaeng 6654 |
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→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐹 “ 𝐶) ≈ 𝐶) |
|
Theorem | f1imaen2g 6655 |
A one-to-one function's image under a subset of its domain is equinumerous
to the subset. (This version of f1imaen 6656 does not need ax-setind 4422.)
(Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro,
25-Jun-2015.)
|
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉)) → (𝐹 “ 𝐶) ≈ 𝐶) |
|
Theorem | f1imaen 6656 |
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→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 “ 𝐶) ≈ 𝐶) |
|
Theorem | en0 6657 |
The empty set is equinumerous only to itself. Exercise 1 of
[TakeutiZaring] p. 88.
(Contributed by NM, 27-May-1998.)
|
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) |
|
Theorem | ensn1 6658 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
4-Nov-2002.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ≈ 1o |
|
Theorem | ensn1g 6659 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
23-Apr-2004.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ 1o) |
|
Theorem | enpr1g 6660 |
{𝐴, 𝐴} has only one element.
(Contributed by FL, 15-Feb-2010.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐴} ≈ 1o) |
|
Theorem | en1 6661* |
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by NM, 25-Jul-2004.)
|
⊢ (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥}) |
|
Theorem | en1bg 6662 |
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by Jim Kingdon, 13-Apr-2020.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ≈ 1o ↔ 𝐴 = {∪ 𝐴})) |
|
Theorem | reuen1 6663* |
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28-Oct-2014.)
|
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} ≈ 1o) |
|
Theorem | euen1 6664 |
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28-Oct-2014.)
|
⊢ (∃!𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≈ 1o) |
|
Theorem | euen1b 6665* |
Two ways to express "𝐴 has a unique element".
(Contributed by
Mario Carneiro, 9-Apr-2015.)
|
⊢ (𝐴 ≈ 1o ↔ ∃!𝑥 𝑥 ∈ 𝐴) |
|
Theorem | en1uniel 6666 |
A singleton contains its sole element. (Contributed by Stefan O'Rear,
16-Aug-2015.)
|
⊢ (𝑆 ≈ 1o → ∪ 𝑆
∈ 𝑆) |
|
Theorem | 2dom 6667* |
A set that dominates ordinal 2 has at least 2 different members.
(Contributed by NM, 25-Jul-2004.)
|
⊢ (2o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦) |
|
Theorem | fundmen 6668 |
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 𝐹 ≈ 𝐹) |
|
Theorem | fundmeng 6669 |
A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98.
(Contributed by NM, 17-Sep-2013.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → dom 𝐹 ≈ 𝐹) |
|
Theorem | cnven 6670 |
A relational set is equinumerous to its converse. (Contributed by Mario
Carneiro, 28-Dec-2014.)
|
⊢ ((Rel 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ ◡𝐴) |
|
Theorem | cnvct 6671 |
If a set is dominated by ω, so is its converse.
(Contributed by
Thierry Arnoux, 29-Dec-2016.)
|
⊢ (𝐴 ≼ ω → ◡𝐴 ≼ ω) |
|
Theorem | fndmeng 6672 |
A function is equinumerate to its domain. (Contributed by Paul Chapman,
22-Jun-2011.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐴 ≈ 𝐹) |
|
Theorem | mapsnen 6673 |
Set exponentiation to a singleton exponent is equinumerous to its base.
Exercise 4.43 of [Mendelson] p. 255.
(Contributed by NM, 17-Dec-2003.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴 ↑𝑚 {𝐵}) ≈ 𝐴 |
|
Theorem | map1 6674 |
Set exponentiation: ordinal 1 to any set is equinumerous to ordinal 1.
Exercise 4.42(b) of [Mendelson] p.
255. (Contributed by NM,
17-Dec-2003.)
|
⊢ (𝐴 ∈ 𝑉 → (1o
↑𝑚 𝐴) ≈ 1o) |
|
Theorem | en2sn 6675 |
Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵}) |
|
Theorem | snfig 6676 |
A singleton is finite. For the proper class case, see snprc 3558.
(Contributed by Jim Kingdon, 13-Apr-2020.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Fin) |
|
Theorem | fiprc 6677 |
The class of finite sets is a proper class. (Contributed by Jeff
Hankins, 3-Oct-2008.)
|
⊢ Fin ∉ V |
|
Theorem | unen 6678 |
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.)
|
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝐴 ∪ 𝐶) ≈ (𝐵 ∪ 𝐷)) |
|
Theorem | enpr2d 6679 |
A pair with distinct elements is equinumerous to ordinal two.
(Contributed by Rohan Ridenour, 3-Aug-2023.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ (𝜑 → 𝐵 ∈ 𝐷)
& ⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o) |
|
Theorem | ssct 6680 |
A subset of a set dominated by ω is dominated by
ω.
(Contributed by Thierry Arnoux, 31-Jan-2017.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω) → 𝐴 ≼ ω) |
|
Theorem | 1domsn 6681 |
A singleton (whether of a set or a proper class) is dominated by one.
(Contributed by Jim Kingdon, 1-Mar-2022.)
|
⊢ {𝐴} ≼ 1o |
|
Theorem | enm 6682* |
A set equinumerous to an inhabited set is inhabited. (Contributed by
Jim Kingdon, 19-May-2020.)
|
⊢ ((𝐴 ≈ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ 𝐵) |
|
Theorem | xpsnen 6683 |
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 ⇒ ⊢ (𝐴 × {𝐵}) ≈ 𝐴 |
|
Theorem | xpsneng 6684 |
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.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × {𝐵}) ≈ 𝐴) |
|
Theorem | xp1en 6685 |
One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised
by Mario Carneiro, 29-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 1o) ≈ 𝐴) |
|
Theorem | endisj 6686* |
Any two sets are equinumerous to disjoint sets. Exercise 4.39 of
[Mendelson] p. 255. (Contributed by
NM, 16-Apr-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∃𝑥∃𝑦((𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵) ∧ (𝑥 ∩ 𝑦) = ∅) |
|
Theorem | xpcomf1o 6687* |
The canonical bijection from (𝐴 × 𝐵) to (𝐵 × 𝐴).
(Contributed by Mario Carneiro, 23-Apr-2014.)
|
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪
◡{𝑥}) ⇒ ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) |
|
Theorem | xpcomco 6688* |
Composition with the bijection of xpcomf1o 6687 swaps the arguments to a
mapping. (Contributed by Mario Carneiro, 30-May-2015.)
|
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪
◡{𝑥})
& ⊢ 𝐺 = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝐺 ∘ 𝐹) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
|
Theorem | xpcomen 6689 |
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 ⇒ ⊢ (𝐴 × 𝐵) ≈ (𝐵 × 𝐴) |
|
Theorem | xpcomeng 6690 |
Commutative law for equinumerosity of Cartesian product. Proposition
4.22(d) of [Mendelson] p. 254.
(Contributed by NM, 27-Mar-2006.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)) |
|
Theorem | xpsnen2g 6691 |
A set is equinumerous to its Cartesian product with a singleton on the
left. (Contributed by Stefan O'Rear, 21-Nov-2014.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × 𝐵) ≈ 𝐵) |
|
Theorem | xpassen 6692 |
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 ⇒ ⊢ ((𝐴 × 𝐵) × 𝐶) ≈ (𝐴 × (𝐵 × 𝐶)) |
|
Theorem | xpdom2 6693 |
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 ⇒ ⊢ (𝐴 ≼ 𝐵 → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵)) |
|
Theorem | xpdom2g 6694 |
Dominance law for Cartesian product. Theorem 6L(c) of [Enderton]
p. 149. (Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵)) |
|
Theorem | xpdom1g 6695 |
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.)
|
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵) → (𝐴 × 𝐶) ≼ (𝐵 × 𝐶)) |
|
Theorem | xpdom3m 6696* |
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.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ∃𝑥 𝑥 ∈ 𝐵) → 𝐴 ≼ (𝐴 × 𝐵)) |
|
Theorem | xpdom1 6697 |
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 ⇒ ⊢ (𝐴 ≼ 𝐵 → (𝐴 × 𝐶) ≼ (𝐵 × 𝐶)) |
|
Theorem | fopwdom 6698 |
Covering implies injection on power sets. (Contributed by Stefan
O'Rear, 6-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.)
|
⊢ ((𝐹 ∈ V ∧ 𝐹:𝐴–onto→𝐵) → 𝒫 𝐵 ≼ 𝒫 𝐴) |
|
Theorem | 0domg 6699 |
Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴) |
|
Theorem | dom0 6700 |
A set dominated by the empty set is empty. (Contributed by NM,
22-Nov-2004.)
|
⊢ (𝐴 ≼ ∅ ↔ 𝐴 = ∅) |