| Metamath
Proof Explorer Theorem List (p. 94 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ssfid 9301 | A subset of a finite set is finite, deduction version of ssfi 9213. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ Fin) | ||
| Theorem | infi 9302 | The intersection of two sets is finite if one of them is. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
| ⊢ (𝐴 ∈ Fin → (𝐴 ∩ 𝐵) ∈ Fin) | ||
| Theorem | rabfi 9303* | A restricted class built from a finite set is finite. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
| ⊢ (𝐴 ∈ Fin → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ Fin) | ||
| Theorem | finresfin 9304 | The restriction of a finite set is finite. (Contributed by Alexander van der Vekens, 3-Jan-2018.) |
| ⊢ (𝐸 ∈ Fin → (𝐸 ↾ 𝐵) ∈ Fin) | ||
| Theorem | f1finf1o 9305 | 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.) Avoid ax-pow 5365. (Revised by BTernaryTau, 4-Jan-2025.) |
| ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵)) | ||
| Theorem | f1finf1oOLD 9306 | Obsolete version of f1finf1o 9305 as of 4-Jan-2025. (Contributed by Jeff Madsen, 5-Jun-2010.) (Revised by Mario Carneiro, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵)) | ||
| Theorem | nfielex 9307* | 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 9308 | A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) Avoid ax-pow 5365, ax-un 7755. (Revised by BTernaryTau, 4-Jan-2025.) |
| ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o) → 𝐵 = {𝐴}) | ||
| Theorem | en1eqsnOLD 9309 | Obsolete version of en1eqsn 9308 as of 4-Jan-2025. (Contributed by FL, 18-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o) → 𝐵 = {𝐴}) | ||
| Theorem | en1eqsnbi 9310 | A set containing an element has exactly one element iff it is a singleton. Formerly part of proof for rngen1zr 20778. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
| ⊢ (𝐴 ∈ 𝐵 → (𝐵 ≈ 1o ↔ 𝐵 = {𝐴})) | ||
| Theorem | dif1ennnALT 9311 | Alternate proof of dif1ennn 9201 using ax-pow 5365. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀) | ||
| Theorem | enp1ilem 9312 | Lemma for uses of enp1i 9313. (Contributed by Mario Carneiro, 5-Jan-2016.) |
| ⊢ 𝑇 = ({𝑥} ∪ 𝑆) ⇒ ⊢ (𝑥 ∈ 𝐴 → ((𝐴 ∖ {𝑥}) = 𝑆 → 𝐴 = 𝑇)) | ||
| Theorem | enp1i 9313* | Proof induction for en2 9315 and related theorems. (Contributed by Mario Carneiro, 5-Jan-2016.) Generalize to all ordinals and avoid ax-pow 5365, ax-un 7755. (Revised by BTernaryTau, 6-Jan-2025.) |
| ⊢ Ord 𝑀 & ⊢ 𝑁 = suc 𝑀 & ⊢ ((𝐴 ∖ {𝑥}) ≈ 𝑀 → 𝜑) & ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ≈ 𝑁 → ∃𝑥𝜓) | ||
| Theorem | enp1iOLD 9314* | Obsolete version of enp1i 9313 as of 6-Jan-2025. (Contributed by Mario Carneiro, 5-Jan-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑀 ∈ ω & ⊢ 𝑁 = suc 𝑀 & ⊢ ((𝐴 ∖ {𝑥}) ≈ 𝑀 → 𝜑) & ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ≈ 𝑁 → ∃𝑥𝜓) | ||
| Theorem | en2 9315* | A set equinumerous to ordinal 2 is a pair. (Contributed by Mario Carneiro, 5-Jan-2016.) |
| ⊢ (𝐴 ≈ 2o → ∃𝑥∃𝑦 𝐴 = {𝑥, 𝑦}) | ||
| Theorem | en3 9316* | A set equinumerous to ordinal 3 is a triple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
| ⊢ (𝐴 ≈ 3o → ∃𝑥∃𝑦∃𝑧 𝐴 = {𝑥, 𝑦, 𝑧}) | ||
| Theorem | en4 9317* | A set equinumerous to ordinal 4 is a quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
| ⊢ (𝐴 ≈ 4o → ∃𝑥∃𝑦∃𝑧∃𝑤 𝐴 = ({𝑥, 𝑦} ∪ {𝑧, 𝑤})) | ||
| Theorem | findcard3 9318* | 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.) Avoid ax-pow 5365. (Revised by BTernaryTau, 7-Jan-2025.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝑦 ∈ Fin → (∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒)) ⇒ ⊢ (𝐴 ∈ Fin → 𝜏) | ||
| Theorem | findcard3OLD 9319* | Obsolete version of findcard3 9318 as of 7-Jan-2025. (Contributed by Mario Carneiro, 13-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝑦 ∈ Fin → (∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒)) ⇒ ⊢ (𝐴 ∈ Fin → 𝜏) | ||
| Theorem | ac6sfi 9320* | A version of ac6s 10524 for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
| ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
| Theorem | frfi 9321 | 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 9322* | 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 9323* | 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 9324* | Lemma showing existence and closure of supremum of a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))) | ||
| Theorem | wofi 9325 | 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 9326 | 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 9327 | 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 9328* | Lemma for unbnn 9332. 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 9329* | Lemma for unbnn 9332. The value of the function 𝐹 belongs to the unbounded set of natural numbers 𝐴. (Contributed by NM, 3-Dec-2003.) |
| ⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω) ⇒ ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ 𝐴)) | ||
| Theorem | unblem3 9330* | Lemma for unbnn 9332. 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 9331* | Lemma for unbnn 9332. 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 9332* | 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 9699 for a stronger version without the first assumption. (Contributed by NM, 3-Dec-2003.) |
| ⊢ ((ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → 𝐴 ≈ ω) | ||
| Theorem | unbnn2 9333* | Version of unbnn 9332 that does not require a strict upper bound. (Contributed by NM, 24-Apr-2004.) |
| ⊢ ((ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) → 𝐴 ≈ ω) | ||
| Theorem | isfinite2 9334 | 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 9335 | Omega strictly dominates a natural number. Example 3 of [Enderton] p. 146. In order to avoid the Axiom of Infinity, we include it as part of the antecedent. See nnsdom 9694 for the version without this sethood requirement. (Contributed by NM, 15-Jun-1998.) Avoid ax-pow 5365. (Revised by BTernaryTau, 7-Jan-2025.) |
| ⊢ ((ω ∈ V ∧ 𝐴 ∈ ω) → 𝐴 ≺ ω) | ||
| Theorem | nnsdomgOLD 9336 | Obsolete version of nnsdomg 9335 as of 7-Jan-2025. (Contributed by NM, 15-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((ω ∈ V ∧ 𝐴 ∈ ω) → 𝐴 ≺ ω) | ||
| Theorem | isfiniteg 9337 | 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 9338 | An infinite set strictly dominates a natural number. (Contributed by NM, 22-Nov-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) Avoid ax-pow 5365. (Revised by BTernaryTau, 7-Jan-2025.) |
| ⊢ ((ω ≼ 𝐴 ∧ 𝐵 ∈ ω) → 𝐵 ≺ 𝐴) | ||
| Theorem | infsdomnnOLD 9339 | Obsolete version of infsdomnn 9338 as of 7-Jan-2025. (Contributed by NM, 22-Nov-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((ω ≼ 𝐴 ∧ 𝐵 ∈ ω) → 𝐵 ≺ 𝐴) | ||
| Theorem | infn0 9340 | An infinite set is not empty. For a shorter proof using ax-un 7755, see infn0ALT 9341. (Contributed by NM, 23-Oct-2004.) Avoid ax-un 7755. (Revised by BTernaryTau, 8-Jan-2025.) |
| ⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅) | ||
| Theorem | infn0ALT 9341 | Shorter proof of infn0 9340 using ax-un 7755. (Contributed by NM, 23-Oct-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅) | ||
| Theorem | fin2inf 9342 | 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 9343* | 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 9344* | 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 9345 | 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 | unfir 9346 | If a union is finite, the operands are finite. Converse of unfi 9211. (Contributed by FL, 3-Aug-2009.) |
| ⊢ ((𝐴 ∪ 𝐵) ∈ Fin → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) | ||
| Theorem | unfib 9347 | A union is finite if and only if the operands are finite. (Contributed by AV, 10-May-2025.) |
| ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) | ||
| Theorem | unfi2 9348 | The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. This version of unfi 9211 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 9342). (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) |
| ⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 ∪ 𝐵) ≺ ω) | ||
| Theorem | difinf 9349 | An infinite set 𝐴 minus a finite set is infinite. (Contributed by FL, 3-Aug-2009.) |
| ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ¬ (𝐴 ∖ 𝐵) ∈ Fin) | ||
| Theorem | fodomfi 9350 | An onto function implies dominance of domain over range, for finite sets. Unlike fodomg 10562 for arbitrary sets, this theorem does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2014.) Avoid ax-pow 5365. (Revised by BTernaryTau, 20-Jun-2025.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴) | ||
| Theorem | fofi 9351 | If an onto function has a finite domain, its codomain/range is finite. Theorem 37 of [Suppes] p. 104. (Contributed by NM, 25-Mar-2007.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ Fin) | ||
| Theorem | f1fi 9352 | 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 | imafi 9353 | Images of finite sets are finite. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
| ⊢ ((Fun 𝐹 ∧ 𝑋 ∈ Fin) → (𝐹 “ 𝑋) ∈ Fin) | ||
| Theorem | imafiOLD 9354 | Obsolete version of imafi 9353 as of 25-Jun-2025. (Contributed by Stefan O'Rear, 22-Feb-2015.) Avoid ax-pow 5365. (Revised by BTernaryTau, 7-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((Fun 𝐹 ∧ 𝑋 ∈ Fin) → (𝐹 “ 𝑋) ∈ Fin) | ||
| Theorem | pwfir 9355 | If the power set of a set is finite, then the set itself is finite. (Contributed by BTernaryTau, 7-Sep-2024.) |
| ⊢ (𝒫 𝐵 ∈ Fin → 𝐵 ∈ Fin) | ||
| Theorem | pwfilem 9356* | Lemma for pwfi 9357. (Contributed by NM, 26-Mar-2007.) Avoid ax-pow 5365. (Revised by BTernaryTau, 7-Sep-2024.) |
| ⊢ 𝐹 = (𝑐 ∈ 𝒫 𝑏 ↦ (𝑐 ∪ {𝑥})) ⇒ ⊢ (𝒫 𝑏 ∈ Fin → 𝒫 (𝑏 ∪ {𝑥}) ∈ Fin) | ||
| Theorem | pwfi 9357 | The power set of a finite set is finite and vice-versa. Theorem 38 of [Suppes] p. 104 and its converse, Theorem 40 of [Suppes] p. 105. (Contributed by NM, 26-Mar-2007.) Avoid ax-pow 5365. (Revised by BTernaryTau, 7-Sep-2024.) |
| ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin) | ||
| Theorem | xpfi 9358 | The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5365. (Revised by BTernaryTau, 10-Jan-2025.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin) | ||
| Theorem | xpfiOLD 9359 | Obsolete version of xpfi 9358 as of 10-Jan-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin) | ||
| Theorem | 3xpfi 9360 | The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
| ⊢ (𝑉 ∈ Fin → ((𝑉 × 𝑉) × 𝑉) ∈ Fin) | ||
| Theorem | domunfican 9361 | 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 9362* | 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 9363 | An unordered pair is finite. For a shorter proof using ax-un 7755, see prfiALT 9364. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2157, ax-un 7755. (Revised by BTernaryTau, 13-Jan-2025.) |
| ⊢ {𝐴, 𝐵} ∈ Fin | ||
| Theorem | prfiALT 9364 | Shorter proof of prfi 9363 using ax-un 7755. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ {𝐴, 𝐵} ∈ Fin | ||
| Theorem | tpfi 9365 | An unordered triple is finite. (Contributed by Mario Carneiro, 28-Sep-2013.) |
| ⊢ {𝐴, 𝐵, 𝐶} ∈ Fin | ||
| Theorem | fiint 9366* | 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.) Use a separate setvar for the right-hand side and avoid ax-pow 5365. (Revised by BTernaryTau, 14-Jan-2025.) |
| ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴)) | ||
| Theorem | fiintOLD 9367* | Obsolete version of fiint 9366 as of 14-Jan-2025. (Contributed by NM, 22-Sep-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴)) | ||
| Theorem | fodomfir 9368* | There exists a mapping from a finite set onto any nonempty set that it dominates, proved without using the Axiom of Power Sets (unlike fodomr 9168). (Contributed by BTernaryTau, 23-Jun-2025.) |
| ⊢ ((𝐴 ∈ Fin ∧ ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵) | ||
| Theorem | fodomfib 9369* | Equivalence of an onto mapping and dominance for a nonempty finite set. Unlike fodomb 10566 for arbitrary sets, this theorem does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.) Avoid ax-pow 5365. (Revised by BTernaryTau, 23-Jun-2025.) |
| ⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) | ||
| Theorem | fodomfiOLD 9370 | Obsolete version of fodomfi 9350 as of 20-Jun-2025. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴) | ||
| Theorem | fodomfibOLD 9371* | Obsolete version of fodomfib 9369 as of 23-Jun-2025. (Contributed by NM, 23-Mar-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴))) | ||
| Theorem | fofinf1o 9372 | 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 9373 | 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 9374 | Any finite set dominates its domain. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
| ⊢ (𝐹 ∈ Fin → dom 𝐹 ≼ 𝐹) | ||
| Theorem | dmfi 9375 | The domain of a finite set is finite. (Contributed by Mario Carneiro, 24-Sep-2013.) |
| ⊢ (𝐴 ∈ Fin → dom 𝐴 ∈ Fin) | ||
| Theorem | fundmfibi 9376 | A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.) |
| ⊢ (Fun 𝐹 → (𝐹 ∈ Fin ↔ dom 𝐹 ∈ Fin)) | ||
| Theorem | resfnfinfin 9377 | 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 9378 | A restricted identity function is finite iff the restricting class is finite. (Contributed by AV, 10-Jan-2020.) |
| ⊢ (( I ↾ 𝐴) ∈ Fin ↔ 𝐴 ∈ Fin) | ||
| Theorem | cnvfiALT 9379 | Shorter proof of cnvfi 9216 using ax-pow 5365. (Contributed by Mario Carneiro, 28-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Fin → ◡𝐴 ∈ Fin) | ||
| Theorem | rnfi 9380 | The range of a finite set is finite. (Contributed by Mario Carneiro, 28-Dec-2014.) |
| ⊢ (𝐴 ∈ Fin → ran 𝐴 ∈ Fin) | ||
| Theorem | f1dmvrnfibi 9381 | A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 9382. (Contributed by AV, 10-Jan-2020.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin)) | ||
| Theorem | f1vrnfibi 9382 | A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 9381. (Contributed by AV, 10-Jan-2020.) |
| ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin)) | ||
| Theorem | iunfi 9383* | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 9384. 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 9384 | 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 9385* | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This version of unifi 9384 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 9342). (Contributed by NM, 11-Mar-2006.) |
| ⊢ ((𝐴 ≺ ω ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ ω) → ∪ 𝐴 ≺ ω) | ||
| Theorem | infssuni 9386* | 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 9387 | 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) | ||
| Theorem | mapfi 9388 | Set exponentiation of finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ↑m 𝐵) ∈ Fin) | ||
| Theorem | ixpfi 9389* | A Cartesian product of finitely many finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.) |
| ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin) → X𝑥 ∈ 𝐴 𝐵 ∈ Fin) | ||
| Theorem | ixpfi2 9390* | A Cartesian product of finite sets such that all but finitely many are singletons is finite. (Note that 𝐵(𝑥) and 𝐷(𝑥) are both possibly dependent on 𝑥.) (Contributed by Mario Carneiro, 25-Jan-2015.) |
| ⊢ (𝜑 → 𝐶 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → 𝐵 ⊆ {𝐷}) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ∈ Fin) | ||
| Theorem | mptfi 9391* | A finite mapping set is finite. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (𝐴 ∈ Fin → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ Fin) | ||
| Theorem | abrexfi 9392* | An image set from a finite set is finite. (Contributed by Mario Carneiro, 13-Feb-2014.) |
| ⊢ (𝐴 ∈ Fin → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ Fin) | ||
| Theorem | cnvimamptfin 9393* | A preimage of a mapping with a finite domain under any class is finite. In contrast to fisuppfi 9411, the range of the mapping needs not to be known. (Contributed by AV, 21-Dec-2018.) |
| ⊢ (𝜑 → 𝑁 ∈ Fin) ⇒ ⊢ (𝜑 → (◡(𝑝 ∈ 𝑁 ↦ 𝑋) “ 𝑌) ∈ Fin) | ||
| Theorem | elfpw 9394 | Membership in a class of finite subsets. (Contributed by Stefan O'Rear, 4-Apr-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
| ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin)) | ||
| Theorem | unifpw 9395 | A set is the union of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ ∪ (𝒫 𝐴 ∩ Fin) = 𝐴 | ||
| Theorem | f1opwfi 9396* | A one-to-one mapping induces a one-to-one mapping on finite subsets. (Contributed by Mario Carneiro, 25-Jan-2015.) |
| ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐹 “ 𝑏)):(𝒫 𝐴 ∩ Fin)–1-1-onto→(𝒫 𝐵 ∩ Fin)) | ||
| Theorem | fissuni 9397* | A finite subset of a union is covered by finitely many elements. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ ((𝐴 ⊆ ∪ 𝐵 ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)𝐴 ⊆ ∪ 𝑐) | ||
| Theorem | fipreima 9398* | Given a finite subset 𝐴 of the range of a function, there exists a finite subset of the domain whose image is 𝐴. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 22-Feb-2015.) |
| ⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)(𝐹 “ 𝑐) = 𝐴) | ||
| Theorem | finsschain 9399* | A finite subset of the union of a superset chain is a subset of some element of the chain. A useful preliminary result for alexsub 24053 and others. (Contributed by Jeff Hankins, 25-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Feb-2015.) (Revised by Mario Carneiro, 18-May-2015.) |
| ⊢ (((𝐴 ≠ ∅ ∧ [⊊] Or 𝐴) ∧ (𝐵 ∈ Fin ∧ 𝐵 ⊆ ∪ 𝐴)) → ∃𝑧 ∈ 𝐴 𝐵 ⊆ 𝑧) | ||
| Theorem | indexfi 9400* | If for every element of a finite indexing set 𝐴 there exists a corresponding element of another set 𝐵, then there exists a finite subset of 𝐵 consisting only of those elements which are indexed by 𝐴. Proven without the Axiom of Choice, unlike indexdom 37741. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐 ∈ Fin (𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |