Home | Metamath
Proof Explorer Theorem List (p. 82 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | enen2 8101 | Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.) |
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≈ 𝐴 ↔ 𝐶 ≈ 𝐵)) | ||
Theorem | domen1 8102 | Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≼ 𝐶 ↔ 𝐵 ≼ 𝐶)) | ||
Theorem | domen2 8103 | Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.) |
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≼ 𝐴 ↔ 𝐶 ≼ 𝐵)) | ||
Theorem | sdomen1 8104 | Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≺ 𝐶 ↔ 𝐵 ≺ 𝐶)) | ||
Theorem | sdomen2 8105 | Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003.) |
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≺ 𝐴 ↔ 𝐶 ≺ 𝐵)) | ||
Theorem | domtriord 8106 | Dominance is trichotomous in the restricted case of ordinal numbers. (Contributed by Jeff Hankins, 24-Oct-2009.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) | ||
Theorem | sdomel 8107 | Strict dominance implies ordinal membership. (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ≺ 𝐵 → 𝐴 ∈ 𝐵)) | ||
Theorem | sdomdif 8108 | The difference of a set from a smaller set cannot be empty. (Contributed by Mario Carneiro, 5-Feb-2013.) |
⊢ (𝐴 ≺ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅) | ||
Theorem | onsdominel 8109 | An ordinal with more elements of some type is larger. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ (𝐴 ∩ 𝐶) ≺ (𝐵 ∩ 𝐶)) → 𝐴 ∈ 𝐵) | ||
Theorem | domunsn 8110 | Dominance over a set with one element added. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (𝐴 ≺ 𝐵 → (𝐴 ∪ {𝐶}) ≼ 𝐵) | ||
Theorem | fodomr 8111* | There exists a mapping from a set onto any (nonempty) set that it dominates. (Contributed by NM, 23-Mar-2006.) |
⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵) | ||
Theorem | pwdom 8112 | Injection of sets implies injection on power sets. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ (𝐴 ≼ 𝐵 → 𝒫 𝐴 ≼ 𝒫 𝐵) | ||
Theorem | canth2 8113 | Cantor's Theorem. No set is equinumerous to its power set. Specifically, any set has a cardinality (size) strictly less than the cardinality of its power set. For example, the cardinality of real numbers is the same as the cardinality of the power set of integers, so real numbers cannot be put into a one-to-one correspondence with integers. Theorem 23 of [Suppes] p. 97. For the function version, see canth 6608. This is Metamath 100 proof #63. (Contributed by NM, 7-Aug-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ≺ 𝒫 𝐴 | ||
Theorem | canth2g 8114 | Cantor's theorem with the sethood requirement expressed as an antecedent. Theorem 23 of [Suppes] p. 97. (Contributed by NM, 7-Nov-2003.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≺ 𝒫 𝐴) | ||
Theorem | 2pwuninel 8115 | The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by NM, 27-Jun-2008.) |
⊢ ¬ 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴 | ||
Theorem | 2pwne 8116 | No set equals the power set of its power set. (Contributed by NM, 17-Nov-2008.) |
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝒫 𝐴 ≠ 𝐴) | ||
Theorem | disjen 8117 | A stronger form of pwuninel 7401. We can use pwuninel 7401, 2pwuninel 8115 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 8118* | Existence version of disjen 8117. (Contributed by Mario Carneiro, 7-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∃𝑥((𝐴 ∩ 𝑥) = ∅ ∧ 𝑥 ≈ 𝐵)) | ||
Theorem | domss2 8119 | A corollary of disjenex 8118. 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 8120* | A corollary of disjenex 8118. 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 8121* | Weakening of domssex 8121 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 8122* | 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 8123 | 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 8124 | 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 8125 | 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 8126 | 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 8127* | Lemma for xpmapen 8128. (Contributed by NM, 1-May-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 = (𝑧 ∈ 𝐶 ↦ (1st ‘(𝑥‘𝑧))) & ⊢ 𝑅 = (𝑧 ∈ 𝐶 ↦ (2nd ‘(𝑥‘𝑧))) & ⊢ 𝑆 = (𝑧 ∈ 𝐶 ↦ 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) ⇒ ⊢ ((𝐴 × 𝐵) ↑𝑚 𝐶) ≈ ((𝐴 ↑𝑚 𝐶) × (𝐵 ↑𝑚 𝐶)) | ||
Theorem | xpmapen 8128 | 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 8129 | 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 8130 | A cardinal power with exponent 2 is equivalent to a Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑𝑚 2𝑜) ≈ (𝐴 × 𝐴)) | ||
Theorem | mapdom2 8131 | 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 8132 | Set exponentiation dominates the mantissa. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅) → 𝐴 ≼ (𝐴 ↑𝑚 𝐵)) | ||
Theorem | pwen 8133 | 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 8134* | Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐴 ≈ 𝐵 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐶)} ≈ {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝑥 ≈ 𝐶)}) | ||
Theorem | limenpsi 8135 | 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 8136 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
⊢ Lim 𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ suc 𝐴) | ||
Theorem | limensuc 8137 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ≈ suc 𝐴) | ||
Theorem | infensuc 8138 | 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 8139 | 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 8140 | 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 8141 | 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 8142 | 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 8143 | 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 8144 | 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 8139 through phplem4 8142, nneneq 8143, and this final piece of the proof. (Contributed by NM, 29-May-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵) | ||
Theorem | php2 8145 | Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ≺ 𝐴) | ||
Theorem | php3 8146 | 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 8147 | Corollary of the Pigeonhole Principle php 8144: a natural number is strictly dominated by its successor. (Contributed by NM, 26-Jul-2004.) |
⊢ (𝐴 ∈ ω → 𝐴 ≺ suc 𝐴) | ||
Theorem | php5 8148 | Corollary of the Pigeonhole Principle php 8144: 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 8149 | 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 8150 | 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 8151 | 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 8152 | A set is a natural number iff it is a finite ordinal. (Contributed by Mario Carneiro, 22-Jan-2013.) |
⊢ ω = (On ∩ Fin) | ||
Theorem | nnfi 8153 | Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin) | ||
Theorem | nndomo 8154 | Cardinal ordering agrees with natural number ordering. Example 3 of [Enderton] p. 146. (Contributed by NM, 17-Jun-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | nnsdomo 8155 | Cardinal ordering agrees with natural number ordering. (Contributed by NM, 17-Jun-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≺ 𝐵 ↔ 𝐴 ⊊ 𝐵)) | ||
Theorem | sucdom2 8156 | 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 8157 | 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 8158 | Strict dominance over zero is the same as dominance over one. (Contributed by NM, 28-Sep-2004.) |
⊢ (∅ ≺ 𝐴 ↔ 1𝑜 ≼ 𝐴) | ||
Theorem | 1sdom2 8159 | Ordinal 1 is strictly dominated by ordinal 2. (Contributed by NM, 4-Apr-2007.) |
⊢ 1𝑜 ≺ 2𝑜 | ||
Theorem | sdom1 8160 | A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (𝐴 ≺ 1𝑜 ↔ 𝐴 = ∅) | ||
Theorem | modom 8161 | Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (∃*𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≼ 1𝑜) | ||
Theorem | modom2 8162* | Two ways to express "at most one". (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 ≼ 1𝑜) | ||
Theorem | 1sdom 8163* | A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom 8029.) (Contributed by Mario Carneiro, 12-Jan-2013.) |
⊢ (𝐴 ∈ 𝑉 → (1𝑜 ≺ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)) | ||
Theorem | unxpdomlem1 8164* | Lemma for unxpdom 8167. (Trivial substitution proof.) (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) ⇒ ⊢ (𝑧 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉)) | ||
Theorem | unxpdomlem2 8165* | Lemma for unxpdom 8167. (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) & ⊢ (𝜑 → 𝑤 ∈ (𝑎 ∪ 𝑏)) & ⊢ (𝜑 → ¬ 𝑚 = 𝑛) & ⊢ (𝜑 → ¬ 𝑠 = 𝑡) ⇒ ⊢ ((𝜑 ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) | ||
Theorem | unxpdomlem3 8166* | Lemma for unxpdom 8167. (Contributed by Mario Carneiro, 13-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) & ⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) ⇒ ⊢ ((1𝑜 ≺ 𝑎 ∧ 1𝑜 ≺ 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)) | ||
Theorem | unxpdom 8167 | 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 8168 | Corollary of unxpdom 8167. (Contributed by NM, 16-Sep-2004.) |
⊢ ((1𝑜 ≺ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≼ (𝐴 × 𝐴)) | ||
Theorem | sucxpdom 8169 | 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 8170 | 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 8171 | A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵) | ||
Theorem | ominf 8172 | The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.) |
⊢ ¬ ω ∈ Fin | ||
Theorem | isinf 8173* | 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 8174 | Lemma for fineqv 8175. (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 8175 | 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 8176 | Equinumerous sets have the same finiteness. (Contributed by NM, 22-Aug-2008.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin)) | ||
Theorem | enfii 8177 | A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin) | ||
Theorem | pssnn 8178* | 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 8179 | A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
Theorem | ssfi 8180 | A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. (Contributed by NM, 24-Jun-1998.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) | ||
Theorem | domfi 8181 | 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 8182 | 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 8183 | A subset of a finite set is finite, deduction version of ssfi 8180. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ Fin) | ||
Theorem | infi 8184 | The intersection of two sets is finite if one of them is. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (𝐴 ∈ Fin → (𝐴 ∩ 𝐵) ∈ Fin) | ||
Theorem | rabfi 8185* | A restricted class built from a finite set is finite. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (𝐴 ∈ Fin → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ Fin) | ||
Theorem | finresfin 8186 | The restriction of a finite set is finite. (Contributed by Alexander van der Vekens, 3-Jan-2018.) |
⊢ (𝐸 ∈ Fin → (𝐸 ↾ 𝐵) ∈ Fin) | ||
Theorem | f1finf1o 8187 | 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 8188 | The empty set is finite. (Contributed by FL, 14-Jul-2008.) |
⊢ ∅ ∈ Fin | ||
Theorem | nfielex 8189* | If a class is not finite, it contains at least one element. (Contributed by Alexander van der Vekens, 12-Jan-2018.) |
⊢ (¬ 𝐴 ∈ Fin → ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | en1eqsn 8190 | A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1𝑜) → 𝐵 = {𝐴}) | ||
Theorem | en1eqsnbi 8191 | A set containing an element has exactly one element iff it is a singleton. Formerly part of proof for rngen1zr 19276. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
⊢ (𝐴 ∈ 𝐵 → (𝐵 ≈ 1𝑜 ↔ 𝐵 = {𝐴})) | ||
Theorem | diffi 8192 | If 𝐴 is finite, (𝐴 ∖ 𝐵) is finite. (Contributed by FL, 3-Aug-2009.) |
⊢ (𝐴 ∈ Fin → (𝐴 ∖ 𝐵) ∈ Fin) | ||
Theorem | dif1en 8193 | 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 8194 | Lemma for uses of enp1i 8195. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 𝑇 = ({𝑥} ∪ 𝑆) ⇒ ⊢ (𝑥 ∈ 𝐴 → ((𝐴 ∖ {𝑥}) = 𝑆 → 𝐴 = 𝑇)) | ||
Theorem | enp1i 8195* | Proof induction for en2i 7993 and related theorems. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 𝑀 ∈ ω & ⊢ 𝑁 = suc 𝑀 & ⊢ ((𝐴 ∖ {𝑥}) ≈ 𝑀 → 𝜑) & ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (𝐴 ≈ 𝑁 → ∃𝑥𝜓) | ||
Theorem | en2 8196* | A set equinumerous to ordinal 2 is a pair. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 2𝑜 → ∃𝑥∃𝑦 𝐴 = {𝑥, 𝑦}) | ||
Theorem | en3 8197* | A set equinumerous to ordinal 3 is a triple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 3𝑜 → ∃𝑥∃𝑦∃𝑧 𝐴 = {𝑥, 𝑦, 𝑧}) | ||
Theorem | en4 8198* | A set equinumerous to ordinal 4 is a quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (𝐴 ≈ 4𝑜 → ∃𝑥∃𝑦∃𝑧∃𝑤 𝐴 = ({𝑥, 𝑦} ∪ {𝑧, 𝑤})) | ||
Theorem | findcard 8199* | 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 8200* | 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 → 𝜏) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |