| Metamath
Proof Explorer Theorem List (p. 93 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 | dif1ennn 9201 | If a set 𝐴 is equinumerous to the successor of a natural number 𝑀, then 𝐴 with an element removed is equinumerous to 𝑀. See also dif1ennnALT 9311. (Contributed by BTernaryTau, 6-Jan-2025.) |
| ⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀) | ||
| Theorem | dif1enOLD 9202 | Obsolete version of dif1en 9200 as of 6-Jan-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid ax-pow 5365. (Revised by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀) | ||
| Theorem | findcard 9203* | 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 9204* | 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.) Avoid ax-pow 5365. (Revised by BTernaryTau, 26-Aug-2024.) |
| ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ Fin → 𝜏) | ||
| Theorem | findcard2s 9205* | Variation of findcard2 9204 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 9206* | Deduction version of findcard2 9204. (Contributed by SO, 16-Jul-2018.) |
| ⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝜃 → 𝜏)) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → 𝜂) | ||
| Theorem | nnfi 9207 | Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) Avoid ax-pow 5365. (Revised by BTernaryTau, 23-Sep-2024.) |
| ⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin) | ||
| Theorem | pssnn 9208* | 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.) Avoid ax-pow 5365. (Revised by BTernaryTau, 31-Jul-2024.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥) | ||
| Theorem | ssnnfi 9209 | A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998.) (Proof shortened by BTernaryTau, 23-Sep-2024.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
| Theorem | 0finOLD 9210 | Obsolete version of 0fi 9082 as of 13-Jan-2025. (Contributed by FL, 14-Jul-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ∅ ∈ Fin | ||
| Theorem | unfi 9211 | The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 16-Nov-2002.) Avoid ax-pow 5365. (Revised by BTernaryTau, 7-Aug-2024.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin) | ||
| Theorem | unfid 9212 | The union of two finite sets is finite. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ Fin) | ||
| Theorem | ssfi 9213 | A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5365, see ssfiALT 9214. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5365. (Revised by BTernaryTau, 12-Aug-2024.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
| Theorem | ssfiALT 9214 | Shorter proof of ssfi 9213 using ax-pow 5365. (Contributed by NM, 24-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
| Theorem | diffi 9215 | If 𝐴 is finite, (𝐴 ∖ 𝐵) is finite. (Contributed by FL, 3-Aug-2009.) |
| ⊢ (𝐴 ∈ Fin → (𝐴 ∖ 𝐵) ∈ Fin) | ||
| Theorem | cnvfi 9216 | If a set is finite, its converse is as well. (Contributed by Mario Carneiro, 28-Dec-2014.) Avoid ax-pow 5365. (Revised by BTernaryTau, 9-Sep-2024.) |
| ⊢ (𝐴 ∈ Fin → ◡𝐴 ∈ Fin) | ||
| Theorem | pwssfi 9217 | Every element of the power set of 𝐴 is finite if and only if 𝐴 is finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ 𝒫 𝐴 ⊆ Fin)) | ||
| Theorem | fnfi 9218 | A version of fnex 7237 for finite sets that does not require Replacement or Power Sets. (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin) → 𝐹 ∈ Fin) | ||
| Theorem | f1oenfi 9219 | If the domain of a one-to-one, onto function is finite, then the domain and range of the function are equinumerous. This theorem is proved without using the Axiom of Replacement or the Axiom of Power Sets (unlike f1oeng 9011). (Contributed by BTernaryTau, 8-Sep-2024.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) | ||
| Theorem | f1oenfirn 9220 | If the range of a one-to-one, onto function is finite, then the domain and range of the function are equinumerous. (Contributed by BTernaryTau, 9-Sep-2024.) |
| ⊢ ((𝐵 ∈ Fin ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) | ||
| Theorem | f1domfi 9221 | If the codomain of a one-to-one function is finite, then the function's domain is dominated by its codomain. This theorem is proved without using the Axiom of Replacement or the Axiom of Power Sets (unlike f1domg 9012). (Contributed by BTernaryTau, 25-Sep-2024.) |
| ⊢ ((𝐵 ∈ Fin ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | ||
| Theorem | f1domfi2 9222 | If the domain of a one-to-one function is finite, then the function's domain is dominated by its codomain when the latter is a set. This theorem is proved without using the Axiom of Power Sets (unlike f1dom2g 9010). (Contributed by BTernaryTau, 24-Nov-2024.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | ||
| Theorem | enreffi 9223 | Equinumerosity is reflexive for finite sets, proved without using the Axiom of Power Sets (unlike enrefg 9024). (Contributed by BTernaryTau, 8-Sep-2024.) |
| ⊢ (𝐴 ∈ Fin → 𝐴 ≈ 𝐴) | ||
| Theorem | ensymfib 9224 | Symmetry of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike ensymb 9042). (Contributed by BTernaryTau, 9-Sep-2024.) |
| ⊢ (𝐴 ∈ Fin → (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴)) | ||
| Theorem | entrfil 9225 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 9046). (Contributed by BTernaryTau, 10-Sep-2024.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) | ||
| Theorem | enfii 9226 | A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5365. (Revised by BTernaryTau, 23-Sep-2024.) |
| ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin) | ||
| Theorem | enfi 9227 | Equinumerous sets have the same finiteness. For a shorter proof using ax-pow 5365, see enfiALT 9228. (Contributed by NM, 22-Aug-2008.) Avoid ax-pow 5365. (Revised by BTernaryTau, 23-Sep-2024.) |
| ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin)) | ||
| Theorem | enfiALT 9228 | Shorter proof of enfi 9227 using ax-pow 5365. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin)) | ||
| Theorem | domfi 9229 | 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 | entrfi 9230 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 9046). (Contributed by BTernaryTau, 23-Sep-2024.) |
| ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) | ||
| Theorem | entrfir 9231 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 9046). (Contributed by BTernaryTau, 23-Sep-2024.) |
| ⊢ ((𝐶 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) | ||
| Theorem | domtrfil 9232 | Transitivity of dominance relation when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike domtr 9047). (Contributed by BTernaryTau, 24-Nov-2024.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | ||
| Theorem | domtrfi 9233 | Transitivity of dominance relation when 𝐵 is finite, proved without using the Axiom of Power Sets (unlike domtr 9047). (Contributed by BTernaryTau, 24-Nov-2024.) |
| ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | ||
| Theorem | domtrfir 9234 | Transitivity of dominance relation for finite sets, proved without using the Axiom of Power Sets (unlike domtr 9047). (Contributed by BTernaryTau, 24-Nov-2024.) |
| ⊢ ((𝐶 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | ||
| Theorem | f1imaenfi 9235 | If a function is one-to-one, then the image of a finite subset of its domain under it is equinumerous to the subset. This theorem is proved without using the Axiom of Replacement or the Axiom of Power Sets (unlike f1imaeng 9054). (Contributed by BTernaryTau, 29-Sep-2024.) |
| ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ Fin) → (𝐹 “ 𝐶) ≈ 𝐶) | ||
| Theorem | ssdomfi 9236 | A finite set dominates its subsets, proved without using the Axiom of Power Sets (unlike ssdomg 9040). (Contributed by BTernaryTau, 12-Nov-2024.) |
| ⊢ (𝐵 ∈ Fin → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵)) | ||
| Theorem | ssdomfi2 9237 | A set dominates its finite subsets, proved without using the Axiom of Power Sets (unlike ssdomg 9040). (Contributed by BTernaryTau, 24-Nov-2024.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → 𝐴 ≼ 𝐵) | ||
| Theorem | sbthfilem 9238* | Lemma for sbthfi 9239. (Contributed by BTernaryTau, 4-Nov-2024.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) | ||
| Theorem | sbthfi 9239 | Schroeder-Bernstein Theorem for finite sets, proved without using the Axiom of Power Sets (unlike sbth 9133). (Contributed by BTernaryTau, 4-Nov-2024.) |
| ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) | ||
| Theorem | domnsymfi 9240 | If a set dominates a finite set, it cannot also be strictly dominated by the finite set. This theorem is proved without using the Axiom of Power Sets (unlike domnsym 9139). (Contributed by BTernaryTau, 22-Nov-2024.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵) → ¬ 𝐵 ≺ 𝐴) | ||
| Theorem | sdomdomtrfi 9241 | Transitivity of strict dominance and dominance when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike sdomdomtr 9150). (Contributed by BTernaryTau, 25-Nov-2024.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≺ 𝐶) | ||
| Theorem | domsdomtrfi 9242 | Transitivity of dominance and strict dominance when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike domsdomtr 9152). (Contributed by BTernaryTau, 25-Nov-2024.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝐶) → 𝐴 ≺ 𝐶) | ||
| Theorem | sucdom2 9243 | 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.) Avoid ax-pow 5365. (Revised by BTernaryTau, 4-Dec-2024.) |
| ⊢ (𝐴 ≺ 𝐵 → suc 𝐴 ≼ 𝐵) | ||
| Theorem | phplem1 9244 | Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus any element of the successor. (Contributed by NM, 26-May-1998.) Avoid ax-pow 5365. (Revised by BTernaryTau, 23-Sep-2024.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) | ||
| Theorem | phplem2 9245 | 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.) Avoid ax-pow 5365. (Revised by BTernaryTau, 4-Nov-2024.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵)) | ||
| Theorem | nneneq 9246 | 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.) Avoid ax-pow 5365. (Revised by BTernaryTau, 11-Nov-2024.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) | ||
| Theorem | php 9247 | 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 phplem1 9244, phplem2 9245, nneneq 9246, and this final piece of the proof. (Contributed by NM, 29-May-1998.) Avoid ax-pow 5365. (Revised by BTernaryTau, 18-Nov-2024.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵) | ||
| Theorem | php2 9248 | Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998.) Avoid ax-pow 5365. (Revised by BTernaryTau, 20-Nov-2024.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
| Theorem | php3 9249 | 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.) Avoid ax-pow 5365. (Revised by BTernaryTau, 26-Nov-2024.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
| Theorem | php4 9250 | Corollary of the Pigeonhole Principle php 9247: a natural number is strictly dominated by its successor. (Contributed by NM, 26-Jul-2004.) |
| ⊢ (𝐴 ∈ ω → 𝐴 ≺ suc 𝐴) | ||
| Theorem | php5 9251 | Corollary of the Pigeonhole Principle php 9247: 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 9252 | Corollary of the Pigeonhole Principle using equality. Strengthening of php 9247 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-pow 5365. (Revised by BTernaryTau, 28-Nov-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| Theorem | nndomog 9253 | Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 9269 when both are natural numbers. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9269. (Revised by RP, 5-Nov-2023.) Avoid ax-pow 5365. (Revised by BTernaryTau, 29-Nov-2024.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
| Theorem | phplem1OLD 9254 | Obsolete lemma for php 9247 as of 22-Nov-2024. (Contributed by NM, 25-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ({𝐴} ∪ (𝐴 ∖ {𝐵})) = (suc 𝐴 ∖ {𝐵})) | ||
| Theorem | phplem2OLD 9255 | Obsolete lemma for php 9247 as of 22-Nov-2024. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) | ||
| Theorem | phplem3OLD 9256 | Obsolete version of phplem1 9244 as of 4-Nov-2024. (Contributed by NM, 26-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) | ||
| Theorem | phplem4OLD 9257 | Obsolete version of phplem2 9245 as of 4-Nov-2024. (Contributed by NM, 28-May-1998.) (Revised by Mario Carneiro, 24-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵)) | ||
| Theorem | nneneqOLD 9258 | Obsolete version of nneneq 9246 as of 11-Nov-2024. (Contributed by NM, 28-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) | ||
| Theorem | phpOLD 9259 | Obsolete version of php 9247 as of 18-Nov-2024. (Contributed by NM, 29-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵) | ||
| Theorem | php2OLD 9260 | Obsolete version of php2 9248 as of 20-Nov-2024. (Contributed by NM, 31-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
| Theorem | php3OLD 9261 | Obsolete version of php3 9249 as of 26-Nov-2024. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
| Theorem | phpeqdOLD 9262 | Obsolete version of phpeqd 9252 as of 28-Nov-2024. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| Theorem | nndomogOLD 9263 | Obsolete version of nndomog 9253 as of 29-Nov-2024. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9269. (Revised by RP, 5-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
| Theorem | snnen2oOLD 9264 | Obsolete version of snnen2o 9273 as of 18-Nov-2024. (Contributed by AV, 6-Aug-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ¬ {𝐴} ≈ 2o | ||
| Theorem | onomeneq 9265 | 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.) Avoid ax-pow 5365. (Revised by BTernaryTau, 2-Dec-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) | ||
| Theorem | onomeneqOLD 9266 | Obsolete version of onomeneq 9265 as of 29-Nov-2024. (Contributed by NM, 26-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) | ||
| Theorem | onfin 9267 | 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 9268 | A set is a natural number iff it is a finite ordinal. (Contributed by Mario Carneiro, 22-Jan-2013.) |
| ⊢ ω = (On ∩ Fin) | ||
| Theorem | nndomo 9269 | Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146. (Contributed by NM, 17-Jun-1998.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
| Theorem | nnsdomo 9270 | Cardinal ordering agrees with natural number ordering. (Contributed by NM, 17-Jun-1998.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≺ 𝐵 ↔ 𝐴 ⊊ 𝐵)) | ||
| Theorem | sucdom 9271 | Strict dominance of a set over a natural number is the same as dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013.) Avoid ax-pow 5365. (Revised by BTernaryTau, 4-Dec-2024.) (Proof shortened by BJ, 11-Jan-2025.) |
| ⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵)) | ||
| Theorem | sucdomOLD 9272 | Obsolete version of sucdom 9271 as of 4-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵)) | ||
| Theorem | snnen2o 9273 | 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.) Avoid ax-pow 5365, ax-un 7755. (Revised by BTernaryTau, 1-Dec-2024.) |
| ⊢ ¬ {𝐴} ≈ 2o | ||
| Theorem | 0sdom1dom 9274 | Strict dominance over 0 is the same as dominance over 1. For a shorter proof requiring ax-un 7755, see 0sdom1domALT . (Contributed by NM, 28-Sep-2004.) Avoid ax-un 7755. (Revised by BTernaryTau, 7-Dec-2024.) |
| ⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴) | ||
| Theorem | 0sdom1domALT 9275 | Alternate proof of 0sdom1dom 9274, shorter but requiring ax-un 7755. (Contributed by NM, 28-Sep-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴) | ||
| Theorem | 1sdom2 9276 | Ordinal 1 is strictly dominated by ordinal 2. For a shorter proof requiring ax-un 7755, see 1sdom2ALT 9277. (Contributed by NM, 4-Apr-2007.) Avoid ax-un 7755. (Revised by BTernaryTau, 8-Dec-2024.) |
| ⊢ 1o ≺ 2o | ||
| Theorem | 1sdom2ALT 9277 | Alternate proof of 1sdom2 9276, shorter but requiring ax-un 7755. (Contributed by NM, 4-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 1o ≺ 2o | ||
| Theorem | sdom1 9278 | A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014.) Avoid ax-pow 5365, ax-un 7755. (Revised by BTernaryTau, 12-Dec-2024.) |
| ⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅) | ||
| Theorem | sdom1OLD 9279 | Obsolete version of sdom1 9278 as of 12-Dec-2024. (Contributed by Stefan O'Rear, 28-Oct-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅) | ||
| Theorem | modom 9280 | Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
| ⊢ (∃*𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≼ 1o) | ||
| Theorem | modom2 9281* | Two ways to express "at most one". (Contributed by Mario Carneiro, 24-Dec-2016.) |
| ⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 ≼ 1o) | ||
| Theorem | rex2dom 9282* | A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦) → 2o ≼ 𝐴) | ||
| Theorem | 1sdom2dom 9283 | Strict dominance over 1 is the same as dominance over 2. (Contributed by BTernaryTau, 23-Dec-2024.) |
| ⊢ (1o ≺ 𝐴 ↔ 2o ≼ 𝐴) | ||
| Theorem | 1sdom 9284* | A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom 9070.) (Contributed by Mario Carneiro, 12-Jan-2013.) Avoid ax-un 7755. (Revised by BTernaryTau, 30-Dec-2024.) |
| ⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) | ||
| Theorem | 1sdomOLD 9285* | Obsolete version of 1sdom 9284 as of 30-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) | ||
| Theorem | unxpdomlem1 9286* | Lemma for unxpdom 9289. (Trivial substitution proof.) (Contributed by Mario Carneiro, 13-Jan-2013.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) ⇒ ⊢ (𝑧 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉)) | ||
| Theorem | unxpdomlem2 9287* | Lemma for unxpdom 9289. (Contributed by Mario Carneiro, 13-Jan-2013.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) & ⊢ (𝜑 → 𝑤 ∈ (𝑎 ∪ 𝑏)) & ⊢ (𝜑 → ¬ 𝑚 = 𝑛) & ⊢ (𝜑 → ¬ 𝑠 = 𝑡) ⇒ ⊢ ((𝜑 ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) | ||
| Theorem | unxpdomlem3 9288* | Lemma for unxpdom 9289. (Contributed by Mario Carneiro, 13-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) ⇒ ⊢ ((1o ≺ 𝑎 ∧ 1o ≺ 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)) | ||
| Theorem | unxpdom 9289 | 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 9290 | Corollary of unxpdom 9289. (Contributed by NM, 16-Sep-2004.) |
| ⊢ ((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴)) | ||
| Theorem | sucxpdom 9291 | 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 9292 | 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 9293 | A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.) |
| ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵) | ||
| Theorem | ominf 9294 | The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.) Avoid ax-pow 5365. (Revised by BTernaryTau, 2-Jan-2025.) |
| ⊢ ¬ ω ∈ Fin | ||
| Theorem | ominfOLD 9295 | Obsolete version of ominf 9294 as of 2-Jan-2025. (Contributed by NM, 2-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ¬ ω ∈ Fin | ||
| Theorem | isinf 9296* | 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.) Avoid ax-pow 5365. (Revised by BTernaryTau, 2-Jan-2025.) |
| ⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)) | ||
| Theorem | isinfOLD 9297* | Obsolete version of isinf 9296 as of 2-Jan-2025. (Contributed by Mario Carneiro, 15-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)) | ||
| Theorem | fineqvlem 9298 | Lemma for fineqv 9299. (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 9299 | 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 | xpfir 9300 | 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)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |