![]() |
Metamath
Proof Explorer Theorem List (p. 88 of 454) | < 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: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 1sdom2 8701 | Ordinal 1 is strictly dominated by ordinal 2. (Contributed by NM, 4-Apr-2007.) |
⊢ 1o ≺ 2o | ||
Theorem | sdom1 8702 | A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅) | ||
Theorem | modom 8703 | Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (∃*𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≼ 1o) | ||
Theorem | modom2 8704* | Two ways to express "at most one". (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 ≼ 1o) | ||
Theorem | 1sdom 8705* | A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom 8565.) (Contributed by Mario Carneiro, 12-Jan-2013.) |
⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) | ||
Theorem | unxpdomlem1 8706* | Lemma for unxpdom 8709. (Trivial substitution proof.) (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) ⇒ ⊢ (𝑧 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉)) | ||
Theorem | unxpdomlem2 8707* | Lemma for unxpdom 8709. (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) & ⊢ (𝜑 → 𝑤 ∈ (𝑎 ∪ 𝑏)) & ⊢ (𝜑 → ¬ 𝑚 = 𝑛) & ⊢ (𝜑 → ¬ 𝑠 = 𝑡) ⇒ ⊢ ((𝜑 ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) | ||
Theorem | unxpdomlem3 8708* | Lemma for unxpdom 8709. (Contributed by Mario Carneiro, 13-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) ⇒ ⊢ ((1o ≺ 𝑎 ∧ 1o ≺ 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)) | ||
Theorem | unxpdom 8709 | 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 8710 | Corollary of unxpdom 8709. (Contributed by NM, 16-Sep-2004.) |
⊢ ((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴)) | ||
Theorem | sucxpdom 8711 | 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 8712 | 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 8713 | A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵) | ||
Theorem | ominf 8714 | The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.) |
⊢ ¬ ω ∈ Fin | ||
Theorem | isinf 8715* | 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 8716 | Lemma for fineqv 8717. (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 8717 | 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 8718 | Equinumerous sets have the same finiteness. (Contributed by NM, 22-Aug-2008.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin)) | ||
Theorem | enfii 8719 | A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin) | ||
Theorem | pssnn 8720* | 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 8721 | A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
Theorem | ssfi 8722 | A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. (Contributed by NM, 24-Jun-1998.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
Theorem | domfi 8723 | 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 8724 | 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 8725 | A subset of a finite set is finite, deduction version of ssfi 8722. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ Fin) | ||
Theorem | infi 8726 | The intersection of two sets is finite if one of them is. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (𝐴 ∈ Fin → (𝐴 ∩ 𝐵) ∈ Fin) | ||
Theorem | rabfi 8727* | A restricted class built from a finite set is finite. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (𝐴 ∈ Fin → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ Fin) | ||
Theorem | finresfin 8728 | The restriction of a finite set is finite. (Contributed by Alexander van der Vekens, 3-Jan-2018.) |
⊢ (𝐸 ∈ Fin → (𝐸 ↾ 𝐵) ∈ Fin) | ||
Theorem | f1finf1o 8729 | 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 8730 | The empty set is finite. (Contributed by FL, 14-Jul-2008.) |
⊢ ∅ ∈ Fin | ||
Theorem | nfielex 8731* | 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 8732 | A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o) → 𝐵 = {𝐴}) | ||
Theorem | en1eqsnbi 8733 | A set containing an element has exactly one element iff it is a singleton. Formerly part of proof for rngen1zr 20042. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
⊢ (𝐴 ∈ 𝐵 → (𝐵 ≈ 1o ↔ 𝐵 = {𝐴})) | ||
Theorem | diffi 8734 | If 𝐴 is finite, (𝐴 ∖ 𝐵) is finite. (Contributed by FL, 3-Aug-2009.) |
⊢ (𝐴 ∈ Fin → (𝐴 ∖ 𝐵) ∈ Fin) | ||
Theorem | dif1en 8735 | 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 8736 | Lemma for uses of enp1i 8737. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 𝑇 = ({𝑥} ∪ 𝑆) ⇒ ⊢ (𝑥 ∈ 𝐴 → ((𝐴 ∖ {𝑥}) = 𝑆 → 𝐴 = 𝑇)) | ||
Theorem | enp1i 8737* | Proof induction for en2i 8530 and related theorems. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 𝑀 ∈ ω & ⊢ 𝑁 = suc 𝑀 & ⊢ ((𝐴 ∖ {𝑥}) ≈ 𝑀 → 𝜑) & ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ≈ 𝑁 → ∃𝑥𝜓) | ||
Theorem | en2 8738* | A set equinumerous to ordinal 2 is a pair. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 2o → ∃𝑥∃𝑦 𝐴 = {𝑥, 𝑦}) | ||
Theorem | en3 8739* | A set equinumerous to ordinal 3 is a triple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 3o → ∃𝑥∃𝑦∃𝑧 𝐴 = {𝑥, 𝑦, 𝑧}) | ||
Theorem | en4 8740* | A set equinumerous to ordinal 4 is a quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 4o → ∃𝑥∃𝑦∃𝑧∃𝑤 𝐴 = ({𝑥, 𝑦} ∪ {𝑧, 𝑤})) | ||
Theorem | findcard 8741* | 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 8742* | 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 8743* | Variation of findcard2 8742 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 8744* | Deduction version of findcard2 8742. (Contributed by SO, 16-Jul-2018.) |
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝜃 → 𝜏)) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | findcard3 8745* | 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 8746* | A version of ac6s 9895 for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | frfi 8747 | 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 8748* | 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 8749* | 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 8750* | Lemma showing existence and closure of supremum of a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))) | ||
Theorem | wofi 8751 | 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 8752 | 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 8753 | 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 8754* | Lemma for unbnn 8758. 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 8755* | Lemma for unbnn 8758. The value of the function 𝐹 belongs to the unbounded set of natural numbers 𝐴. (Contributed by NM, 3-Dec-2003.) |
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω) ⇒ ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ 𝐴)) | ||
Theorem | unblem3 8756* | Lemma for unbnn 8758. 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 8757* | Lemma for unbnn 8758. 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 8758* | 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 9106 for a stronger version without the first assumption. (Contributed by NM, 3-Dec-2003.) |
⊢ ((ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → 𝐴 ≈ ω) | ||
Theorem | unbnn2 8759* | Version of unbnn 8758 that does not require a strict upper bound. (Contributed by NM, 24-Apr-2004.) |
⊢ ((ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) → 𝐴 ≈ ω) | ||
Theorem | isfinite2 8760 | 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 8761 | 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 8762 | 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 8763 | An infinite set strictly dominates a natural number. (Contributed by NM, 22-Nov-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) |
⊢ ((ω ≼ 𝐴 ∧ 𝐵 ∈ ω) → 𝐵 ≺ 𝐴) | ||
Theorem | infn0 8764 | An infinite set is not empty. (Contributed by NM, 23-Oct-2004.) |
⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅) | ||
Theorem | fin2inf 8765 | 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 8766* | 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 8767* | 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 8768 | 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 8769 | 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 8770 | If a union is finite, the operands are finite. Converse of unfi 8769. (Contributed by FL, 3-Aug-2009.) |
⊢ ((𝐴 ∪ 𝐵) ∈ Fin → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) | ||
Theorem | unfi2 8771 | The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. This version of unfi 8769 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 8765). (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) |
⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 ∪ 𝐵) ≺ ω) | ||
Theorem | difinf 8772 | An infinite set 𝐴 minus a finite set is infinite. (Contributed by FL, 3-Aug-2009.) |
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ¬ (𝐴 ∖ 𝐵) ∈ Fin) | ||
Theorem | xpfi 8773 | 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 8774 | The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
⊢ (𝑉 ∈ Fin → ((𝑉 × 𝑉) × 𝑉) ∈ Fin) | ||
Theorem | domunfican 8775 | 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 8776* | 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 8777 | An unordered pair is finite. (Contributed by NM, 22-Aug-2008.) |
⊢ {𝐴, 𝐵} ∈ Fin | ||
Theorem | tpfi 8778 | An unordered triple is finite. (Contributed by Mario Carneiro, 28-Sep-2013.) |
⊢ {𝐴, 𝐵, 𝐶} ∈ Fin | ||
Theorem | fiint 8779* | 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 8780 | A version of fnex 6957 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 8781 | An onto function implies dominance of domain over range, for finite sets. Unlike fodom 9934 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→𝐵) → 𝐵 ≼ 𝐴) | ||
Theorem | fodomfib 8782* | Equivalence of an onto mapping and dominance for a nonempty finite set. Unlike fodomb 9937 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.) |
⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) | ||
Theorem | fofinf1o 8783 | Any surjection from one finite set to another of equal size must be a bijection. (Contributed by Mario Carneiro, 19-Aug-2014.) |
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → 𝐹:𝐴–1-1-onto→𝐵) | ||
Theorem | rneqdmfinf1o 8784 | Any function from a finite set onto the same set must be a bijection. (Contributed by AV, 5-Jul-2021.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐴) → 𝐹:𝐴–1-1-onto→𝐴) | ||
Theorem | fidomdm 8785 | Any finite set dominates its domain. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐹 ∈ Fin → dom 𝐹 ≼ 𝐹) | ||
Theorem | dmfi 8786 | The domain of a finite set is finite. (Contributed by Mario Carneiro, 24-Sep-2013.) |
⊢ (𝐴 ∈ Fin → dom 𝐴 ∈ Fin) | ||
Theorem | fundmfibi 8787 | A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.) |
⊢ (Fun 𝐹 → (𝐹 ∈ Fin ↔ dom 𝐹 ∈ Fin)) | ||
Theorem | resfnfinfin 8788 | The restriction of a function to a finite set is finite. (Contributed by Alexander van der Vekens, 3-Feb-2018.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ Fin) → (𝐹 ↾ 𝐵) ∈ Fin) | ||
Theorem | residfi 8789 | A restricted identity function is finite iff the restricting class is finite. (Contributed by AV, 10-Jan-2020.) |
⊢ (( I ↾ 𝐴) ∈ Fin ↔ 𝐴 ∈ Fin) | ||
Theorem | cnvfi 8790 | If a set is finite, its converse is as well. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ (𝐴 ∈ Fin → ◡𝐴 ∈ Fin) | ||
Theorem | rnfi 8791 | The range of a finite set is finite. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ (𝐴 ∈ Fin → ran 𝐴 ∈ Fin) | ||
Theorem | f1dmvrnfibi 8792 | A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 8793. (Contributed by AV, 10-Jan-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin)) | ||
Theorem | f1vrnfibi 8793 | A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 8792. (Contributed by AV, 10-Jan-2020.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin)) | ||
Theorem | fofi 8794 | If a function has a finite domain, its range is finite. Theorem 37 of [Suppes] p. 104. (Contributed by NM, 25-Mar-2007.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ Fin) | ||
Theorem | f1fi 8795 | If a 1-to-1 function has a finite codomain its domain is finite. (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ∈ Fin) | ||
Theorem | iunfi 8796* | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 8797. Note that 𝐵 depends on 𝑥, i.e. can be thought of as 𝐵(𝑥). (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin) | ||
Theorem | unifi 8797 | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. (Contributed by NM, 22-Aug-2008.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴 ∈ Fin) | ||
Theorem | unifi2 8798* | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This version of unifi 8797 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 8765). (Contributed by NM, 11-Mar-2006.) |
⊢ ((𝐴 ≺ ω ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ ω) → ∪ 𝐴 ≺ ω) | ||
Theorem | infssuni 8799* | If an infinite set 𝐴 is included in the underlying set of a finite cover 𝐵, then there exists a set of the cover that contains an infinite number of element of 𝐴. (Contributed by FL, 2-Aug-2009.) |
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐴 ⊆ ∪ 𝐵) → ∃𝑥 ∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin) | ||
Theorem | unirnffid 8800 | The union of the range of a function from a finite set into the class of finite sets is finite. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐹:𝑇⟶Fin) & ⊢ (𝜑 → 𝑇 ∈ Fin) ⇒ ⊢ (𝜑 → ∪ ran 𝐹 ∈ Fin) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |