Home | Metamath
Proof Explorer Theorem List (p. 81 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2pwne 8001 | No set equals the power set of its power set. (Contributed by NM, 17-Nov-2008.) |
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝒫 𝐴 ≠ 𝐴) | ||
Theorem | disjen 8002 | A stronger form of pwuninel 7288. We can use pwuninel 7288, 2pwuninel 8000 to create one or two sets disjoint from a given set 𝐴, but here we show that in fact such constructions exist for arbitrarily large disjoint extensions, which is to say that for any set 𝐵 we can construct a set 𝑥 that is equinumerous to it and disjoint from 𝐴. (Contributed by Mario Carneiro, 7-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∩ (𝐵 × {𝒫 ∪ ran 𝐴})) = ∅ ∧ (𝐵 × {𝒫 ∪ ran 𝐴}) ≈ 𝐵)) | ||
Theorem | disjenex 8003* | Existence version of disjen 8002. (Contributed by Mario Carneiro, 7-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∃𝑥((𝐴 ∩ 𝑥) = ∅ ∧ 𝑥 ≈ 𝐵)) | ||
Theorem | domss2 8004 | A corollary of disjenex 8003. If 𝐹 is an injection from 𝐴 to 𝐵 then 𝐺 is a right inverse of 𝐹 from 𝐵 to a superset of 𝐴. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐺 = ◡(𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) ⇒ ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺:𝐵–1-1-onto→ran 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))) | ||
Theorem | domssex2 8005* | A corollary of disjenex 8003. If 𝐹 is an injection from 𝐴 to 𝐵 then there is a right inverse 𝑔 of 𝐹 from 𝐵 to a superset of 𝐴. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∃𝑔(𝑔:𝐵–1-1→V ∧ (𝑔 ∘ 𝐹) = ( I ↾ 𝐴))) | ||
Theorem | domssex 8006* | Weakening of domssex 8006 to forget the functions in favor of dominance and equinumerosity. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝐴 ≼ 𝐵 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥)) | ||
Theorem | xpf1o 8007* | Construct a bijection on a Cartesian product given bijections on the factors. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑋):𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → (𝑦 ∈ 𝐶 ↦ 𝑌):𝐶–1-1-onto→𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 〈𝑋, 𝑌〉):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷)) | ||
Theorem | xpen 8008 | Equinumerosity law for Cartesian product. Proposition 4.22(b) of [Mendelson] p. 254. (Contributed by NM, 24-Jul-2004.) (Proof shortened by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 × 𝐶) ≈ (𝐵 × 𝐷)) | ||
Theorem | mapen 8009 | Two set exponentiations are equinumerous when their bases and exponents are equinumerous. Theorem 6H(c) of [Enderton] p. 139. (Contributed by NM, 16-Dec-2003.) (Proof shortened by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ↑𝑚 𝐶) ≈ (𝐵 ↑𝑚 𝐷)) | ||
Theorem | mapdom1 8010 | Order-preserving property of set exponentiation. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 9-Mar-2013.) |
⊢ (𝐴 ≼ 𝐵 → (𝐴 ↑𝑚 𝐶) ≼ (𝐵 ↑𝑚 𝐶)) | ||
Theorem | mapxpen 8011 | Equinumerosity law for double set exponentiation. Proposition 10.45 of [TakeutiZaring] p. 96. (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ↑𝑚 𝐵) ↑𝑚 𝐶) ≈ (𝐴 ↑𝑚 (𝐵 × 𝐶))) | ||
Theorem | xpmapenlem 8012* | Lemma for xpmapen 8013. (Contributed by NM, 1-May-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 = (𝑧 ∈ 𝐶 ↦ (1st ‘(𝑥‘𝑧))) & ⊢ 𝑅 = (𝑧 ∈ 𝐶 ↦ (2nd ‘(𝑥‘𝑧))) & ⊢ 𝑆 = (𝑧 ∈ 𝐶 ↦ 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) ⇒ ⊢ ((𝐴 × 𝐵) ↑𝑚 𝐶) ≈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) | ||
Theorem | xpmapen 8013 | Equinumerosity law for set exponentiation of a Cartesian product. Exercise 4.47 of [Mendelson] p. 255. (Contributed by NM, 23-Feb-2004.) (Proof shortened by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ ((𝐴 × 𝐵) ↑𝑚 𝐶) ≈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) | ||
Theorem | mapunen 8014 | Equinumerosity law for set exponentiation of a disjoint union. Exercise 4.45 of [Mendelson] p. 255. (Contributed by NM, 23-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ≈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵))) | ||
Theorem | map2xp 8015 | A cardinal power with exponent 2 is equivalent to a Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑𝑚 2𝑜) ≈ (𝐴 × 𝐴)) | ||
Theorem | mapdom2 8016 | Order-preserving property of set exponentiation. Theorem 6L(d) of [Enderton] p. 149. (Contributed by NM, 23-Sep-2004.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶 ↑𝑚 𝐴) ≼ (𝐶 ↑𝑚 𝐵)) | ||
Theorem | mapdom3 8017 | Set exponentiation dominates the mantissa. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅) → 𝐴 ≼ (𝐴 ↑𝑚 𝐵)) | ||
Theorem | pwen 8018 | 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 8019* | Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐴 ≈ 𝐵 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐶)} ≈ {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝑥 ≈ 𝐶)}) | ||
Theorem | limenpsi 8020 | 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 8021 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
⊢ Lim 𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ suc 𝐴) | ||
Theorem | limensuc 8022 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ≈ suc 𝐴) | ||
Theorem | infensuc 8023 | 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 | phplem1 8024 | Lemma for Pigeonhole Principle. If we join a natural number to itself minus an element, we end up with its successor minus the same element. (Contributed by NM, 25-May-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ({𝐴} ∪ (𝐴 ∖ {𝐵})) = (suc 𝐴 ∖ {𝐵})) | ||
Theorem | phplem2 8025 | Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus one of its elements. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) | ||
Theorem | phplem3 8026 | Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus any element of the successor. (Contributed by NM, 26-May-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) | ||
Theorem | phplem4 8027 | 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.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵)) | ||
Theorem | nneneq 8028 | 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.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | php 8029 | 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 lemmas phplem1 8024 through phplem4 8027, nneneq 8028, and this final piece of the proof. (Contributed by NM, 29-May-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵) | ||
Theorem | php2 8030 | Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
Theorem | php3 8031 | 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.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
Theorem | php4 8032 | Corollary of the Pigeonhole Principle php 8029: a natural number is strictly dominated by its successor. (Contributed by NM, 26-Jul-2004.) |
⊢ (𝐴 ∈ ω → 𝐴 ≺ suc 𝐴) | ||
Theorem | php5 8033 | Corollary of the Pigeonhole Principle php 8029: 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 | snnen2o 8034 | 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.) |
⊢ ¬ {𝐴} ≈ 2𝑜 | ||
Theorem | onomeneq 8035 | 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.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | onfin 8036 | 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 8037 | A set is a natural number iff it is a finite ordinal. (Contributed by Mario Carneiro, 22-Jan-2013.) |
⊢ ω = (On ∩ Fin) | ||
Theorem | nnfi 8038 | Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin) | ||
Theorem | nndomo 8039 | Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146. (Contributed by NM, 17-Jun-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | nnsdomo 8040 | Cardinal ordering agrees with natural number ordering. (Contributed by NM, 17-Jun-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≺ 𝐵 ↔ 𝐴 ⊊ 𝐵)) | ||
Theorem | sucdom2 8041 | 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.) |
⊢ (𝐴 ≺ 𝐵 → suc 𝐴 ≼ 𝐵) | ||
Theorem | sucdom 8042 | Strict dominance of a set over a natural number is the same as dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013.) |
⊢ (𝐴 ∈ ω → (𝐴 ≺ 𝐵 ↔ suc 𝐴 ≼ 𝐵)) | ||
Theorem | 0sdom1dom 8043 | Strict dominance over zero is the same as dominance over one. (Contributed by NM, 28-Sep-2004.) |
⊢ (∅ ≺ 𝐴 ↔ 1𝑜 ≼ 𝐴) | ||
Theorem | 1sdom2 8044 | Ordinal 1 is strictly dominated by ordinal 2. (Contributed by NM, 4-Apr-2007.) |
⊢ 1𝑜 ≺ 2𝑜 | ||
Theorem | sdom1 8045 | A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (𝐴 ≺ 1𝑜 ↔ 𝐴 = ∅) | ||
Theorem | modom 8046 | Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (∃*𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≼ 1𝑜) | ||
Theorem | modom2 8047* | Two ways to express "at most one". (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 ≼ 1𝑜) | ||
Theorem | 1sdom 8048* | A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom 7915.) (Contributed by Mario Carneiro, 12-Jan-2013.) |
⊢ (𝐴 ∈ 𝑉 → (1𝑜 ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) | ||
Theorem | unxpdomlem1 8049* | Lemma for unxpdom 8052. (Trivial substitution proof.) (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) ⇒ ⊢ (𝑧 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉)) | ||
Theorem | unxpdomlem2 8050* | Lemma for unxpdom 8052. (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) & ⊢ (𝜑 → 𝑤 ∈ (𝑎 ∪ 𝑏)) & ⊢ (𝜑 → ¬ 𝑚 = 𝑛) & ⊢ (𝜑 → ¬ 𝑠 = 𝑡) ⇒ ⊢ ((𝜑 ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) | ||
Theorem | unxpdomlem3 8051* | Lemma for unxpdom 8052. (Contributed by Mario Carneiro, 13-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) ⇒ ⊢ ((1𝑜 ≺ 𝑎 ∧ 1𝑜 ≺ 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)) | ||
Theorem | unxpdom 8052 | 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.) |
⊢ ((1𝑜 ≺ 𝐴 ∧ 1𝑜 ≺ 𝐵) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐵)) | ||
Theorem | unxpdom2 8053 | Corollary of unxpdom 8052. (Contributed by NM, 16-Sep-2004.) |
⊢ ((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴)) | ||
Theorem | sucxpdom 8054 | 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.) |
⊢ (1𝑜 ≺ 𝐴 → suc 𝐴 ≼ (𝐴 × 𝐴)) | ||
Theorem | pssinf 8055 | 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 8056 | A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵) | ||
Theorem | ominf 8057 | The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.) |
⊢ ¬ ω ∈ Fin | ||
Theorem | isinf 8058* | Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set has countably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by Mario Carneiro, 15-Jan-2013.) |
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛)) | ||
Theorem | fineqvlem 8059 | Lemma for fineqv 8060. (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 8060 | If the Axiom of Infinity is denied, then all sets are finite (which implies the Axiom of Choice). (Contributed by Mario Carneiro, 20-Jan-2013.) (Revised by Mario Carneiro, 3-Jan-2015.) |
⊢ (¬ ω ∈ V ↔ Fin = V) | ||
Theorem | enfi 8061 | Equinumerous sets have the same finiteness. (Contributed by NM, 22-Aug-2008.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin)) | ||
Theorem | enfii 8062 | A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin) | ||
Theorem | pssnn 8063* | A proper subset of a natural number is equinumerous to some smaller number. Lemma 6F of [Enderton] p. 137. (Contributed by NM, 22-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥) | ||
Theorem | ssnnfi 8064 | A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
Theorem | ssfi 8065 | A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. (Contributed by NM, 24-Jun-1998.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
Theorem | domfi 8066 | A set dominated by a finite set is finite. (Contributed by NM, 23-Mar-2006.) (Revised by Mario Carneiro, 12-Mar-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ Fin) | ||
Theorem | xpfir 8067 | 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 8068 | A subset of a finite set is finite, deduction version of ssfi 8065. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ Fin) | ||
Theorem | infi 8069 | The intersection of two sets is finite if one of them is. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (𝐴 ∈ Fin → (𝐴 ∩ 𝐵) ∈ Fin) | ||
Theorem | rabfi 8070* | A restricted class built from a finite set is finite. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (𝐴 ∈ Fin → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ Fin) | ||
Theorem | finresfin 8071 | The restriction of a finite set is finite. (Contributed by Alexander van der Vekens, 3-Jan-2018.) |
⊢ (𝐸 ∈ Fin → (𝐸 ↾ 𝐵) ∈ Fin) | ||
Theorem | f1finf1o 8072 | Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010.) (Revised by Mario Carneiro, 27-Feb-2014.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵)) | ||
Theorem | 0fin 8073 | The empty set is finite. (Contributed by FL, 14-Jul-2008.) |
⊢ ∅ ∈ Fin | ||
Theorem | nfielex 8074* | If a class is not finite, it contains at least one element. (Contributed by Alexander van der Vekens, 12-Jan-2018.) |
⊢ (¬ 𝐴 ∈ Fin → ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | en1eqsn 8075 | A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1𝑜) → 𝐵 = {𝐴}) | ||
Theorem | en1eqsnbi 8076 | A set containing an element has exactly one element iff it is a singleton. Formerly part of proof for rngen1zr 19097. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
⊢ (𝐴 ∈ 𝐵 → (𝐵 ≈ 1𝑜 ↔ 𝐵 = {𝐴})) | ||
Theorem | diffi 8077 | If 𝐴 is finite, (𝐴 ∖ 𝐵) is finite. (Contributed by FL, 3-Aug-2009.) |
⊢ (𝐴 ∈ Fin → (𝐴 ∖ 𝐵) ∈ Fin) | ||
Theorem | dif1en 8078 | If a set 𝐴 is equinumerous to the successor of a natural number 𝑀, then 𝐴 with an element removed is equinumerous to 𝑀. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) |
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀) | ||
Theorem | enp1ilem 8079 | Lemma for uses of enp1i 8080. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 𝑇 = ({𝑥} ∪ 𝑆) ⇒ ⊢ (𝑥 ∈ 𝐴 → ((𝐴 ∖ {𝑥}) = 𝑆 → 𝐴 = 𝑇)) | ||
Theorem | enp1i 8080* | Proof induction for en2i 7879 and related theorems. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 𝑀 ∈ ω & ⊢ 𝑁 = suc 𝑀 & ⊢ ((𝐴 ∖ {𝑥}) ≈ 𝑀 → 𝜑) & ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ≈ 𝑁 → ∃𝑥𝜓) | ||
Theorem | en2 8081* | A set equinumerous to ordinal 2 is a pair. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 2𝑜 → ∃𝑥∃𝑦 𝐴 = {𝑥, 𝑦}) | ||
Theorem | en3 8082* | A set equinumerous to ordinal 3 is a triple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 3𝑜 → ∃𝑥∃𝑦∃𝑧 𝐴 = {𝑥, 𝑦, 𝑧}) | ||
Theorem | en4 8083* | A set equinumerous to ordinal 4 is a quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 4𝑜 → ∃𝑥∃𝑦∃𝑧∃𝑤 𝐴 = ({𝑥, 𝑦} ∪ {𝑧, 𝑤})) | ||
Theorem | findcard 8084* | 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 8085* | Schema for induction on the cardinality of a finite set. The inductive step shows that the result is true if one more element is added to the set. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 8-Jul-2010.) |
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ Fin → 𝜏) | ||
Theorem | findcard2s 8086* | Variation of findcard2 8085 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 8087* | Deduction version of findcard2 8085. (Contributed by SO, 16-Jul-2018.) |
⊢ (𝑥 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝜃 → 𝜏)) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | findcard3 8088* | Schema for strong induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on any proper subset. The result is then proven to be true for all finite sets. (Contributed by Mario Carneiro, 13-Dec-2013.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝑦 ∈ Fin → (∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒)) ⇒ ⊢ (𝐴 ∈ Fin → 𝜏) | ||
Theorem | ac6sfi 8089* | A version of ac6s 9189 for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.) |
⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | frfi 8090 | 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 8091* | 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 8092* | 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 8093* | Lemma showing existence and closure of supremum of a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))) | ||
Theorem | wofi 8094 | 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 8095 | 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 8096 | 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 8097* | Lemma for unbnn 8101. 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 8098* | Lemma for unbnn 8101. The value of the function 𝐹 belongs to the unbounded set of natural numbers 𝐴. (Contributed by NM, 3-Dec-2003.) |
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω) ⇒ ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ 𝐴)) | ||
Theorem | unblem3 8099* | Lemma for unbnn 8101. 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 8100* | Lemma for unbnn 8101. 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→𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |