Home | Metamath
Proof Explorer Theorem List (p. 88 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28698) |
Hilbert Space Explorer
(28699-30221) |
Users' Mathboxes
(30222-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | phplem3 8701 | Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus any element of the successor. (Contributed by NM, 26-May-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) | ||
Theorem | phplem4 8702 | 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 | nneneq 8703 | 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 | php 8704 | Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. 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 8699 through phplem4 8702, nneneq 8703, and this final piece of the proof. (Contributed by NM, 29-May-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵) | ||
Theorem | php2 8705 | Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
Theorem | php3 8706 | Corollary of Pigeonhole Principle. If 𝐴 is finite and 𝐵 is a proper subset of 𝐴, the 𝐵 is strictly less numerous than 𝐴. Stronger version of Corollary 6C of [Enderton] p. 135. (Contributed by NM, 22-Aug-2008.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
Theorem | php4 8707 | Corollary of the Pigeonhole Principle php 8704: a natural number is strictly dominated by its successor. (Contributed by NM, 26-Jul-2004.) |
⊢ (𝐴 ∈ ω → 𝐴 ≺ suc 𝐴) | ||
Theorem | php5 8708 | Corollary of the Pigeonhole Principle php 8704: 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 | phpeqd 8709 | Corollary of the Pigeonhole Principle using equality. Strengthening of php 8704 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | snnen2o 8710 | A singleton {𝐴} is never equinumerous with the ordinal number 2. This holds for proper singletons (𝐴 ∈ V) as well as for singletons being the empty set (𝐴 ∉ V). (Contributed by AV, 6-Aug-2019.) |
⊢ ¬ {𝐴} ≈ 2o | ||
Theorem | onomeneq 8711 | An ordinal number equinumerous to a natural number is equal to it. Proposition 10.22 of [TakeutiZaring] p. 90 and its converse. (Contributed by NM, 26-Jul-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | onfin 8712 | An ordinal number is finite iff it is a natural number. Proposition 10.32 of [TakeutiZaring] p. 92. (Contributed by NM, 26-Jul-2004.) |
⊢ (𝐴 ∈ On → (𝐴 ∈ Fin ↔ 𝐴 ∈ ω)) | ||
Theorem | onfin2 8713 | A set is a natural number iff it is a finite ordinal. (Contributed by Mario Carneiro, 22-Jan-2013.) |
⊢ ω = (On ∩ Fin) | ||
Theorem | nnfi 8714 | Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin) | ||
Theorem | nndomo 8715 | Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146. (Contributed by NM, 17-Jun-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | nnsdomo 8716 | Cardinal ordering agrees with natural number ordering. (Contributed by NM, 17-Jun-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≺ 𝐵 ↔ 𝐴 ⊊ 𝐵)) | ||
Theorem | sucdom2 8717 | Strict dominance of a set over another set implies dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) |
⊢ (𝐴 ≺ 𝐵 → suc 𝐴 ≼ 𝐵) | ||
Theorem | sucdom 8718 | Strict dominance of a set over a natural number is the same as dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013.) |
⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵)) | ||
Theorem | 0sdom1dom 8719 | Strict dominance over zero is the same as dominance over one. (Contributed by NM, 28-Sep-2004.) |
⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴) | ||
Theorem | 1sdom2 8720 | Ordinal 1 is strictly dominated by ordinal 2. (Contributed by NM, 4-Apr-2007.) |
⊢ 1o ≺ 2o | ||
Theorem | sdom1 8721 | A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅) | ||
Theorem | modom 8722 | Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (∃*𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≼ 1o) | ||
Theorem | modom2 8723* | Two ways to express "at most one". (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 ≼ 1o) | ||
Theorem | 1sdom 8724* | A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom 8585.) (Contributed by Mario Carneiro, 12-Jan-2013.) |
⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) | ||
Theorem | unxpdomlem1 8725* | Lemma for unxpdom 8728. (Trivial substitution proof.) (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) ⇒ ⊢ (𝑧 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉)) | ||
Theorem | unxpdomlem2 8726* | Lemma for unxpdom 8728. (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) & ⊢ (𝜑 → 𝑤 ∈ (𝑎 ∪ 𝑏)) & ⊢ (𝜑 → ¬ 𝑚 = 𝑛) & ⊢ (𝜑 → ¬ 𝑠 = 𝑡) ⇒ ⊢ ((𝜑 ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) | ||
Theorem | unxpdomlem3 8727* | Lemma for unxpdom 8728. (Contributed by Mario Carneiro, 13-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) ⇒ ⊢ ((1o ≺ 𝑎 ∧ 1o ≺ 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)) | ||
Theorem | unxpdom 8728 | Cartesian product dominates union for sets with cardinality greater than 1. Proposition 10.36 of [TakeutiZaring] p. 93. (Contributed by Mario Carneiro, 13-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) |
⊢ ((1o ≺ 𝐴 ∧ 1o ≺ 𝐵) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐵)) | ||
Theorem | unxpdom2 8729 | Corollary of unxpdom 8728. (Contributed by NM, 16-Sep-2004.) |
⊢ ((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴)) | ||
Theorem | sucxpdom 8730 | Cartesian product dominates successor for set with cardinality greater than 1. Proposition 10.38 of [TakeutiZaring] p. 93 (but generalized to arbitrary sets, not just ordinals). (Contributed by NM, 3-Sep-2004.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) |
⊢ (1o ≺ 𝐴 → suc 𝐴 ≼ (𝐴 × 𝐴)) | ||
Theorem | pssinf 8731 | A set equinumerous to a proper subset of itself is infinite. Corollary 6D(a) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.) |
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐴 ≈ 𝐵) → ¬ 𝐵 ∈ Fin) | ||
Theorem | fisseneq 8732 | A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵) | ||
Theorem | ominf 8733 | The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.) |
⊢ ¬ ω ∈ Fin | ||
Theorem | isinf 8734* | Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set has countably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by Mario Carneiro, 15-Jan-2013.) |
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)) | ||
Theorem | fineqvlem 8735 | Lemma for fineqv 8736. (Contributed by Mario Carneiro, 20-Jan-2013.) (Proof shortened by Stefan O'Rear, 3-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ω ≼ 𝒫 𝒫 𝐴) | ||
Theorem | fineqv 8736 | If the Axiom of Infinity is denied, then all sets are finite (which implies the Axiom of Choice). (Contributed by Mario Carneiro, 20-Jan-2013.) (Revised by Mario Carneiro, 3-Jan-2015.) |
⊢ (¬ ω ∈ V ↔ Fin = V) | ||
Theorem | enfi 8737 | Equinumerous sets have the same finiteness. (Contributed by NM, 22-Aug-2008.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin)) | ||
Theorem | enfii 8738 | A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin) | ||
Theorem | pssnn 8739* | A proper subset of a natural number is equinumerous to some smaller number. Lemma 6F of [Enderton] p. 137. (Contributed by NM, 22-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥) | ||
Theorem | ssnnfi 8740 | A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
Theorem | ssfi 8741 | A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. (Contributed by NM, 24-Jun-1998.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
Theorem | domfi 8742 | A set dominated by a finite set is finite. (Contributed by NM, 23-Mar-2006.) (Revised by Mario Carneiro, 12-Mar-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ Fin) | ||
Theorem | xpfir 8743 | The components of a nonempty finite Cartesian product are finite. (Contributed by Paul Chapman, 11-Apr-2009.) (Proof shortened by Mario Carneiro, 29-Apr-2015.) |
⊢ (((𝐴 × 𝐵) ∈ Fin ∧ (𝐴 × 𝐵) ≠ ∅) → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) | ||
Theorem | ssfid 8744 | A subset of a finite set is finite, deduction version of ssfi 8741. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ Fin) | ||
Theorem | infi 8745 | The intersection of two sets is finite if one of them is. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (𝐴 ∈ Fin → (𝐴 ∩ 𝐵) ∈ Fin) | ||
Theorem | rabfi 8746* | A restricted class built from a finite set is finite. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (𝐴 ∈ Fin → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ Fin) | ||
Theorem | finresfin 8747 | The restriction of a finite set is finite. (Contributed by Alexander van der Vekens, 3-Jan-2018.) |
⊢ (𝐸 ∈ Fin → (𝐸 ↾ 𝐵) ∈ Fin) | ||
Theorem | f1finf1o 8748 | Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010.) (Revised by Mario Carneiro, 27-Feb-2014.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵)) | ||
Theorem | 0fin 8749 | The empty set is finite. (Contributed by FL, 14-Jul-2008.) |
⊢ ∅ ∈ Fin | ||
Theorem | nfielex 8750* | If a class is not finite, then it contains at least one element. (Contributed by Alexander van der Vekens, 12-Jan-2018.) |
⊢ (¬ 𝐴 ∈ Fin → ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | en1eqsn 8751 | A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o) → 𝐵 = {𝐴}) | ||
Theorem | en1eqsnbi 8752 | A set containing an element has exactly one element iff it is a singleton. Formerly part of proof for rngen1zr 20052. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
⊢ (𝐴 ∈ 𝐵 → (𝐵 ≈ 1o ↔ 𝐵 = {𝐴})) | ||
Theorem | diffi 8753 | If 𝐴 is finite, (𝐴 ∖ 𝐵) is finite. (Contributed by FL, 3-Aug-2009.) |
⊢ (𝐴 ∈ Fin → (𝐴 ∖ 𝐵) ∈ Fin) | ||
Theorem | dif1en 8754 | If a set 𝐴 is equinumerous to the successor of a natural number 𝑀, then 𝐴 with an element removed is equinumerous to 𝑀. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) |
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀) | ||
Theorem | enp1ilem 8755 | Lemma for uses of enp1i 8756. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 𝑇 = ({𝑥} ∪ 𝑆) ⇒ ⊢ (𝑥 ∈ 𝐴 → ((𝐴 ∖ {𝑥}) = 𝑆 → 𝐴 = 𝑇)) | ||
Theorem | enp1i 8756* | Proof induction for en2i 8550 and related theorems. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 𝑀 ∈ ω & ⊢ 𝑁 = suc 𝑀 & ⊢ ((𝐴 ∖ {𝑥}) ≈ 𝑀 → 𝜑) & ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ≈ 𝑁 → ∃𝑥𝜓) | ||
Theorem | en2 8757* | A set equinumerous to ordinal 2 is a pair. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 2o → ∃𝑥∃𝑦 𝐴 = {𝑥, 𝑦}) | ||
Theorem | en3 8758* | A set equinumerous to ordinal 3 is a triple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 3o → ∃𝑥∃𝑦∃𝑧 𝐴 = {𝑥, 𝑦, 𝑧}) | ||
Theorem | en4 8759* | A set equinumerous to ordinal 4 is a quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 4o → ∃𝑥∃𝑦∃𝑧∃𝑤 𝐴 = ({𝑥, 𝑦} ∪ {𝑧, 𝑤})) | ||
Theorem | findcard 8760* | Schema for induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on the given set with any one element removed. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = (𝑦 ∖ {𝑧}) → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ Fin → (∀𝑧 ∈ 𝑦 𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ Fin → 𝜏) | ||
Theorem | findcard2 8761* | Schema for induction on the cardinality of a finite set. The inductive step shows that the result is true if one more element is added to the set. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 8-Jul-2010.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ Fin → 𝜏) | ||
Theorem | findcard2s 8762* | Variation of findcard2 8761 requiring that the element added in the induction step not be a member of the original set. (Contributed by Paul Chapman, 30-Nov-2012.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ Fin → 𝜏) | ||
Theorem | findcard2d 8763* | Deduction version of findcard2 8761. (Contributed by SO, 16-Jul-2018.) |
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝜃 → 𝜏)) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | findcard3 8764* | Schema for strong induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on any proper subset. The result is then proven to be true for all finite sets. (Contributed by Mario Carneiro, 13-Dec-2013.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝑦 ∈ Fin → (∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒)) ⇒ ⊢ (𝐴 ∈ Fin → 𝜏) | ||
Theorem | ac6sfi 8765* | A version of ac6s 9909 for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | frfi 8766 | A partial order is well-founded on a finite set. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
⊢ ((𝑅 Po 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 Fr 𝐴) | ||
Theorem | fimax2g 8767* | A finite set has a maximum under a total order. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦) | ||
Theorem | fimaxg 8768* | A finite set has a maximum under a total order. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → 𝑦𝑅𝑥)) | ||
Theorem | fisupg 8769* | Lemma showing existence and closure of supremum of a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))) | ||
Theorem | wofi 8770 | A total order on a finite set is a well-order. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 We 𝐴) | ||
Theorem | ordunifi 8771 | The maximum of a finite collection of ordinals is in the set. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 29-Jan-2014.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∪ 𝐴 ∈ 𝐴) | ||
Theorem | nnunifi 8772 | The union (supremum) of a finite set of finite ordinals is a finite ordinal. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ ((𝑆 ⊆ ω ∧ 𝑆 ∈ Fin) → ∪ 𝑆 ∈ ω) | ||
Theorem | unblem1 8773* | Lemma for unbnn 8777. After removing the successor of an element from an unbounded set of natural numbers, the intersection of the result belongs to the original unbounded set. (Contributed by NM, 3-Dec-2003.) |
⊢ (((𝐵 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦) ∧ 𝐴 ∈ 𝐵) → ∩ (𝐵 ∖ suc 𝐴) ∈ 𝐵) | ||
Theorem | unblem2 8774* | Lemma for unbnn 8777. The value of the function 𝐹 belongs to the unbounded set of natural numbers 𝐴. (Contributed by NM, 3-Dec-2003.) |
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω) ⇒ ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ 𝐴)) | ||
Theorem | unblem3 8775* | Lemma for unbnn 8777. The value of the function 𝐹 is less than its value at a successor. (Contributed by NM, 3-Dec-2003.) |
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω) ⇒ ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ (𝐹‘suc 𝑧))) | ||
Theorem | unblem4 8776* | Lemma for unbnn 8777. The function 𝐹 maps the set of natural numbers one-to-one to the set of unbounded natural numbers 𝐴. (Contributed by NM, 3-Dec-2003.) |
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω) ⇒ ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → 𝐹:ω–1-1→𝐴) | ||
Theorem | unbnn 8777* | Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. Part of the proof of Theorem 42 of [Suppes] p. 151. See unbnn3 9125 for a stronger version without the first assumption. (Contributed by NM, 3-Dec-2003.) |
⊢ ((ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → 𝐴 ≈ ω) | ||
Theorem | unbnn2 8778* | Version of unbnn 8777 that does not require a strict upper bound. (Contributed by NM, 24-Apr-2004.) |
⊢ ((ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) → 𝐴 ≈ ω) | ||
Theorem | isfinite2 8779 | Any set strictly dominated by the class of natural numbers is finite. Sufficiency part of Theorem 42 of [Suppes] p. 151. This theorem does not require the Axiom of Infinity. (Contributed by NM, 24-Apr-2004.) |
⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin) | ||
Theorem | nnsdomg 8780 | Omega strictly dominates a natural number. Example 3 of [Enderton] p. 146. In order to avoid the Axiom of infinity, we include it as a hypothesis. (Contributed by NM, 15-Jun-1998.) |
⊢ ((ω ∈ V ∧ 𝐴 ∈ ω) → 𝐴 ≺ ω) | ||
Theorem | isfiniteg 8781 | A set is finite iff it is strictly dominated by the class of natural number. Theorem 42 of [Suppes] p. 151. In order to avoid the Axiom of infinity, we include it as a hypothesis. (Contributed by NM, 3-Nov-2002.) (Revised by Mario Carneiro, 27-Apr-2015.) |
⊢ (ω ∈ V → (𝐴 ∈ Fin ↔ 𝐴 ≺ ω)) | ||
Theorem | infsdomnn 8782 | An infinite set strictly dominates a natural number. (Contributed by NM, 22-Nov-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) |
⊢ ((ω ≼ 𝐴 ∧ 𝐵 ∈ ω) → 𝐵 ≺ 𝐴) | ||
Theorem | infn0 8783 | An infinite set is not empty. (Contributed by NM, 23-Oct-2004.) |
⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅) | ||
Theorem | fin2inf 8784 | This (useless) theorem, which was proved without the Axiom of Infinity, demonstrates an artifact of our definition of binary relation, which is meaningful only when its arguments exist. In particular, the antecedent cannot be satisfied unless ω exists. (Contributed by NM, 13-Nov-2003.) |
⊢ (𝐴 ≺ ω → ω ∈ V) | ||
Theorem | unfilem1 8785* | Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 10-Nov-2002.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ ω & ⊢ 𝐵 ∈ ω & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥)) ⇒ ⊢ ran 𝐹 = ((𝐴 +o 𝐵) ∖ 𝐴) | ||
Theorem | unfilem2 8786* | Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 10-Nov-2002.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ ω & ⊢ 𝐵 ∈ ω & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥)) ⇒ ⊢ 𝐹:𝐵–1-1-onto→((𝐴 +o 𝐵) ∖ 𝐴) | ||
Theorem | unfilem3 8787 | Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 16-Nov-2002.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐵 ≈ ((𝐴 +o 𝐵) ∖ 𝐴)) | ||
Theorem | unfi 8788 | The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 16-Nov-2002.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin) | ||
Theorem | unfir 8789 | If a union is finite, the operands are finite. Converse of unfi 8788. (Contributed by FL, 3-Aug-2009.) |
⊢ ((𝐴 ∪ 𝐵) ∈ Fin → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) | ||
Theorem | unfi2 8790 | The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. This version of unfi 8788 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 8784). (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) |
⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 ∪ 𝐵) ≺ ω) | ||
Theorem | difinf 8791 | An infinite set 𝐴 minus a finite set is infinite. (Contributed by FL, 3-Aug-2009.) |
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ¬ (𝐴 ∖ 𝐵) ∈ Fin) | ||
Theorem | xpfi 8792 | The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin) | ||
Theorem | 3xpfi 8793 | The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
⊢ (𝑉 ∈ Fin → ((𝑉 × 𝑉) × 𝑉) ∈ Fin) | ||
Theorem | domunfican 8794 | A finite set union cancellation law for dominance. (Contributed by Stefan O'Rear, 19-Feb-2015.) (Revised by Stefan O'Rear, 5-May-2015.) |
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ≈ 𝐴) ∧ ((𝐴 ∩ 𝑋) = ∅ ∧ (𝐵 ∩ 𝑌) = ∅)) → ((𝐴 ∪ 𝑋) ≼ (𝐵 ∪ 𝑌) ↔ 𝑋 ≼ 𝑌)) | ||
Theorem | infcntss 8795* | Every infinite set has a denumerable subset. Similar to Exercise 8 of [TakeutiZaring] p. 91. (However, we need neither AC nor the Axiom of Infinity because of the way we express "infinite" in the antecedent.) (Contributed by NM, 23-Oct-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (ω ≼ 𝐴 → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω)) | ||
Theorem | prfi 8796 | An unordered pair is finite. (Contributed by NM, 22-Aug-2008.) |
⊢ {𝐴, 𝐵} ∈ Fin | ||
Theorem | tpfi 8797 | An unordered triple is finite. (Contributed by Mario Carneiro, 28-Sep-2013.) |
⊢ {𝐴, 𝐵, 𝐶} ∈ Fin | ||
Theorem | fiint 8798* | Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite nonempty subcollection of 𝐴 is in 𝐴". This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally. (Contributed by NM, 22-Sep-2002.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴)) | ||
Theorem | fnfi 8799 | A version of fnex 6983 for finite sets that does not require Replacement. (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin) → 𝐹 ∈ Fin) | ||
Theorem | fodomfi 8800 | An onto function implies dominance of domain over range, for finite sets. Unlike fodom 9947 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |