Theorem List for Intuitionistic Logic Explorer - 6601-6700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ixpeq2dv 6601* |
Equality theorem for infinite Cartesian product. (Contributed by Mario
Carneiro, 11-Jun-2016.)
|
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
|
Theorem | cbvixp 6602* |
Change bound variable in an indexed Cartesian product. (Contributed by
Jeff Madsen, 20-Jun-2011.)
|
⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝐶
& ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶 |
|
Theorem | cbvixpv 6603* |
Change bound variable in an indexed Cartesian product. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶 |
|
Theorem | nfixpxy 6604* |
Bound-variable hypothesis builder for indexed Cartesian product.
(Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by Jim Kingdon,
15-Feb-2023.)
|
⊢ Ⅎ𝑦𝐴
& ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦X𝑥 ∈ 𝐴 𝐵 |
|
Theorem | nfixp1 6605 |
The index variable in an indexed Cartesian product is not free.
(Contributed by Jeff Madsen, 19-Jun-2011.) (Revised by Mario Carneiro,
15-Oct-2016.)
|
⊢ Ⅎ𝑥X𝑥 ∈ 𝐴 𝐵 |
|
Theorem | ixpprc 6606* |
A cartesian product of proper-class many sets is empty, because any
function in the cartesian product has to be a set with domain 𝐴,
which is not possible for a proper class domain. (Contributed by Mario
Carneiro, 25-Jan-2015.)
|
⊢ (¬ 𝐴 ∈ V → X𝑥 ∈
𝐴 𝐵 = ∅) |
|
Theorem | ixpf 6607* |
A member of an infinite Cartesian product maps to the indexed union of
the product argument. Remark in [Enderton] p. 54. (Contributed by NM,
28-Sep-2006.)
|
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹:𝐴⟶∪
𝑥 ∈ 𝐴 𝐵) |
|
Theorem | uniixp 6608* |
The union of an infinite Cartesian product is included in a Cartesian
product. (Contributed by NM, 28-Sep-2006.) (Revised by Mario Carneiro,
24-Jun-2015.)
|
⊢ ∪ X𝑥 ∈
𝐴 𝐵 ⊆ (𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵) |
|
Theorem | ixpexgg 6609* |
The existence of an infinite Cartesian product. 𝑥 is normally a
free-variable parameter in 𝐵. Remark in Enderton p. 54.
(Contributed by NM, 28-Sep-2006.) (Revised by Jim Kingdon,
15-Feb-2023.)
|
⊢ ((𝐴 ∈ 𝑊 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → X𝑥 ∈ 𝐴 𝐵 ∈ V) |
|
Theorem | ixpin 6610* |
The intersection of two infinite Cartesian products. (Contributed by
Mario Carneiro, 3-Feb-2015.)
|
⊢ X𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (X𝑥 ∈ 𝐴 𝐵 ∩ X𝑥 ∈ 𝐴 𝐶) |
|
Theorem | ixpiinm 6611* |
The indexed intersection of a collection of infinite Cartesian products.
(Contributed by Mario Carneiro, 6-Feb-2015.) (Revised by Jim Kingdon,
15-Feb-2023.)
|
⊢ (∃𝑧 𝑧 ∈ 𝐵 → X𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 = ∩
𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝐶) |
|
Theorem | ixpintm 6612* |
The intersection of a collection of infinite Cartesian products.
(Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Jim Kingdon,
15-Feb-2023.)
|
⊢ (∃𝑧 𝑧 ∈ 𝐵 → X𝑥 ∈ 𝐴 ∩ 𝐵 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝑦) |
|
Theorem | ixp0x 6613 |
An infinite Cartesian product with an empty index set. (Contributed by
NM, 21-Sep-2007.)
|
⊢ X𝑥 ∈ ∅ 𝐴 = {∅} |
|
Theorem | ixpssmap2g 6614* |
An infinite Cartesian product is a subset of set exponentiation. This
version of ixpssmapg 6615 avoids ax-coll 4038. (Contributed by Mario
Carneiro, 16-Nov-2014.)
|
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴)) |
|
Theorem | ixpssmapg 6615* |
An infinite Cartesian product is a subset of set exponentiation.
(Contributed by Jeff Madsen, 19-Jun-2011.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴)) |
|
Theorem | 0elixp 6616 |
Membership of the empty set in an infinite Cartesian product.
(Contributed by Steve Rodriguez, 29-Sep-2006.)
|
⊢ ∅ ∈ X𝑥 ∈ ∅ 𝐴 |
|
Theorem | ixpm 6617* |
If an infinite Cartesian product of a family 𝐵(𝑥) is inhabited,
every 𝐵(𝑥) is inhabited. (Contributed by Mario
Carneiro,
22-Jun-2016.) (Revised by Jim Kingdon, 16-Feb-2023.)
|
⊢ (∃𝑓 𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 → ∀𝑥 ∈ 𝐴 ∃𝑧 𝑧 ∈ 𝐵) |
|
Theorem | ixp0 6618 |
The infinite Cartesian product of a family 𝐵(𝑥) with an empty
member is empty. (Contributed by NM, 1-Oct-2006.) (Revised by Jim
Kingdon, 16-Feb-2023.)
|
⊢ (∃𝑥 ∈ 𝐴 𝐵 = ∅ → X𝑥 ∈
𝐴 𝐵 = ∅) |
|
Theorem | ixpssmap 6619* |
An infinite Cartesian product is a subset of set exponentiation. Remark
in [Enderton] p. 54. (Contributed by
NM, 28-Sep-2006.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴) |
|
Theorem | resixp 6620* |
Restriction of an element of an infinite Cartesian product.
(Contributed by FL, 7-Nov-2011.) (Proof shortened by Mario Carneiro,
31-May-2014.)
|
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X𝑥 ∈ 𝐴 𝐶) → (𝐹 ↾ 𝐵) ∈ X𝑥 ∈ 𝐵 𝐶) |
|
Theorem | mptelixpg 6621* |
Condition for an explicit member of an indexed product. (Contributed by
Stefan O'Rear, 4-Jan-2015.)
|
⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾)) |
|
Theorem | elixpsn 6622* |
Membership in a class of singleton functions. (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ {𝐴}𝐵 ↔ ∃𝑦 ∈ 𝐵 𝐹 = {〈𝐴, 𝑦〉})) |
|
Theorem | ixpsnf1o 6623* |
A bijection between a class and single-point functions to it.
(Contributed by Stefan O'Rear, 24-Jan-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ({𝐼} × {𝑥})) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐹:𝐴–1-1-onto→X𝑦 ∈ {𝐼}𝐴) |
|
Theorem | mapsnf1o 6624* |
A bijection between a set and single-point functions to it.
(Contributed by Stefan O'Rear, 24-Jan-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ({𝐼} × {𝑥})) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐴–1-1-onto→(𝐴 ↑𝑚 {𝐼})) |
|
2.6.27 Equinumerosity
|
|
Syntax | cen 6625 |
Extend class definition to include the equinumerosity relation
("approximately equals" symbol)
|
class ≈ |
|
Syntax | cdom 6626 |
Extend class definition to include the dominance relation (curly
less-than-or-equal)
|
class ≼ |
|
Syntax | cfn 6627 |
Extend class definition to include the class of all finite sets.
|
class Fin |
|
Definition | df-en 6628* |
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 6634. (Contributed by NM, 28-Mar-1998.)
|
⊢ ≈ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦} |
|
Definition | df-dom 6629* |
Define the dominance relation. Compare Definition of [Enderton] p. 145.
Typical textbook definitions are derived as brdom 6637 and domen 6638.
(Contributed by NM, 28-Mar-1998.)
|
⊢ ≼ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} |
|
Definition | df-fin 6630* |
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 13163. (Contributed by NM,
22-Aug-2008.)
|
⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦} |
|
Theorem | relen 6631 |
Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
|
⊢ Rel ≈ |
|
Theorem | reldom 6632 |
Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
|
⊢ Rel ≼ |
|
Theorem | encv 6633 |
If two classes are equinumerous, both classes are sets. (Contributed by
AV, 21-Mar-2019.)
|
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
|
Theorem | bren 6634* |
Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
|
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
|
Theorem | brdomg 6635* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) |
|
Theorem | brdomi 6636* |
Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
|
Theorem | brdom 6637* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵) |
|
Theorem | domen 6638* |
Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146.
(Contributed by NM, 15-Jun-1998.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) |
|
Theorem | domeng 6639* |
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 6640 |
A class dominated by ω is a set. See also ctfoex 6996 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 6641 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6644 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 6642 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6644 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 10-Sep-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
|
Theorem | f1dom2g 6643 |
The domain of a one-to-one function is dominated by its codomain. This
variation of f1domg 6645 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 24-Jun-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) |
|
Theorem | f1oeng 6644 |
The domain and range of a one-to-one, onto function are equinumerous.
(Contributed by NM, 19-Jun-1998.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
|
Theorem | f1domg 6645 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 4-Sep-2004.)
|
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵)) |
|
Theorem | f1oen 6646 |
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 6647 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 19-Jun-1998.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵) |
|
Theorem | isfi 6648* |
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 6649 |
Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
|
⊢ ≈ ⊆ ≼ |
|
Theorem | endom 6650 |
Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94.
(Contributed by NM, 28-May-1998.)
|
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵) |
|
Theorem | enrefg 6651 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴) |
|
Theorem | enref 6652 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ≈ 𝐴 |
|
Theorem | eqeng 6653 |
Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) |
|
Theorem | domrefg 6654 |
Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
|
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≼ 𝐴) |
|
Theorem | en2d 6655* |
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 6656* |
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 6657* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 4-Jan-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ V) & ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ V) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷)) ⇒ ⊢ 𝐴 ≈ 𝐵 |
|
Theorem | en3i 6658* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 19-Jul-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)
& ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴)
& ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ 𝐴 ≈ 𝐵 |
|
Theorem | dom2lem 6659* |
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 6660* |
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 6661* |
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 6662* |
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 6663* |
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 6664 |
Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ I ⊆ ≈ |
|
Theorem | ssdomg 6665 |
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 6666 |
Equinumerosity is an equivalence relation. (Contributed by NM,
19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ≈ Er V |
|
Theorem | ensymb 6667 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴) |
|
Theorem | ensym 6668 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
|
Theorem | ensymi 6669 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵 ⇒ ⊢ 𝐵 ≈ 𝐴 |
|
Theorem | ensymd 6670 |
Symmetry of equinumerosity. Deduction form of ensym 6668. (Contributed
by David Moews, 1-May-2017.)
|
⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≈ 𝐴) |
|
Theorem | entr 6671 |
Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
(Contributed by NM, 9-Jun-1998.)
|
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) |
|
Theorem | domtr 6672 |
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 6673 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐵 ≈ 𝐶 ⇒ ⊢ 𝐴 ≈ 𝐶 |
|
Theorem | entr2i 6674 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐵 ≈ 𝐶 ⇒ ⊢ 𝐶 ≈ 𝐴 |
|
Theorem | entr3i 6675 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐴 ≈ 𝐶 ⇒ ⊢ 𝐵 ≈ 𝐶 |
|
Theorem | entr4i 6676 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐶 ≈ 𝐵 ⇒ ⊢ 𝐴 ≈ 𝐶 |
|
Theorem | endomtr 6677 |
Transitivity of equinumerosity and dominance. (Contributed by NM,
7-Jun-1998.)
|
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) |
|
Theorem | domentr 6678 |
Transitivity of dominance and equinumerosity. (Contributed by NM,
7-Jun-1998.)
|
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶) |
|
Theorem | f1imaeng 6679 |
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 6680 |
A one-to-one function's image under a subset of its domain is equinumerous
to the subset. (This version of f1imaen 6681 does not need ax-setind 4447.)
(Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro,
25-Jun-2015.)
|
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉)) → (𝐹 “ 𝐶) ≈ 𝐶) |
|
Theorem | f1imaen 6681 |
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 6682 |
The empty set is equinumerous only to itself. Exercise 1 of
[TakeutiZaring] p. 88.
(Contributed by NM, 27-May-1998.)
|
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) |
|
Theorem | ensn1 6683 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
4-Nov-2002.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ≈ 1o |
|
Theorem | ensn1g 6684 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
23-Apr-2004.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ 1o) |
|
Theorem | enpr1g 6685 |
{𝐴, 𝐴} has only one element.
(Contributed by FL, 15-Feb-2010.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐴} ≈ 1o) |
|
Theorem | en1 6686* |
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by NM, 25-Jul-2004.)
|
⊢ (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥}) |
|
Theorem | en1bg 6687 |
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by Jim Kingdon, 13-Apr-2020.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ≈ 1o ↔ 𝐴 = {∪ 𝐴})) |
|
Theorem | reuen1 6688* |
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28-Oct-2014.)
|
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} ≈ 1o) |
|
Theorem | euen1 6689 |
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28-Oct-2014.)
|
⊢ (∃!𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≈ 1o) |
|
Theorem | euen1b 6690* |
Two ways to express "𝐴 has a unique element".
(Contributed by
Mario Carneiro, 9-Apr-2015.)
|
⊢ (𝐴 ≈ 1o ↔ ∃!𝑥 𝑥 ∈ 𝐴) |
|
Theorem | en1uniel 6691 |
A singleton contains its sole element. (Contributed by Stefan O'Rear,
16-Aug-2015.)
|
⊢ (𝑆 ≈ 1o → ∪ 𝑆
∈ 𝑆) |
|
Theorem | 2dom 6692* |
A set that dominates ordinal 2 has at least 2 different members.
(Contributed by NM, 25-Jul-2004.)
|
⊢ (2o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦) |
|
Theorem | fundmen 6693 |
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 6694 |
A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98.
(Contributed by NM, 17-Sep-2013.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → dom 𝐹 ≈ 𝐹) |
|
Theorem | cnven 6695 |
A relational set is equinumerous to its converse. (Contributed by Mario
Carneiro, 28-Dec-2014.)
|
⊢ ((Rel 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ ◡𝐴) |
|
Theorem | cnvct 6696 |
If a set is dominated by ω, so is its converse.
(Contributed by
Thierry Arnoux, 29-Dec-2016.)
|
⊢ (𝐴 ≼ ω → ◡𝐴 ≼ ω) |
|
Theorem | fndmeng 6697 |
A function is equinumerate to its domain. (Contributed by Paul Chapman,
22-Jun-2011.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐴 ≈ 𝐹) |
|
Theorem | mapsnen 6698 |
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 6699 |
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 6700 |
Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵}) |