![]() |
Metamath
Proof Explorer Theorem List (p. 92 of 474) | < 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-29923) |
![]() (29924-31446) |
![]() (31447-47372) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pwen 9101 | If two sets are equinumerous, then their power sets are equinumerous. Proposition 10.15 of [TakeutiZaring] p. 87. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 9-Apr-2015.) |
⊢ (𝐴 ≈ 𝐵 → 𝒫 𝐴 ≈ 𝒫 𝐵) | ||
Theorem | ssenen 9102* | Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐴 ≈ 𝐵 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐶)} ≈ {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝑥 ≈ 𝐶)}) | ||
Theorem | limenpsi 9103 | A limit ordinal is equinumerous to a proper subset of itself. (Contributed by NM, 30-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ Lim 𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ (𝐴 ∖ {∅})) | ||
Theorem | limensuci 9104 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
⊢ Lim 𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ suc 𝐴) | ||
Theorem | limensuc 9105 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ≈ suc 𝐴) | ||
Theorem | infensuc 9106 | Any infinite ordinal is equinumerous to its successor. Exercise 7 of [TakeutiZaring] p. 88. Proved without the Axiom of Infinity. (Contributed by NM, 30-Oct-2003.) (Revised by Mario Carneiro, 13-Jan-2013.) |
⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → 𝐴 ≈ suc 𝐴) | ||
Theorem | dif1enlem 9107 | Lemma for rexdif1en 9109 and dif1en 9111. (Contributed by BTernaryTau, 18-Aug-2024.) Generalize to all ordinals and add a sethood requirement to avoid ax-un 7677. (Revised by BTernaryTau, 5-Jan-2025.) |
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝑀 ∈ On) ∧ 𝐹:𝐴–1-1-onto→suc 𝑀) → (𝐴 ∖ {(◡𝐹‘𝑀)}) ≈ 𝑀) | ||
Theorem | dif1enlemOLD 9108 | Obsolete version of dif1enlem 9107 as of 5-Jan-2025. (Contributed by BTernaryTau, 18-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑀 ∈ ω ∧ 𝐹:𝐴–1-1-onto→suc 𝑀) → (𝐴 ∖ {(◡𝐹‘𝑀)}) ≈ 𝑀) | ||
Theorem | rexdif1en 9109* | If a set is equinumerous to a nonzero ordinal, then there exists an element in that set such that removing it leaves the set equinumerous to the predecessor of that ordinal. (Contributed by BTernaryTau, 26-Aug-2024.) Generalize to all ordinals and avoid ax-un 7677. (Revised by BTernaryTau, 5-Jan-2025.) |
⊢ ((𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀) → ∃𝑥 ∈ 𝐴 (𝐴 ∖ {𝑥}) ≈ 𝑀) | ||
Theorem | rexdif1enOLD 9110* | Obsolete version of rexdif1en 9109 as of 5-Jan-2025. (Contributed by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀) → ∃𝑥 ∈ 𝐴 (𝐴 ∖ {𝑥}) ≈ 𝑀) | ||
Theorem | dif1en 9111 | If a set 𝐴 is equinumerous to the successor of an ordinal 𝑀, then 𝐴 with an element removed is equinumerous to 𝑀. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid ax-pow 5325. (Revised by BTernaryTau, 26-Aug-2024.) Generalize to all ordinals. (Revised by BTernaryTau, 6-Jan-2025.) |
⊢ ((𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀) | ||
Theorem | dif1ennn 9112 | If a set 𝐴 is equinumerous to the successor of a natural number 𝑀, then 𝐴 with an element removed is equinumerous to 𝑀. See also dif1ennnALT 9228. (Contributed by BTernaryTau, 6-Jan-2025.) |
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀) | ||
Theorem | dif1enOLD 9113 | Obsolete version of dif1en 9111 as of 6-Jan-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid ax-pow 5325. (Revised by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀) | ||
Theorem | findcard 9114* | 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 9115* | 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 5325. (Revised by BTernaryTau, 26-Aug-2024.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ Fin → 𝜏) | ||
Theorem | findcard2s 9116* | Variation of findcard2 9115 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 9117* | Deduction version of findcard2 9115. (Contributed by SO, 16-Jul-2018.) |
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝜃 → 𝜏)) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | nnfi 9118 | Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) Avoid ax-pow 5325. (Revised by BTernaryTau, 23-Sep-2024.) |
⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin) | ||
Theorem | pssnn 9119* | 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 5325. (Revised by BTernaryTau, 31-Jul-2024.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥) | ||
Theorem | ssnnfi 9120 | A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998.) (Proof shortened by BTernaryTau, 23-Sep-2024.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
Theorem | ssnnfiOLD 9121 | Obsolete version of ssnnfi 9120 as of 23-Sep-2024. (Contributed by NM, 24-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
Theorem | 0fin 9122 | The empty set is finite. (Contributed by FL, 14-Jul-2008.) |
⊢ ∅ ∈ Fin | ||
Theorem | unfi 9123 | 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 5325. (Revised by BTernaryTau, 7-Aug-2024.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin) | ||
Theorem | ssfi 9124 | A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. For a shorter proof using ax-pow 5325, see ssfiALT 9125. (Contributed by NM, 24-Jun-1998.) Avoid ax-pow 5325. (Revised by BTernaryTau, 12-Aug-2024.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
Theorem | ssfiALT 9125 | Shorter proof of ssfi 9124 using ax-pow 5325. (Contributed by NM, 24-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
Theorem | imafi 9126 | Images of finite sets are finite. For a shorter proof using ax-pow 5325, see imafiALT 9296. (Contributed by Stefan O'Rear, 22-Feb-2015.) Avoid ax-pow 5325. (Revised by BTernaryTau, 7-Sep-2024.) |
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ Fin) → (𝐹 “ 𝑋) ∈ Fin) | ||
Theorem | pwfir 9127 | 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 9128* | Lemma for pwfi 9129. (Contributed by NM, 26-Mar-2007.) Avoid ax-pow 5325. (Revised by BTernaryTau, 7-Sep-2024.) |
⊢ 𝐹 = (𝑐 ∈ 𝒫 𝑏 ↦ (𝑐 ∪ {𝑥})) ⇒ ⊢ (𝒫 𝑏 ∈ Fin → 𝒫 (𝑏 ∪ {𝑥}) ∈ Fin) | ||
Theorem | pwfi 9129 | 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 5325. (Revised by BTernaryTau, 7-Sep-2024.) |
⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin) | ||
Theorem | diffi 9130 | If 𝐴 is finite, (𝐴 ∖ 𝐵) is finite. (Contributed by FL, 3-Aug-2009.) |
⊢ (𝐴 ∈ Fin → (𝐴 ∖ 𝐵) ∈ Fin) | ||
Theorem | cnvfi 9131 | If a set is finite, its converse is as well. (Contributed by Mario Carneiro, 28-Dec-2014.) Avoid ax-pow 5325. (Revised by BTernaryTau, 9-Sep-2024.) |
⊢ (𝐴 ∈ Fin → ◡𝐴 ∈ Fin) | ||
Theorem | fnfi 9132 | A version of fnex 7172 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 9133 | 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 8918). (Contributed by BTernaryTau, 8-Sep-2024.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) | ||
Theorem | f1oenfirn 9134 | 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 9135 | 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 8919). (Contributed by BTernaryTau, 25-Sep-2024.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | ||
Theorem | f1domfi2 9136 | 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 8916). (Contributed by BTernaryTau, 24-Nov-2024.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | ||
Theorem | enreffi 9137 | Equinumerosity is reflexive for finite sets, proved without using the Axiom of Power Sets (unlike enrefg 8931). (Contributed by BTernaryTau, 8-Sep-2024.) |
⊢ (𝐴 ∈ Fin → 𝐴 ≈ 𝐴) | ||
Theorem | ensymfib 9138 | Symmetry of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike ensymb 8949). (Contributed by BTernaryTau, 9-Sep-2024.) |
⊢ (𝐴 ∈ Fin → (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴)) | ||
Theorem | entrfil 9139 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8953). (Contributed by BTernaryTau, 10-Sep-2024.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) | ||
Theorem | enfii 9140 | A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5325. (Revised by BTernaryTau, 23-Sep-2024.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin) | ||
Theorem | enfi 9141 | Equinumerous sets have the same finiteness. For a shorter proof using ax-pow 5325, see enfiALT 9142. (Contributed by NM, 22-Aug-2008.) Avoid ax-pow 5325. (Revised by BTernaryTau, 23-Sep-2024.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin)) | ||
Theorem | enfiALT 9142 | Shorter proof of enfi 9141 using ax-pow 5325. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin)) | ||
Theorem | domfi 9143 | 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 9144 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8953). (Contributed by BTernaryTau, 23-Sep-2024.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) | ||
Theorem | entrfir 9145 | Transitivity of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike entr 8953). (Contributed by BTernaryTau, 23-Sep-2024.) |
⊢ ((𝐶 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) | ||
Theorem | domtrfil 9146 | Transitivity of dominance relation when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike domtr 8954). (Contributed by BTernaryTau, 24-Nov-2024.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | ||
Theorem | domtrfi 9147 | Transitivity of dominance relation when 𝐵 is finite, proved without using the Axiom of Power Sets (unlike domtr 8954). (Contributed by BTernaryTau, 24-Nov-2024.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | ||
Theorem | domtrfir 9148 | Transitivity of dominance relation for finite sets, proved without using the Axiom of Power Sets (unlike domtr 8954). (Contributed by BTernaryTau, 24-Nov-2024.) |
⊢ ((𝐶 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | ||
Theorem | f1imaenfi 9149 | 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 8961). (Contributed by BTernaryTau, 29-Sep-2024.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ Fin) → (𝐹 “ 𝐶) ≈ 𝐶) | ||
Theorem | ssdomfi 9150 | A finite set dominates its subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8947). (Contributed by BTernaryTau, 12-Nov-2024.) |
⊢ (𝐵 ∈ Fin → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵)) | ||
Theorem | ssdomfi2 9151 | A set dominates its finite subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8947). (Contributed by BTernaryTau, 24-Nov-2024.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → 𝐴 ≼ 𝐵) | ||
Theorem | sbthfilem 9152* | Lemma for sbthfi 9153. (Contributed by BTernaryTau, 4-Nov-2024.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) | ||
Theorem | sbthfi 9153 | Schroeder-Bernstein Theorem for finite sets, proved without using the Axiom of Power Sets (unlike sbth 9044). (Contributed by BTernaryTau, 4-Nov-2024.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) | ||
Theorem | domnsymfi 9154 | 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 9050). (Contributed by BTernaryTau, 22-Nov-2024.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵) → ¬ 𝐵 ≺ 𝐴) | ||
Theorem | sdomdomtrfi 9155 | Transitivity of strict dominance and dominance when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike sdomdomtr 9061). (Contributed by BTernaryTau, 25-Nov-2024.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≺ 𝐶) | ||
Theorem | domsdomtrfi 9156 | Transitivity of dominance and strict dominance when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike domsdomtr 9063). (Contributed by BTernaryTau, 25-Nov-2024.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝐶) → 𝐴 ≺ 𝐶) | ||
Theorem | sucdom2 9157 | 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 5325. (Revised by BTernaryTau, 4-Dec-2024.) |
⊢ (𝐴 ≺ 𝐵 → suc 𝐴 ≼ 𝐵) | ||
Theorem | phplem1 9158 | 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 5325. (Revised by BTernaryTau, 23-Sep-2024.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) | ||
Theorem | phplem2 9159 | 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 5325. (Revised by BTernaryTau, 4-Nov-2024.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵)) | ||
Theorem | nneneq 9160 | 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 5325. (Revised by BTernaryTau, 11-Nov-2024.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | php 9161 | 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 9158, phplem2 9159, nneneq 9160, and this final piece of the proof. (Contributed by NM, 29-May-1998.) Avoid ax-pow 5325. (Revised by BTernaryTau, 18-Nov-2024.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵) | ||
Theorem | php2 9162 | Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998.) Avoid ax-pow 5325. (Revised by BTernaryTau, 20-Nov-2024.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
Theorem | php3 9163 | 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 5325. (Revised by BTernaryTau, 26-Nov-2024.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
Theorem | php4 9164 | Corollary of the Pigeonhole Principle php 9161: a natural number is strictly dominated by its successor. (Contributed by NM, 26-Jul-2004.) |
⊢ (𝐴 ∈ ω → 𝐴 ≺ suc 𝐴) | ||
Theorem | php5 9165 | Corollary of the Pigeonhole Principle php 9161: 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 9166 | Corollary of the Pigeonhole Principle using equality. Strengthening of php 9161 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-pow. (Revised by BTernaryTau, 28-Nov-2024.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | nndomog 9167 | Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 9184 when both are natural numbers. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9184. (Revised by RP, 5-Nov-2023.) Avoid ax-pow 5325. (Revised by BTernaryTau, 29-Nov-2024.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | phplem1OLD 9168 | Obsolete lemma for php 9161. (Contributed by NM, 25-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ({𝐴} ∪ (𝐴 ∖ {𝐵})) = (suc 𝐴 ∖ {𝐵})) | ||
Theorem | phplem2OLD 9169 | Obsolete lemma for php 9161. (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 9170 | Obsolete version of phplem1 9158 as of 23-Sep-2024. (Contributed by NM, 26-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) | ||
Theorem | phplem4OLD 9171 | Obsolete version of phplem2 9159 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 9172 | Obsolete version of nneneq 9160 as of 11-Nov-2024. (Contributed by NM, 28-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | phpOLD 9173 | Obsolete version of php 9161 as of 18-Nov-2024. (Contributed by NM, 29-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵) | ||
Theorem | php2OLD 9174 | Obsolete version of php2 9162 as of 20-Nov-2024. (Contributed by NM, 31-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
Theorem | php3OLD 9175 | Obsolete version of php3 9163 as of 26-Nov-2024. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
Theorem | phpeqdOLD 9176 | Obsolete version of phpeqd 9166 as of 28-Nov-2024. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | nndomogOLD 9177 | Obsolete version of nndomog 9167 as of 29-Nov-2024. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9184. (Revised by RP, 5-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | snnen2oOLD 9178 | Obsolete version of snnen2o 9188 as of 18-Nov-2024. (Contributed by AV, 6-Aug-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ {𝐴} ≈ 2o | ||
Theorem | onomeneq 9179 | 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 5325. (Revised by BTernaryTau, 2-Dec-2024.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | onomeneqOLD 9180 | Obsolete version of onomeneq 9179 as of 29-Nov-2024. (Contributed by NM, 26-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | onfin 9181 | 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 9182 | A set is a natural number iff it is a finite ordinal. (Contributed by Mario Carneiro, 22-Jan-2013.) |
⊢ ω = (On ∩ Fin) | ||
Theorem | nnfiOLD 9183 | Obsolete version of nnfi 9118 as of 23-Sep-2024. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin) | ||
Theorem | nndomo 9184 | Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146. (Contributed by NM, 17-Jun-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | nnsdomo 9185 | Cardinal ordering agrees with natural number ordering. (Contributed by NM, 17-Jun-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≺ 𝐵 ↔ 𝐴 ⊊ 𝐵)) | ||
Theorem | sucdom 9186 | 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 5325. (Revised by BTernaryTau, 4-Dec-2024.) (Proof shortened by BJ, 11-Jan-2025.) |
⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵)) | ||
Theorem | sucdomOLD 9187 | Obsolete version of sucdom 9186 as of 4-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵)) | ||
Theorem | snnen2o 9188 | 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 5325, ax-un 7677. (Revised by BTernaryTau, 1-Dec-2024.) |
⊢ ¬ {𝐴} ≈ 2o | ||
Theorem | 0sdom1dom 9189 | Strict dominance over 0 is the same as dominance over 1. For a shorter proof requiring ax-un 7677, see 0sdom1domALT . (Contributed by NM, 28-Sep-2004.) Avoid ax-un 7677. (Revised by BTernaryTau, 7-Dec-2024.) |
⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴) | ||
Theorem | 0sdom1domALT 9190 | Alternate proof of 0sdom1dom 9189, shorter but requiring ax-un 7677. (Contributed by NM, 28-Sep-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴) | ||
Theorem | 1sdom2 9191 | Ordinal 1 is strictly dominated by ordinal 2. For a shorter proof requiring ax-un 7677, see 1sdom2ALT 9192. (Contributed by NM, 4-Apr-2007.) Avoid ax-un 7677. (Revised by BTernaryTau, 8-Dec-2024.) |
⊢ 1o ≺ 2o | ||
Theorem | 1sdom2ALT 9192 | Alternate proof of 1sdom2 9191, shorter but requiring ax-un 7677. (Contributed by NM, 4-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 1o ≺ 2o | ||
Theorem | sdom1 9193 | A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014.) Avoid ax-pow 5325, ax-un 7677. (Revised by BTernaryTau, 12-Dec-2024.) |
⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅) | ||
Theorem | sdom1OLD 9194 | Obsolete version of sdom1 9193 as of 12-Dec-2024. (Contributed by Stefan O'Rear, 28-Oct-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅) | ||
Theorem | modom 9195 | Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (∃*𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≼ 1o) | ||
Theorem | modom2 9196* | Two ways to express "at most one". (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 ≼ 1o) | ||
Theorem | rex2dom 9197* | A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦) → 2o ≼ 𝐴) | ||
Theorem | 1sdom2dom 9198 | Strict dominance over 1 is the same as dominance over 2. (Contributed by BTernaryTau, 23-Dec-2024.) |
⊢ (1o ≺ 𝐴 ↔ 2o ≼ 𝐴) | ||
Theorem | 1sdom 9199* | A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom 8981.) (Contributed by Mario Carneiro, 12-Jan-2013.) Avoid ax-un 7677. (Revised by BTernaryTau, 30-Dec-2024.) |
⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) | ||
Theorem | 1sdomOLD 9200* | Obsolete version of 1sdom 9199 as of 30-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |