Theorem List for Intuitionistic Logic Explorer - 6701-6800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | relen 6701 |
Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
|
⊢ Rel ≈ |
|
Theorem | reldom 6702 |
Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
|
⊢ Rel ≼ |
|
Theorem | encv 6703 |
If two classes are equinumerous, both classes are sets. (Contributed by
AV, 21-Mar-2019.)
|
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
|
Theorem | bren 6704* |
Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
|
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
|
Theorem | brdomg 6705* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) |
|
Theorem | brdomi 6706* |
Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
|
Theorem | brdom 6707* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵) |
|
Theorem | domen 6708* |
Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146.
(Contributed by NM, 15-Jun-1998.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) |
|
Theorem | domeng 6709* |
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 6710 |
A class dominated by ω is a set. See also ctfoex 7074 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 6711 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6714 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 6712 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6714 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 10-Sep-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
|
Theorem | f1dom2g 6713 |
The domain of a one-to-one function is dominated by its codomain. This
variation of f1domg 6715 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 24-Jun-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) |
|
Theorem | f1oeng 6714 |
The domain and range of a one-to-one, onto function are equinumerous.
(Contributed by NM, 19-Jun-1998.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
|
Theorem | f1domg 6715 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 4-Sep-2004.)
|
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵)) |
|
Theorem | f1oen 6716 |
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 6717 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 19-Jun-1998.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵) |
|
Theorem | isfi 6718* |
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 6719 |
Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
|
⊢ ≈ ⊆ ≼ |
|
Theorem | endom 6720 |
Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94.
(Contributed by NM, 28-May-1998.)
|
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵) |
|
Theorem | enrefg 6721 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴) |
|
Theorem | enref 6722 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ≈ 𝐴 |
|
Theorem | eqeng 6723 |
Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) |
|
Theorem | domrefg 6724 |
Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
|
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≼ 𝐴) |
|
Theorem | en2d 6725* |
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 6726* |
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 6727* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 4-Jan-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ V) & ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ V) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷)) ⇒ ⊢ 𝐴 ≈ 𝐵 |
|
Theorem | en3i 6728* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 19-Jul-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)
& ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴)
& ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ 𝐴 ≈ 𝐵 |
|
Theorem | dom2lem 6729* |
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 6730* |
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 6731* |
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 6732* |
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 6733* |
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 6734 |
Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ I ⊆ ≈ |
|
Theorem | ssdomg 6735 |
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 6736 |
Equinumerosity is an equivalence relation. (Contributed by NM,
19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ≈ Er V |
|
Theorem | ensymb 6737 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴) |
|
Theorem | ensym 6738 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
|
Theorem | ensymi 6739 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵 ⇒ ⊢ 𝐵 ≈ 𝐴 |
|
Theorem | ensymd 6740 |
Symmetry of equinumerosity. Deduction form of ensym 6738. (Contributed
by David Moews, 1-May-2017.)
|
⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≈ 𝐴) |
|
Theorem | entr 6741 |
Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
(Contributed by NM, 9-Jun-1998.)
|
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) |
|
Theorem | domtr 6742 |
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 6743 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐵 ≈ 𝐶 ⇒ ⊢ 𝐴 ≈ 𝐶 |
|
Theorem | entr2i 6744 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐵 ≈ 𝐶 ⇒ ⊢ 𝐶 ≈ 𝐴 |
|
Theorem | entr3i 6745 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐴 ≈ 𝐶 ⇒ ⊢ 𝐵 ≈ 𝐶 |
|
Theorem | entr4i 6746 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐶 ≈ 𝐵 ⇒ ⊢ 𝐴 ≈ 𝐶 |
|
Theorem | endomtr 6747 |
Transitivity of equinumerosity and dominance. (Contributed by NM,
7-Jun-1998.)
|
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) |
|
Theorem | domentr 6748 |
Transitivity of dominance and equinumerosity. (Contributed by NM,
7-Jun-1998.)
|
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶) |
|
Theorem | f1imaeng 6749 |
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 6750 |
A one-to-one function's image under a subset of its domain is equinumerous
to the subset. (This version of f1imaen 6751 does not need ax-setind 4508.)
(Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro,
25-Jun-2015.)
|
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉)) → (𝐹 “ 𝐶) ≈ 𝐶) |
|
Theorem | f1imaen 6751 |
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 6752 |
The empty set is equinumerous only to itself. Exercise 1 of
[TakeutiZaring] p. 88.
(Contributed by NM, 27-May-1998.)
|
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) |
|
Theorem | ensn1 6753 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
4-Nov-2002.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ≈ 1o |
|
Theorem | ensn1g 6754 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
23-Apr-2004.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ 1o) |
|
Theorem | enpr1g 6755 |
{𝐴, 𝐴} has only one element.
(Contributed by FL, 15-Feb-2010.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐴} ≈ 1o) |
|
Theorem | en1 6756* |
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by NM, 25-Jul-2004.)
|
⊢ (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥}) |
|
Theorem | en1bg 6757 |
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by Jim Kingdon, 13-Apr-2020.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ≈ 1o ↔ 𝐴 = {∪ 𝐴})) |
|
Theorem | reuen1 6758* |
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28-Oct-2014.)
|
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} ≈ 1o) |
|
Theorem | euen1 6759 |
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28-Oct-2014.)
|
⊢ (∃!𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≈ 1o) |
|
Theorem | euen1b 6760* |
Two ways to express "𝐴 has a unique element".
(Contributed by
Mario Carneiro, 9-Apr-2015.)
|
⊢ (𝐴 ≈ 1o ↔ ∃!𝑥 𝑥 ∈ 𝐴) |
|
Theorem | en1uniel 6761 |
A singleton contains its sole element. (Contributed by Stefan O'Rear,
16-Aug-2015.)
|
⊢ (𝑆 ≈ 1o → ∪ 𝑆
∈ 𝑆) |
|
Theorem | 2dom 6762* |
A set that dominates ordinal 2 has at least 2 different members.
(Contributed by NM, 25-Jul-2004.)
|
⊢ (2o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦) |
|
Theorem | fundmen 6763 |
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 6764 |
A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98.
(Contributed by NM, 17-Sep-2013.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → dom 𝐹 ≈ 𝐹) |
|
Theorem | cnven 6765 |
A relational set is equinumerous to its converse. (Contributed by Mario
Carneiro, 28-Dec-2014.)
|
⊢ ((Rel 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ ◡𝐴) |
|
Theorem | cnvct 6766 |
If a set is dominated by ω, so is its converse.
(Contributed by
Thierry Arnoux, 29-Dec-2016.)
|
⊢ (𝐴 ≼ ω → ◡𝐴 ≼ ω) |
|
Theorem | fndmeng 6767 |
A function is equinumerate to its domain. (Contributed by Paul Chapman,
22-Jun-2011.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐴 ≈ 𝐹) |
|
Theorem | mapsnen 6768 |
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 6769 |
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 6770 |
Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵}) |
|
Theorem | snfig 6771 |
A singleton is finite. For the proper class case, see snprc 3635.
(Contributed by Jim Kingdon, 13-Apr-2020.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Fin) |
|
Theorem | fiprc 6772 |
The class of finite sets is a proper class. (Contributed by Jeff
Hankins, 3-Oct-2008.)
|
⊢ Fin ∉ V |
|
Theorem | unen 6773 |
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 6774 |
A pair with distinct elements is equinumerous to ordinal two.
(Contributed by Rohan Ridenour, 3-Aug-2023.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ (𝜑 → 𝐵 ∈ 𝐷)
& ⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o) |
|
Theorem | ssct 6775 |
A subset of a set dominated by ω is dominated by
ω.
(Contributed by Thierry Arnoux, 31-Jan-2017.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω) → 𝐴 ≼ ω) |
|
Theorem | 1domsn 6776 |
A singleton (whether of a set or a proper class) is dominated by one.
(Contributed by Jim Kingdon, 1-Mar-2022.)
|
⊢ {𝐴} ≼ 1o |
|
Theorem | enm 6777* |
A set equinumerous to an inhabited set is inhabited. (Contributed by
Jim Kingdon, 19-May-2020.)
|
⊢ ((𝐴 ≈ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ 𝐵) |
|
Theorem | xpsnen 6778 |
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 6779 |
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 6780 |
One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised
by Mario Carneiro, 29-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 1o) ≈ 𝐴) |
|
Theorem | endisj 6781* |
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 6782* |
The canonical bijection from (𝐴 × 𝐵) to (𝐵 × 𝐴).
(Contributed by Mario Carneiro, 23-Apr-2014.)
|
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪
◡{𝑥}) ⇒ ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) |
|
Theorem | xpcomco 6783* |
Composition with the bijection of xpcomf1o 6782 swaps the arguments to a
mapping. (Contributed by Mario Carneiro, 30-May-2015.)
|
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪
◡{𝑥})
& ⊢ 𝐺 = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝐺 ∘ 𝐹) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
|
Theorem | xpcomen 6784 |
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 6785 |
Commutative law for equinumerosity of Cartesian product. Proposition
4.22(d) of [Mendelson] p. 254.
(Contributed by NM, 27-Mar-2006.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)) |
|
Theorem | xpsnen2g 6786 |
A set is equinumerous to its Cartesian product with a singleton on the
left. (Contributed by Stefan O'Rear, 21-Nov-2014.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × 𝐵) ≈ 𝐵) |
|
Theorem | xpassen 6787 |
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 6788 |
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 6789 |
Dominance law for Cartesian product. Theorem 6L(c) of [Enderton]
p. 149. (Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵)) |
|
Theorem | xpdom1g 6790 |
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 6791* |
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 6792 |
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 6793 |
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 6794 |
Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴) |
|
Theorem | dom0 6795 |
A set dominated by the empty set is empty. (Contributed by NM,
22-Nov-2004.)
|
⊢ (𝐴 ≼ ∅ ↔ 𝐴 = ∅) |
|
Theorem | 0dom 6796 |
Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ∅ ≼ 𝐴 |
|
Theorem | enen1 6797 |
Equality-like theorem for equinumerosity. (Contributed by NM,
18-Dec-2003.)
|
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≈ 𝐶 ↔ 𝐵 ≈ 𝐶)) |
|
Theorem | enen2 6798 |
Equality-like theorem for equinumerosity. (Contributed by NM,
18-Dec-2003.)
|
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≈ 𝐴 ↔ 𝐶 ≈ 𝐵)) |
|
Theorem | domen1 6799 |
Equality-like theorem for equinumerosity and dominance. (Contributed by
NM, 8-Nov-2003.)
|
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≼ 𝐶 ↔ 𝐵 ≼ 𝐶)) |
|
Theorem | domen2 6800 |
Equality-like theorem for equinumerosity and dominance. (Contributed by
NM, 8-Nov-2003.)
|
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≼ 𝐴 ↔ 𝐶 ≼ 𝐵)) |