Theorem List for Intuitionistic Logic Explorer - 6801-6900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | dom3d 6801* |
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 6802* |
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 6803* |
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 6804 |
Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ I ⊆ ≈ |
|
Theorem | ssdomg 6805 |
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 6806 |
Equinumerosity is an equivalence relation. (Contributed by NM,
19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ≈ Er V |
|
Theorem | ensymb 6807 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴) |
|
Theorem | ensym 6808 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by
NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
|
Theorem | ensymi 6809 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed
by NM, 25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵 ⇒ ⊢ 𝐵 ≈ 𝐴 |
|
Theorem | ensymd 6810 |
Symmetry of equinumerosity. Deduction form of ensym 6808. (Contributed
by David Moews, 1-May-2017.)
|
⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≈ 𝐴) |
|
Theorem | entr 6811 |
Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
(Contributed by NM, 9-Jun-1998.)
|
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) |
|
Theorem | domtr 6812 |
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 6813 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐵 ≈ 𝐶 ⇒ ⊢ 𝐴 ≈ 𝐶 |
|
Theorem | entr2i 6814 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐵 ≈ 𝐶 ⇒ ⊢ 𝐶 ≈ 𝐴 |
|
Theorem | entr3i 6815 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐴 ≈ 𝐶 ⇒ ⊢ 𝐵 ≈ 𝐶 |
|
Theorem | entr4i 6816 |
A chained equinumerosity inference. (Contributed by NM,
25-Sep-2004.)
|
⊢ 𝐴 ≈ 𝐵
& ⊢ 𝐶 ≈ 𝐵 ⇒ ⊢ 𝐴 ≈ 𝐶 |
|
Theorem | endomtr 6817 |
Transitivity of equinumerosity and dominance. (Contributed by NM,
7-Jun-1998.)
|
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) |
|
Theorem | domentr 6818 |
Transitivity of dominance and equinumerosity. (Contributed by NM,
7-Jun-1998.)
|
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶) |
|
Theorem | f1imaeng 6819 |
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 6820 |
A one-to-one function's image under a subset of its domain is equinumerous
to the subset. (This version of f1imaen 6821 does not need ax-setind 4554.)
(Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro,
25-Jun-2015.)
|
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉)) → (𝐹 “ 𝐶) ≈ 𝐶) |
|
Theorem | f1imaen 6821 |
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 6822 |
The empty set is equinumerous only to itself. Exercise 1 of
[TakeutiZaring] p. 88.
(Contributed by NM, 27-May-1998.)
|
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) |
|
Theorem | ensn1 6823 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
4-Nov-2002.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ≈ 1o |
|
Theorem | ensn1g 6824 |
A singleton is equinumerous to ordinal one. (Contributed by NM,
23-Apr-2004.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ 1o) |
|
Theorem | enpr1g 6825 |
{𝐴, 𝐴} has only one element.
(Contributed by FL, 15-Feb-2010.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐴} ≈ 1o) |
|
Theorem | en1 6826* |
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by NM, 25-Jul-2004.)
|
⊢ (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥}) |
|
Theorem | en1bg 6827 |
A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by Jim Kingdon, 13-Apr-2020.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ≈ 1o ↔ 𝐴 = {∪ 𝐴})) |
|
Theorem | reuen1 6828* |
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28-Oct-2014.)
|
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} ≈ 1o) |
|
Theorem | euen1 6829 |
Two ways to express "exactly one". (Contributed by Stefan O'Rear,
28-Oct-2014.)
|
⊢ (∃!𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≈ 1o) |
|
Theorem | euen1b 6830* |
Two ways to express "𝐴 has a unique element".
(Contributed by
Mario Carneiro, 9-Apr-2015.)
|
⊢ (𝐴 ≈ 1o ↔ ∃!𝑥 𝑥 ∈ 𝐴) |
|
Theorem | en1uniel 6831 |
A singleton contains its sole element. (Contributed by Stefan O'Rear,
16-Aug-2015.)
|
⊢ (𝑆 ≈ 1o → ∪ 𝑆
∈ 𝑆) |
|
Theorem | 2dom 6832* |
A set that dominates ordinal 2 has at least 2 different members.
(Contributed by NM, 25-Jul-2004.)
|
⊢ (2o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦) |
|
Theorem | fundmen 6833 |
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 6834 |
A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98.
(Contributed by NM, 17-Sep-2013.)
|
⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → dom 𝐹 ≈ 𝐹) |
|
Theorem | cnven 6835 |
A relational set is equinumerous to its converse. (Contributed by Mario
Carneiro, 28-Dec-2014.)
|
⊢ ((Rel 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ ◡𝐴) |
|
Theorem | cnvct 6836 |
If a set is dominated by ω, so is its converse.
(Contributed by
Thierry Arnoux, 29-Dec-2016.)
|
⊢ (𝐴 ≼ ω → ◡𝐴 ≼ ω) |
|
Theorem | fndmeng 6837 |
A function is equinumerate to its domain. (Contributed by Paul Chapman,
22-Jun-2011.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐴 ≈ 𝐹) |
|
Theorem | mapsnen 6838 |
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 6839 |
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 6840 |
Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵}) |
|
Theorem | snfig 6841 |
A singleton is finite. For the proper class case, see snprc 3672.
(Contributed by Jim Kingdon, 13-Apr-2020.)
|
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Fin) |
|
Theorem | fiprc 6842 |
The class of finite sets is a proper class. (Contributed by Jeff
Hankins, 3-Oct-2008.)
|
⊢ Fin ∉ V |
|
Theorem | unen 6843 |
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 6844 |
A pair with distinct elements is equinumerous to ordinal two.
(Contributed by Rohan Ridenour, 3-Aug-2023.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐶)
& ⊢ (𝜑 → 𝐵 ∈ 𝐷)
& ⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o) |
|
Theorem | ssct 6845 |
A subset of a set dominated by ω is dominated by
ω.
(Contributed by Thierry Arnoux, 31-Jan-2017.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω) → 𝐴 ≼ ω) |
|
Theorem | 1domsn 6846 |
A singleton (whether of a set or a proper class) is dominated by one.
(Contributed by Jim Kingdon, 1-Mar-2022.)
|
⊢ {𝐴} ≼ 1o |
|
Theorem | enm 6847* |
A set equinumerous to an inhabited set is inhabited. (Contributed by
Jim Kingdon, 19-May-2020.)
|
⊢ ((𝐴 ≈ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ 𝐵) |
|
Theorem | xpsnen 6848 |
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 6849 |
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 6850 |
One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised
by Mario Carneiro, 29-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 1o) ≈ 𝐴) |
|
Theorem | endisj 6851* |
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 6852* |
The canonical bijection from (𝐴 × 𝐵) to (𝐵 × 𝐴).
(Contributed by Mario Carneiro, 23-Apr-2014.)
|
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪
◡{𝑥}) ⇒ ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) |
|
Theorem | xpcomco 6853* |
Composition with the bijection of xpcomf1o 6852 swaps the arguments to a
mapping. (Contributed by Mario Carneiro, 30-May-2015.)
|
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪
◡{𝑥})
& ⊢ 𝐺 = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝐺 ∘ 𝐹) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
|
Theorem | xpcomen 6854 |
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 6855 |
Commutative law for equinumerosity of Cartesian product. Proposition
4.22(d) of [Mendelson] p. 254.
(Contributed by NM, 27-Mar-2006.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)) |
|
Theorem | xpsnen2g 6856 |
A set is equinumerous to its Cartesian product with a singleton on the
left. (Contributed by Stefan O'Rear, 21-Nov-2014.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × 𝐵) ≈ 𝐵) |
|
Theorem | xpassen 6857 |
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 6858 |
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 6859 |
Dominance law for Cartesian product. Theorem 6L(c) of [Enderton]
p. 149. (Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵)) |
|
Theorem | xpdom1g 6860 |
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 6861* |
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 6862 |
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 | pw2f1odclem 6863* |
Lemma for pw2f1odc 6864. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝐶 ∈ 𝑊)
& ⊢ (𝜑 → 𝐵 ≠ 𝐶)
& ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝒫 𝐴DECID 𝑝 ∈ 𝑞) ⇒ ⊢ (𝜑 → ((𝑆 ∈ 𝒫 𝐴 ∧ 𝐺 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑆, 𝐶, 𝐵))) ↔ (𝐺 ∈ ({𝐵, 𝐶} ↑𝑚 𝐴) ∧ 𝑆 = (◡𝐺 “ {𝐶})))) |
|
Theorem | pw2f1odc 6864* |
The power set of a set is equinumerous to set exponentiation with an
unordered pair base of ordinal 2. Generalized from Proposition 10.44 of
[TakeutiZaring] p. 96.
(Contributed by Mario Carneiro, 6-Oct-2014.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝐶 ∈ 𝑊)
& ⊢ (𝜑 → 𝐵 ≠ 𝐶)
& ⊢ (𝜑 → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝒫 𝐴DECID 𝑝 ∈ 𝑞)
& ⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑥, 𝐶, 𝐵))) ⇒ ⊢ (𝜑 → 𝐹:𝒫 𝐴–1-1-onto→({𝐵, 𝐶} ↑𝑚 𝐴)) |
|
Theorem | fopwdom 6865 |
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 6866 |
Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴) |
|
Theorem | dom0 6867 |
A set dominated by the empty set is empty. (Contributed by NM,
22-Nov-2004.)
|
⊢ (𝐴 ≼ ∅ ↔ 𝐴 = ∅) |
|
Theorem | 0dom 6868 |
Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ∅ ≼ 𝐴 |
|
Theorem | enen1 6869 |
Equality-like theorem for equinumerosity. (Contributed by NM,
18-Dec-2003.)
|
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≈ 𝐶 ↔ 𝐵 ≈ 𝐶)) |
|
Theorem | enen2 6870 |
Equality-like theorem for equinumerosity. (Contributed by NM,
18-Dec-2003.)
|
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≈ 𝐴 ↔ 𝐶 ≈ 𝐵)) |
|
Theorem | domen1 6871 |
Equality-like theorem for equinumerosity and dominance. (Contributed by
NM, 8-Nov-2003.)
|
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≼ 𝐶 ↔ 𝐵 ≼ 𝐶)) |
|
Theorem | domen2 6872 |
Equality-like theorem for equinumerosity and dominance. (Contributed by
NM, 8-Nov-2003.)
|
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≼ 𝐴 ↔ 𝐶 ≼ 𝐵)) |
|
2.6.29 Equinumerosity (cont.)
|
|
Theorem | xpf1o 6873* |
Construct a bijection on a Cartesian product given bijections on the
factors. (Contributed by Mario Carneiro, 30-May-2015.)
|
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑋):𝐴–1-1-onto→𝐵)
& ⊢ (𝜑 → (𝑦 ∈ 𝐶 ↦ 𝑌):𝐶–1-1-onto→𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 〈𝑋, 𝑌〉):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷)) |
|
Theorem | xpen 6874 |
Equinumerosity law for Cartesian product. Proposition 4.22(b) of
[Mendelson] p. 254. (Contributed by
NM, 24-Jul-2004.)
|
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 × 𝐶) ≈ (𝐵 × 𝐷)) |
|
Theorem | mapen 6875 |
Two set exponentiations are equinumerous when their bases and exponents
are equinumerous. Theorem 6H(c) of [Enderton] p. 139. (Contributed by
NM, 16-Dec-2003.) (Proof shortened by Mario Carneiro, 26-Apr-2015.)
|
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ↑𝑚 𝐶) ≈ (𝐵 ↑𝑚 𝐷)) |
|
Theorem | mapdom1g 6876 |
Order-preserving property of set exponentiation. (Contributed by Jim
Kingdon, 15-Jul-2022.)
|
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝐴 ↑𝑚 𝐶) ≼ (𝐵 ↑𝑚 𝐶)) |
|
Theorem | mapxpen 6877 |
Equinumerosity law for double set exponentiation. Proposition 10.45 of
[TakeutiZaring] p. 96.
(Contributed by NM, 21-Feb-2004.) (Revised by
Mario Carneiro, 24-Jun-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ↑𝑚 𝐵) ↑𝑚
𝐶) ≈ (𝐴 ↑𝑚
(𝐵 × 𝐶))) |
|
Theorem | xpmapenlem 6878* |
Lemma for xpmapen 6879. (Contributed by NM, 1-May-2004.) (Revised
by
Mario Carneiro, 16-Nov-2014.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 = (𝑧 ∈ 𝐶 ↦ (1st ‘(𝑥‘𝑧))) & ⊢ 𝑅 = (𝑧 ∈ 𝐶 ↦ (2nd ‘(𝑥‘𝑧))) & ⊢ 𝑆 = (𝑧 ∈ 𝐶 ↦ 〈((1st
‘𝑦)‘𝑧), ((2nd
‘𝑦)‘𝑧)〉) ⇒ ⊢ ((𝐴 × 𝐵) ↑𝑚 𝐶) ≈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) |
|
Theorem | xpmapen 6879 |
Equinumerosity law for set exponentiation of a Cartesian product.
Exercise 4.47 of [Mendelson] p. 255.
(Contributed by NM, 23-Feb-2004.)
(Proof shortened by Mario Carneiro, 16-Nov-2014.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈
V ⇒ ⊢ ((𝐴 × 𝐵) ↑𝑚 𝐶) ≈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) |
|
Theorem | ssenen 6880* |
Equinumerosity of equinumerous subsets of a set. (Contributed by NM,
30-Sep-2004.) (Revised by Mario Carneiro, 16-Nov-2014.)
|
⊢ (𝐴 ≈ 𝐵 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐶)} ≈ {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝑥 ≈ 𝐶)}) |
|
2.6.30 Pigeonhole Principle
|
|
Theorem | phplem1 6881 |
Lemma for Pigeonhole Principle. If we join a natural number to itself
minus an element, we end up with its successor minus the same element.
(Contributed by NM, 25-May-1998.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ({𝐴} ∪ (𝐴 ∖ {𝐵})) = (suc 𝐴 ∖ {𝐵})) |
|
Theorem | phplem2 6882 |
Lemma for Pigeonhole Principle. A natural number is equinumerous to its
successor minus one of its elements. (Contributed by NM, 11-Jun-1998.)
(Revised by Mario Carneiro, 16-Nov-2014.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) |
|
Theorem | phplem3 6883 |
Lemma for Pigeonhole Principle. A natural number is equinumerous to its
successor minus any element of the successor. For a version without the
redundant hypotheses, see phplem3g 6885. (Contributed by NM,
26-May-1998.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) |
|
Theorem | phplem4 6884 |
Lemma for Pigeonhole Principle. Equinumerosity of successors implies
equinumerosity of the original natural numbers. (Contributed by NM,
28-May-1998.) (Revised by Mario Carneiro, 24-Jun-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵)) |
|
Theorem | phplem3g 6885 |
A natural number is equinumerous to its successor minus any element of
the successor. Version of phplem3 6883 with unnecessary hypotheses
removed. (Contributed by Jim Kingdon, 1-Sep-2021.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) |
|
Theorem | nneneq 6886 |
Two equinumerous natural numbers are equal. Proposition 10.20 of
[TakeutiZaring] p. 90 and its
converse. Also compare Corollary 6E of
[Enderton] p. 136. (Contributed by NM,
28-May-1998.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) |
|
Theorem | php5 6887 |
A natural number is not equinumerous to its successor. Corollary
10.21(1) of [TakeutiZaring] p. 90.
(Contributed by NM, 26-Jul-2004.)
|
⊢ (𝐴 ∈ ω → ¬ 𝐴 ≈ suc 𝐴) |
|
Theorem | snnen2og 6888 |
A singleton {𝐴} is never equinumerous with the
ordinal number 2. If
𝐴 is a proper class, see snnen2oprc 6889. (Contributed by Jim Kingdon,
1-Sep-2021.)
|
⊢ (𝐴 ∈ 𝑉 → ¬ {𝐴} ≈ 2o) |
|
Theorem | snnen2oprc 6889 |
A singleton {𝐴} is never equinumerous with the
ordinal number 2. If
𝐴 is a set, see snnen2og 6888. (Contributed by Jim Kingdon,
1-Sep-2021.)
|
⊢ (¬ 𝐴 ∈ V → ¬ {𝐴} ≈ 2o) |
|
Theorem | 1nen2 6890 |
One and two are not equinumerous. (Contributed by Jim Kingdon,
25-Jan-2022.)
|
⊢ ¬ 1o ≈
2o |
|
Theorem | phplem4dom 6891 |
Dominance of successors implies dominance of the original natural
numbers. (Contributed by Jim Kingdon, 1-Sep-2021.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≼ suc 𝐵 → 𝐴 ≼ 𝐵)) |
|
Theorem | php5dom 6892 |
A natural number does not dominate its successor. (Contributed by Jim
Kingdon, 1-Sep-2021.)
|
⊢ (𝐴 ∈ ω → ¬ suc 𝐴 ≼ 𝐴) |
|
Theorem | nndomo 6893 |
Cardinal ordering agrees with natural number ordering. Example 3 of
[Enderton] p. 146. (Contributed by NM,
17-Jun-1998.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) |
|
Theorem | phpm 6894* |
Pigeonhole Principle. A natural number is not equinumerous to a proper
subset of itself. By "proper subset" here we mean that there
is an
element which is in the natural number and not in the subset, or in
symbols ∃𝑥𝑥 ∈ (𝐴 ∖ 𝐵) (which is stronger than not being
equal
in the absence of excluded middle). Theorem (Pigeonhole Principle) of
[Enderton] p. 134. The theorem is
so-called because you can't put n +
1 pigeons into n holes (if each hole holds only one pigeon). The
proof consists of lemmas phplem1 6881 through phplem4 6884, nneneq 6886, and
this final piece of the proof. (Contributed by NM, 29-May-1998.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴 ∧ ∃𝑥 𝑥 ∈ (𝐴 ∖ 𝐵)) → ¬ 𝐴 ≈ 𝐵) |
|
Theorem | phpelm 6895 |
Pigeonhole Principle. A natural number is not equinumerous to an
element of itself. (Contributed by Jim Kingdon, 6-Sep-2021.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ¬ 𝐴 ≈ 𝐵) |
|
Theorem | phplem4on 6896 |
Equinumerosity of successors of an ordinal and a natural number implies
equinumerosity of the originals. (Contributed by Jim Kingdon,
5-Sep-2021.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵)) |
|
2.6.31 Finite sets
|
|
Theorem | fict 6897 |
A finite set is dominated by ω. Also see finct 7146. (Contributed
by Thierry Arnoux, 27-Mar-2018.)
|
⊢ (𝐴 ∈ Fin → 𝐴 ≼ ω) |
|
Theorem | fidceq 6898 |
Equality of members of a finite set is decidable. This may be
counterintuitive: cannot any two sets be elements of a finite set?
Well, to show, for example, that {𝐵, 𝐶} is finite would require
showing it is equinumerous to 1o or
to 2o but to show that you'd
need to know 𝐵 = 𝐶 or ¬ 𝐵 = 𝐶, respectively. (Contributed by
Jim Kingdon, 5-Sep-2021.)
|
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → DECID 𝐵 = 𝐶) |
|
Theorem | fidifsnen 6899 |
All decrements of a finite set are equinumerous. (Contributed by Jim
Kingdon, 9-Sep-2021.)
|
⊢ ((𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵})) |
|
Theorem | fidifsnid 6900 |
If we remove a single element from a finite set then put it back in, we
end up with the original finite set. This strengthens difsnss 3753 from
subset to equality when the set is finite. (Contributed by Jim Kingdon,
9-Sep-2021.)
|
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |