Theorem List for Intuitionistic Logic Explorer - 6701-6800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fpmg 6701 |
A total function is a partial function. (Contributed by Mario Carneiro,
31-Dec-2013.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴⟶𝐵) → 𝐹 ∈ (𝐵 ↑pm 𝐴)) |
|
Theorem | pmss12g 6702 |
Subset relation for the set of partial functions. (Contributed by Mario
Carneiro, 31-Dec-2013.)
|
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊)) → (𝐴 ↑pm 𝐵) ⊆ (𝐶 ↑pm 𝐷)) |
|
Theorem | pmresg 6703 |
Elementhood of a restricted function in the set of partial functions.
(Contributed by Mario Carneiro, 31-Dec-2013.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) |
|
Theorem | elmap 6704 |
Membership relation for set exponentiation. (Contributed by NM,
8-Dec-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐹 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐹:𝐵⟶𝐴) |
|
Theorem | mapval2 6705* |
Alternate expression for the value of set exponentiation. (Contributed
by NM, 3-Nov-2007.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴 ↑𝑚 𝐵) = (𝒫 (𝐵 × 𝐴) ∩ {𝑓 ∣ 𝑓 Fn 𝐵}) |
|
Theorem | elpm 6706 |
The predicate "is a partial function". (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (Fun 𝐹 ∧ 𝐹 ⊆ (𝐵 × 𝐴))) |
|
Theorem | elpm2 6707 |
The predicate "is a partial function". (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵)) |
|
Theorem | fpm 6708 |
A total function is a partial function. (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ∈ (𝐵 ↑pm 𝐴)) |
|
Theorem | mapsspm 6709 |
Set exponentiation is a subset of partial maps. (Contributed by NM,
15-Nov-2007.) (Revised by Mario Carneiro, 27-Feb-2016.)
|
⊢ (𝐴 ↑𝑚 𝐵) ⊆ (𝐴 ↑pm 𝐵) |
|
Theorem | pmsspw 6710 |
Partial maps are a subset of the power set of the Cartesian product of
its arguments. (Contributed by Mario Carneiro, 2-Jan-2017.)
|
⊢ (𝐴 ↑pm 𝐵) ⊆ 𝒫 (𝐵 × 𝐴) |
|
Theorem | mapsspw 6711 |
Set exponentiation is a subset of the power set of the Cartesian product
of its arguments. (Contributed by NM, 8-Dec-2006.) (Revised by Mario
Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ↑𝑚 𝐵) ⊆ 𝒫 (𝐵 × 𝐴) |
|
Theorem | fvmptmap 6712* |
Special case of fvmpt 5614 for operator theorems. (Contributed by NM,
27-Nov-2007.)
|
⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝑅 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
& ⊢ 𝐹 = (𝑥 ∈ (𝑅 ↑𝑚 𝐷) ↦ 𝐵) ⇒ ⊢ (𝐴:𝐷⟶𝑅 → (𝐹‘𝐴) = 𝐶) |
|
Theorem | map0e 6713 |
Set exponentiation with an empty exponent (ordinal number 0) is ordinal
number 1. Exercise 4.42(a) of [Mendelson] p. 255. (Contributed by NM,
10-Dec-2003.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑𝑚 ∅) =
1o) |
|
Theorem | map0b 6714 |
Set exponentiation with an empty base is the empty set, provided the
exponent is nonempty. Theorem 96 of [Suppes] p. 89. (Contributed by
NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ≠ ∅ → (∅
↑𝑚 𝐴) = ∅) |
|
Theorem | map0g 6715 |
Set exponentiation is empty iff the base is empty and the exponent is
not empty. Theorem 97 of [Suppes] p. 89.
(Contributed by Mario
Carneiro, 30-Apr-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ↑𝑚 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 ≠
∅))) |
|
Theorem | map0 6716 |
Set exponentiation is empty iff the base is empty and the exponent is
not empty. Theorem 97 of [Suppes] p. 89.
(Contributed by NM,
10-Dec-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ((𝐴 ↑𝑚 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 ≠
∅)) |
|
Theorem | mapsn 6717* |
The value of set exponentiation with a singleton exponent. Theorem 98
of [Suppes] p. 89. (Contributed by NM,
10-Dec-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴 ↑𝑚 {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}} |
|
Theorem | mapss 6718 |
Subset inheritance for set exponentiation. Theorem 99 of [Suppes]
p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶)) |
|
Theorem | fdiagfn 6719* |
Functionality of the diagonal map. (Contributed by Stefan O'Rear,
24-Jan-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑𝑚 𝐼)) |
|
Theorem | fvdiagfn 6720* |
Functionality of the diagonal map. (Contributed by Stefan O'Rear,
24-Jan-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (𝐼 × {𝑋})) |
|
Theorem | mapsnconst 6721 |
Every singleton map is a constant function. (Contributed by Stefan
O'Rear, 25-Mar-2015.)
|
⊢ 𝑆 = {𝑋}
& ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈
V ⇒ ⊢ (𝐹 ∈ (𝐵 ↑𝑚 𝑆) → 𝐹 = (𝑆 × {(𝐹‘𝑋)})) |
|
Theorem | mapsncnv 6722* |
Expression for the inverse of the canonical map between a set and its
set of singleton functions. (Contributed by Stefan O'Rear,
21-Mar-2015.)
|
⊢ 𝑆 = {𝑋}
& ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↦ (𝑥‘𝑋)) ⇒ ⊢ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦})) |
|
Theorem | mapsnf1o2 6723* |
Explicit bijection between a set and its singleton functions.
(Contributed by Stefan O'Rear, 21-Mar-2015.)
|
⊢ 𝑆 = {𝑋}
& ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↦ (𝑥‘𝑋)) ⇒ ⊢ 𝐹:(𝐵 ↑𝑚 𝑆)–1-1-onto→𝐵 |
|
Theorem | mapsnf1o3 6724* |
Explicit bijection in the reverse of mapsnf1o2 6723. (Contributed by
Stefan O'Rear, 24-Mar-2015.)
|
⊢ 𝑆 = {𝑋}
& ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦})) ⇒ ⊢ 𝐹:𝐵–1-1-onto→(𝐵 ↑𝑚 𝑆) |
|
2.6.27 Infinite Cartesian products
|
|
Syntax | cixp 6725 |
Extend class notation to include infinite Cartesian products.
|
class X𝑥 ∈ 𝐴 𝐵 |
|
Definition | df-ixp 6726* |
Definition of infinite Cartesian product of [Enderton] p. 54. Enderton
uses a bold "X" with 𝑥 ∈ 𝐴 written underneath or as a
subscript, as
does Stoll p. 47. Some books use a capital pi, but we will reserve that
notation for products of numbers. Usually 𝐵 represents a class
expression containing 𝑥 free and thus can be thought of as
𝐵(𝑥). Normally, 𝑥 is not free in 𝐴,
although this is
not a requirement of the definition. (Contributed by NM,
28-Sep-2006.)
|
⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} |
|
Theorem | dfixp 6727* |
Eliminate the expression {𝑥 ∣ 𝑥 ∈ 𝐴} in df-ixp 6726, under the
assumption that 𝐴 and 𝑥 are disjoint. This way,
we can say that
𝑥 is bound in X𝑥 ∈
𝐴𝐵 even if it appears free in 𝐴.
(Contributed by Mario Carneiro, 12-Aug-2016.)
|
⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} |
|
Theorem | ixpsnval 6728* |
The value of an infinite Cartesian product with a singleton.
(Contributed by AV, 3-Dec-2018.)
|
⊢ (𝑋 ∈ 𝑉 → X𝑥 ∈ {𝑋}𝐵 = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌𝐵)}) |
|
Theorem | elixp2 6729* |
Membership in an infinite Cartesian product. See df-ixp 6726 for
discussion of the notation. (Contributed by NM, 28-Sep-2006.)
|
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
|
Theorem | fvixp 6730* |
Projection of a factor of an indexed Cartesian product. (Contributed by
Mario Carneiro, 11-Jun-2016.)
|
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐷) |
|
Theorem | ixpfn 6731* |
A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by
Mario Carneiro, 31-May-2014.)
|
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹 Fn 𝐴) |
|
Theorem | elixp 6732* |
Membership in an infinite Cartesian product. (Contributed by NM,
28-Sep-2006.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
|
Theorem | elixpconst 6733* |
Membership in an infinite Cartesian product of a constant 𝐵.
(Contributed by NM, 12-Apr-2008.)
|
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
|
Theorem | ixpconstg 6734* |
Infinite Cartesian product of a constant 𝐵. (Contributed by Mario
Carneiro, 11-Jan-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑𝑚 𝐴)) |
|
Theorem | ixpconst 6735* |
Infinite Cartesian product of a constant 𝐵. (Contributed by NM,
28-Sep-2006.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑𝑚 𝐴) |
|
Theorem | ixpeq1 6736* |
Equality theorem for infinite Cartesian product. (Contributed by NM,
29-Sep-2006.)
|
⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶) |
|
Theorem | ixpeq1d 6737* |
Equality theorem for infinite Cartesian product. (Contributed by Mario
Carneiro, 11-Jun-2016.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶) |
|
Theorem | ss2ixp 6738 |
Subclass theorem for infinite Cartesian product. (Contributed by NM,
29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶) |
|
Theorem | ixpeq2 6739 |
Equality theorem for infinite Cartesian product. (Contributed by NM,
29-Sep-2006.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
|
Theorem | ixpeq2dva 6740* |
Equality theorem for infinite Cartesian product. (Contributed by Mario
Carneiro, 11-Jun-2016.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
|
Theorem | ixpeq2dv 6741* |
Equality theorem for infinite Cartesian product. (Contributed by Mario
Carneiro, 11-Jun-2016.)
|
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) |
|
Theorem | cbvixp 6742* |
Change bound variable in an indexed Cartesian product. (Contributed by
Jeff Madsen, 20-Jun-2011.)
|
⊢ Ⅎ𝑦𝐵
& ⊢ Ⅎ𝑥𝐶
& ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶 |
|
Theorem | cbvixpv 6743* |
Change bound variable in an indexed Cartesian product. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶 |
|
Theorem | nfixpxy 6744* |
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 6745 |
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 6746* |
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 6747* |
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 6748* |
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 6749* |
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 6750* |
The intersection of two infinite Cartesian products. (Contributed by
Mario Carneiro, 3-Feb-2015.)
|
⊢ X𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (X𝑥 ∈ 𝐴 𝐵 ∩ X𝑥 ∈ 𝐴 𝐶) |
|
Theorem | ixpiinm 6751* |
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 6752* |
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 6753 |
An infinite Cartesian product with an empty index set. (Contributed by
NM, 21-Sep-2007.)
|
⊢ X𝑥 ∈ ∅ 𝐴 = {∅} |
|
Theorem | ixpssmap2g 6754* |
An infinite Cartesian product is a subset of set exponentiation. This
version of ixpssmapg 6755 avoids ax-coll 4133. (Contributed by Mario
Carneiro, 16-Nov-2014.)
|
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴)) |
|
Theorem | ixpssmapg 6755* |
An infinite Cartesian product is a subset of set exponentiation.
(Contributed by Jeff Madsen, 19-Jun-2011.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴)) |
|
Theorem | 0elixp 6756 |
Membership of the empty set in an infinite Cartesian product.
(Contributed by Steve Rodriguez, 29-Sep-2006.)
|
⊢ ∅ ∈ X𝑥 ∈ ∅ 𝐴 |
|
Theorem | ixpm 6757* |
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 6758 |
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 6759* |
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 6760* |
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 6761* |
Condition for an explicit member of an indexed product. (Contributed by
Stefan O'Rear, 4-Jan-2015.)
|
⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾)) |
|
Theorem | elixpsn 6762* |
Membership in a class of singleton functions. (Contributed by Stefan
O'Rear, 24-Jan-2015.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ {𝐴}𝐵 ↔ ∃𝑦 ∈ 𝐵 𝐹 = {〈𝐴, 𝑦〉})) |
|
Theorem | ixpsnf1o 6763* |
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 6764* |
A bijection between a set and single-point functions to it.
(Contributed by Stefan O'Rear, 24-Jan-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ({𝐼} × {𝑥})) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐴–1-1-onto→(𝐴 ↑𝑚 {𝐼})) |
|
2.6.28 Equinumerosity
|
|
Syntax | cen 6765 |
Extend class definition to include the equinumerosity relation
("approximately equals" symbol)
|
class ≈ |
|
Syntax | cdom 6766 |
Extend class definition to include the dominance relation (curly
less-than-or-equal)
|
class ≼ |
|
Syntax | cfn 6767 |
Extend class definition to include the class of all finite sets.
|
class Fin |
|
Definition | df-en 6768* |
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 6774. (Contributed by NM, 28-Mar-1998.)
|
⊢ ≈ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦} |
|
Definition | df-dom 6769* |
Define the dominance relation. Compare Definition of [Enderton] p. 145.
Typical textbook definitions are derived as brdom 6777 and domen 6778.
(Contributed by NM, 28-Mar-1998.)
|
⊢ ≼ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} |
|
Definition | df-fin 6770* |
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 15206. (Contributed by NM,
22-Aug-2008.)
|
⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦} |
|
Theorem | relen 6771 |
Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
|
⊢ Rel ≈ |
|
Theorem | reldom 6772 |
Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
|
⊢ Rel ≼ |
|
Theorem | encv 6773 |
If two classes are equinumerous, both classes are sets. (Contributed by
AV, 21-Mar-2019.)
|
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
|
Theorem | bren 6774* |
Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
|
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) |
|
Theorem | brdomg 6775* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) |
|
Theorem | brdomi 6776* |
Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
|
Theorem | brdom 6777* |
Dominance relation. (Contributed by NM, 15-Jun-1998.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵) |
|
Theorem | domen 6778* |
Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146.
(Contributed by NM, 15-Jun-1998.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) |
|
Theorem | domeng 6779* |
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 6780 |
A class dominated by ω is a set. See also ctfoex 7148 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 6781 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6784 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 6782 |
The domain and range of a one-to-one, onto function are equinumerous.
This variation of f1oeng 6784 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 10-Sep-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
|
Theorem | f1dom2g 6783 |
The domain of a one-to-one function is dominated by its codomain. This
variation of f1domg 6785 does not require the Axiom of Replacement.
(Contributed by Mario Carneiro, 24-Jun-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) |
|
Theorem | f1oeng 6784 |
The domain and range of a one-to-one, onto function are equinumerous.
(Contributed by NM, 19-Jun-1998.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
|
Theorem | f1domg 6785 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 4-Sep-2004.)
|
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵)) |
|
Theorem | f1oen 6786 |
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 6787 |
The domain of a one-to-one function is dominated by its codomain.
(Contributed by NM, 19-Jun-1998.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵) |
|
Theorem | isfi 6788* |
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 6789 |
Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
|
⊢ ≈ ⊆ ≼ |
|
Theorem | endom 6790 |
Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94.
(Contributed by NM, 28-May-1998.)
|
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵) |
|
Theorem | enrefg 6791 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴) |
|
Theorem | enref 6792 |
Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ≈ 𝐴 |
|
Theorem | eqeng 6793 |
Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) |
|
Theorem | domrefg 6794 |
Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
|
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≼ 𝐴) |
|
Theorem | en2d 6795* |
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 6796* |
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 6797* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 4-Jan-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ V) & ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ V) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷)) ⇒ ⊢ 𝐴 ≈ 𝐵 |
|
Theorem | en3i 6798* |
Equinumerosity inference from an implicit one-to-one onto function.
(Contributed by NM, 19-Jul-2004.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)
& ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴)
& ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ 𝐴 ≈ 𝐵 |
|
Theorem | dom2lem 6799* |
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 6800* |
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.)
|
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦))) ⇒ ⊢ (𝜑 → (𝐵 ∈ 𝑅 → 𝐴 ≼ 𝐵)) |