Home | Metamath
Proof Explorer Theorem List (p. 92 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | php2OLD 9101 | Obsolete version of php2 9089 as of 20-Nov-2024. (Contributed by NM, 31-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
Theorem | php3OLD 9102 | Obsolete version of php3 9090 as of 26-Nov-2024. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
Theorem | phpeqdOLD 9103 | Obsolete version of phpeqd 9093 as of 28-Nov-2024. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | nndomogOLD 9104 | Obsolete version of nndomog 9094 as of 29-Nov-2024. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9111. (Revised by RP, 5-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | snnen2oOLD 9105 | Obsolete version of snnen2o 9115 as of 18-Nov-2024. (Contributed by AV, 6-Aug-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ {𝐴} ≈ 2o | ||
Theorem | onomeneq 9106 | 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 5319. (Revised by BTernaryTau, 2-Dec-2024.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | onomeneqOLD 9107 | Obsolete version of onomeneq 9106 as of 29-Nov-2024. (Contributed by NM, 26-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | onfin 9108 | 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 9109 | A set is a natural number iff it is a finite ordinal. (Contributed by Mario Carneiro, 22-Jan-2013.) |
⊢ ω = (On ∩ Fin) | ||
Theorem | nnfiOLD 9110 | Obsolete version of nnfi 9045 as of 23-Sep-2024. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin) | ||
Theorem | nndomo 9111 | Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146. (Contributed by NM, 17-Jun-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | nnsdomo 9112 | Cardinal ordering agrees with natural number ordering. (Contributed by NM, 17-Jun-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≺ 𝐵 ↔ 𝐴 ⊊ 𝐵)) | ||
Theorem | sucdom 9113 | 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 5319. (Revised by BTernaryTau, 4-Dec-2024.) (Proof shortened by BJ, 11-Jan-2025.) |
⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵)) | ||
Theorem | sucdomOLD 9114 | Obsolete version of sucdom 9113 as of 4-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵)) | ||
Theorem | snnen2o 9115 | 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 5319, ax-un 7663. (Revised by BTernaryTau, 1-Dec-2024.) |
⊢ ¬ {𝐴} ≈ 2o | ||
Theorem | 0sdom1dom 9116 | Strict dominance over 0 is the same as dominance over 1. For a shorter proof requiring ax-un 7663, see 0sdom1domALT . (Contributed by NM, 28-Sep-2004.) Avoid ax-un 7663. (Revised by BTernaryTau, 7-Dec-2024.) |
⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴) | ||
Theorem | 0sdom1domALT 9117 | Alternate proof of 0sdom1dom 9116, shorter but requiring ax-un 7663. (Contributed by NM, 28-Sep-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∅ ≺ 𝐴 ↔ 1o ≼ 𝐴) | ||
Theorem | 1sdom2 9118 | Ordinal 1 is strictly dominated by ordinal 2. For a shorter proof requiring ax-un 7663, see 1sdom2ALT 9119. (Contributed by NM, 4-Apr-2007.) Avoid ax-un 7663. (Revised by BTernaryTau, 8-Dec-2024.) |
⊢ 1o ≺ 2o | ||
Theorem | 1sdom2ALT 9119 | Alternate proof of 1sdom2 9118, shorter but requiring ax-un 7663. (Contributed by NM, 4-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 1o ≺ 2o | ||
Theorem | sdom1 9120 | A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014.) Avoid ax-pow 5319, ax-un 7663. (Revised by BTernaryTau, 12-Dec-2024.) |
⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅) | ||
Theorem | sdom1OLD 9121 | Obsolete version of sdom1 9120 as of 12-Dec-2024. (Contributed by Stefan O'Rear, 28-Oct-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≺ 1o ↔ 𝐴 = ∅) | ||
Theorem | modom 9122 | Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (∃*𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≼ 1o) | ||
Theorem | modom2 9123* | Two ways to express "at most one". (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 ≼ 1o) | ||
Theorem | rex2dom 9124* | A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦) → 2o ≼ 𝐴) | ||
Theorem | 1sdom2dom 9125 | Strict dominance over 1 is the same as dominance over 2. (Contributed by BTernaryTau, 23-Dec-2024.) |
⊢ (1o ≺ 𝐴 ↔ 2o ≼ 𝐴) | ||
Theorem | 1sdom 9126* | A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom 8908.) (Contributed by Mario Carneiro, 12-Jan-2013.) Avoid ax-un 7663. (Revised by BTernaryTau, 30-Dec-2024.) |
⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) | ||
Theorem | 1sdomOLD 9127* | Obsolete version of 1sdom 9126 as of 30-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (1o ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) | ||
Theorem | unxpdomlem1 9128* | Lemma for unxpdom 9131. (Trivial substitution proof.) (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩) ⇒ ⊢ (𝑧 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, ⟨𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧⟩)) | ||
Theorem | unxpdomlem2 9129* | Lemma for unxpdom 9131. (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩) & ⊢ (𝜑 → 𝑤 ∈ (𝑎 ∪ 𝑏)) & ⊢ (𝜑 → ¬ 𝑚 = 𝑛) & ⊢ (𝜑 → ¬ 𝑠 = 𝑡) ⇒ ⊢ ((𝜑 ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) | ||
Theorem | unxpdomlem3 9130* | Lemma for unxpdom 9131. (Contributed by Mario Carneiro, 13-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, ⟨𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)⟩, ⟨if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥⟩) ⇒ ⊢ ((1o ≺ 𝑎 ∧ 1o ≺ 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)) | ||
Theorem | unxpdom 9131 | 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 9132 | Corollary of unxpdom 9131. (Contributed by NM, 16-Sep-2004.) |
⊢ ((1o ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴)) | ||
Theorem | sucxpdom 9133 | 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 9134 | 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 9135 | A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵) | ||
Theorem | ominf 9136 | The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.) Avoid ax-pow 5319. (Revised by BTernaryTau, 2-Jan-2025.) |
⊢ ¬ ω ∈ Fin | ||
Theorem | ominfOLD 9137 | Obsolete version of ominf 9136 as of 2-Jan-2025. (Contributed by NM, 2-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ω ∈ Fin | ||
Theorem | isinf 9138* | 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 5319. (Revised by BTernaryTau, 2-Jan-2025.) |
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)) | ||
Theorem | isinfOLD 9139* | Obsolete version of isinf 9138 as of 2-Jan-2025. (Contributed by Mario Carneiro, 15-Jan-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)) | ||
Theorem | fineqvlem 9140 | Lemma for fineqv 9141. (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 9141 | 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 | enfiiOLD 9142 | Obsolete version of enfii 9067 as of 23-Sep-2024. (Contributed by Mario Carneiro, 12-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin) | ||
Theorem | pssnnOLD 9143* | Obsolete version of pssnn 9046 as of 31-Jul-2024. (Contributed by NM, 22-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥) | ||
Theorem | xpfir 9144 | 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 9145 | A subset of a finite set is finite, deduction version of ssfi 9051. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ Fin) | ||
Theorem | infi 9146 | The intersection of two sets is finite if one of them is. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (𝐴 ∈ Fin → (𝐴 ∩ 𝐵) ∈ Fin) | ||
Theorem | rabfi 9147* | A restricted class built from a finite set is finite. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (𝐴 ∈ Fin → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ Fin) | ||
Theorem | finresfin 9148 | The restriction of a finite set is finite. (Contributed by Alexander van der Vekens, 3-Jan-2018.) |
⊢ (𝐸 ∈ Fin → (𝐸 ↾ 𝐵) ∈ Fin) | ||
Theorem | f1finf1o 9149 | 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 5319. (Revised by BTernaryTau, 4-Jan-2025.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵)) | ||
Theorem | f1finf1oOLD 9150 | Obsolete version of f1finf1o 9149 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 9151* | 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 9152 | A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) Avoid ax-pow 5319, ax-un 7663. (Revised by BTernaryTau, 4-Jan-2025.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o) → 𝐵 = {𝐴}) | ||
Theorem | en1eqsnOLD 9153 | Obsolete version of en1eqsn 9152 as of 4-Jan-2025. (Contributed by FL, 18-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o) → 𝐵 = {𝐴}) | ||
Theorem | en1eqsnbi 9154 | A set containing an element has exactly one element iff it is a singleton. Formerly part of proof for rngen1zr 20669. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
⊢ (𝐴 ∈ 𝐵 → (𝐵 ≈ 1o ↔ 𝐵 = {𝐴})) | ||
Theorem | dif1ennnALT 9155 | Alternate proof of dif1ennn 9039 using ax-pow 5319. (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 9156 | Lemma for uses of enp1i 9157. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 𝑇 = ({𝑥} ∪ 𝑆) ⇒ ⊢ (𝑥 ∈ 𝐴 → ((𝐴 ∖ {𝑥}) = 𝑆 → 𝐴 = 𝑇)) | ||
Theorem | enp1i 9157* | Proof induction for en2 9159 and related theorems. (Contributed by Mario Carneiro, 5-Jan-2016.) Generalize to all ordinals and avoid ax-pow 5319, ax-un 7663. (Revised by BTernaryTau, 6-Jan-2025.) |
⊢ Ord 𝑀 & ⊢ 𝑁 = suc 𝑀 & ⊢ ((𝐴 ∖ {𝑥}) ≈ 𝑀 → 𝜑) & ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ≈ 𝑁 → ∃𝑥𝜓) | ||
Theorem | enp1iOLD 9158* | Obsolete version of enp1i 9157 as of 6-Jan-2025. (Contributed by Mario Carneiro, 5-Jan-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑀 ∈ ω & ⊢ 𝑁 = suc 𝑀 & ⊢ ((𝐴 ∖ {𝑥}) ≈ 𝑀 → 𝜑) & ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ≈ 𝑁 → ∃𝑥𝜓) | ||
Theorem | en2 9159* | A set equinumerous to ordinal 2 is a pair. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 2o → ∃𝑥∃𝑦 𝐴 = {𝑥, 𝑦}) | ||
Theorem | en3 9160* | A set equinumerous to ordinal 3 is a triple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 3o → ∃𝑥∃𝑦∃𝑧 𝐴 = {𝑥, 𝑦, 𝑧}) | ||
Theorem | en4 9161* | A set equinumerous to ordinal 4 is a quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 4o → ∃𝑥∃𝑦∃𝑧∃𝑤 𝐴 = ({𝑥, 𝑦} ∪ {𝑧, 𝑤})) | ||
Theorem | findcard2OLD 9162* | Obsolete version of findcard2 9042 as of 6-Aug-2024. (Contributed by Jeff Madsen, 8-Jul-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ Fin → 𝜏) | ||
Theorem | findcard3 9163* | 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 5319. (Revised by BTernaryTau, 7-Jan-2025.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝑦 ∈ Fin → (∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒)) ⇒ ⊢ (𝐴 ∈ Fin → 𝜏) | ||
Theorem | findcard3OLD 9164* | Obsolete version of findcard3 9163 as of 7-Jan-2025. (Contributed by Mario Carneiro, 13-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝑦 ∈ Fin → (∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒)) ⇒ ⊢ (𝐴 ∈ Fin → 𝜏) | ||
Theorem | ac6sfi 9165* | A version of ac6s 10354 for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | frfi 9166 | 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 9167* | 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 9168* | 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 9169* | Lemma showing existence and closure of supremum of a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))) | ||
Theorem | wofi 9170 | 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 9171 | 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 9172 | 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 9173* | Lemma for unbnn 9177. 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 9174* | Lemma for unbnn 9177. The value of the function 𝐹 belongs to the unbounded set of natural numbers 𝐴. (Contributed by NM, 3-Dec-2003.) |
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω) ⇒ ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ 𝐴)) | ||
Theorem | unblem3 9175* | Lemma for unbnn 9177. 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 9176* | Lemma for unbnn 9177. 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 9177* | 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 9529 for a stronger version without the first assumption. (Contributed by NM, 3-Dec-2003.) |
⊢ ((ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → 𝐴 ≈ ω) | ||
Theorem | unbnn2 9178* | Version of unbnn 9177 that does not require a strict upper bound. (Contributed by NM, 24-Apr-2004.) |
⊢ ((ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) → 𝐴 ≈ ω) | ||
Theorem | isfinite2 9179 | 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 9180 | 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 9524 for the version without this sethood requirement. (Contributed by NM, 15-Jun-1998.) Avoid ax-pow 5319. (Revised by BTernaryTau, 7-Jan-2025.) |
⊢ ((ω ∈ V ∧ 𝐴 ∈ ω) → 𝐴 ≺ ω) | ||
Theorem | nnsdomgOLD 9181 | Obsolete version of nnsdomg 9180 as of 7-Jan-2025. (Contributed by NM, 15-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((ω ∈ V ∧ 𝐴 ∈ ω) → 𝐴 ≺ ω) | ||
Theorem | isfiniteg 9182 | 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 9183 | An infinite set strictly dominates a natural number. (Contributed by NM, 22-Nov-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) Avoid ax-pow 5319. (Revised by BTernaryTau, 7-Jan-2025.) |
⊢ ((ω ≼ 𝐴 ∧ 𝐵 ∈ ω) → 𝐵 ≺ 𝐴) | ||
Theorem | infsdomnnOLD 9184 | Obsolete version of infsdomnn 9183 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 9185 | An infinite set is not empty. For a shorter proof using ax-un 7663, see infn0ALT 9186. (Contributed by NM, 23-Oct-2004.) Avoid ax-un 7663. (Revised by BTernaryTau, 8-Jan-2025.) |
⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅) | ||
Theorem | infn0ALT 9186 | Shorter proof of infn0 9185 using ax-un 7663. (Contributed by NM, 23-Oct-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅) | ||
Theorem | fin2inf 9187 | 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 9188* | 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 9189* | 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 9190 | 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 | unfiOLD 9191 | Obsolete version of unfi 9050 as of 7-Aug-2024. (Contributed by NM, 16-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin) | ||
Theorem | unfir 9192 | If a union is finite, the operands are finite. Converse of unfi 9050. (Contributed by FL, 3-Aug-2009.) |
⊢ ((𝐴 ∪ 𝐵) ∈ Fin → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin)) | ||
Theorem | unfi2 9193 | The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. This version of unfi 9050 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 9187). (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) |
⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 ∪ 𝐵) ≺ ω) | ||
Theorem | difinf 9194 | An infinite set 𝐴 minus a finite set is infinite. (Contributed by FL, 3-Aug-2009.) |
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ¬ (𝐴 ∖ 𝐵) ∈ Fin) | ||
Theorem | xpfi 9195 | 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 5319. (Revised by BTernaryTau, 10-Jan-2025.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin) | ||
Theorem | xpfiOLD 9196 | Obsolete version of xpfi 9195 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 9197 | The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
⊢ (𝑉 ∈ Fin → ((𝑉 × 𝑉) × 𝑉) ∈ Fin) | ||
Theorem | domunfican 9198 | 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 9199* | 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 9200 | An unordered pair is finite. (Contributed by NM, 22-Aug-2008.) |
⊢ {𝐴, 𝐵} ∈ Fin |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |