Home | Metamath
Proof Explorer Theorem List (p. 132 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 | bcnp1n 13101 | Binomial coefficient: 𝑁 + 1 choose 𝑁. (Contributed by NM, 20-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1)C𝑁) = (𝑁 + 1)) | ||
Theorem | bcm1k 13102 | The proportion of one binomial coefficient to another with 𝐾 decreased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.) |
⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾))) | ||
Theorem | bcp1n 13103 | The proportion of one binomial coefficient to another with 𝑁 increased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.) |
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C𝐾) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾)))) | ||
Theorem | bcp1nk 13104 | The proportion of one binomial coefficient to another with 𝑁 and 𝐾 increased by 1. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C(𝐾 + 1)) = ((𝑁C𝐾) · ((𝑁 + 1) / (𝐾 + 1)))) | ||
Theorem | bcval5 13105 | Write out the top and bottom parts of the binomial coefficient (𝑁C𝐾) = (𝑁 · (𝑁 − 1) · ... · ((𝑁 − 𝐾) + 1)) / 𝐾! explicitly. In this form, it is valid even for 𝑁 < 𝐾, although it is no longer valid for nonpositive 𝐾. (Contributed by Mario Carneiro, 22-May-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ) → (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾))) | ||
Theorem | bcn2 13106 | Binomial coefficient: 𝑁 choose 2. (Contributed by Mario Carneiro, 22-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C2) = ((𝑁 · (𝑁 − 1)) / 2)) | ||
Theorem | bcp1m1 13107 | Compute the binomial coefficient of (𝑁 + 1) over (𝑁 − 1) (Contributed by Scott Fenton, 11-May-2014.) (Revised by Mario Carneiro, 22-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1)C(𝑁 − 1)) = (((𝑁 + 1) · 𝑁) / 2)) | ||
Theorem | bcpasc 13108 | Pascal's rule for the binomial coefficient, generalized to all integers 𝐾. Equation 2 of [Gleason] p. 295. (Contributed by NM, 13-Jul-2005.) (Revised by Mario Carneiro, 10-Mar-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)) | ||
Theorem | bccl 13109 | A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by NM, 10-Jul-2005.) (Revised by Mario Carneiro, 9-Nov-2013.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ) → (𝑁C𝐾) ∈ ℕ0) | ||
Theorem | bccl2 13110 | A binomial coefficient, in its standard domain, is a positive integer. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 10-Mar-2014.) |
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) ∈ ℕ) | ||
Theorem | bcn2m1 13111 | Compute the binomial coefficient "𝑁 choose 2 " from "(𝑁 − 1) choose 2 ": (N-1) + ( (N-1) 2 ) = ( N 2 ). (Contributed by Alexander van der Vekens, 7-Jan-2018.) |
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + ((𝑁 − 1)C2)) = (𝑁C2)) | ||
Theorem | bcn2p1 13112 | Compute the binomial coefficient "(𝑁 + 1) choose 2 " from "𝑁 choose 2 ": N + ( N 2 ) = ( (N+1) 2 ). (Contributed by Alexander van der Vekens, 8-Jan-2018.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁 + (𝑁C2)) = ((𝑁 + 1)C2)) | ||
Theorem | permnn 13113 | The number of permutations of 𝑁 − 𝑅 objects from a collection of 𝑁 objects is a positive integer. (Contributed by Jason Orendorff, 24-Jan-2007.) |
⊢ (𝑅 ∈ (0...𝑁) → ((!‘𝑁) / (!‘𝑅)) ∈ ℕ) | ||
Theorem | bcnm1 13114 | The binomial coefficent of (𝑁 − 1) is 𝑁. (Contributed by Scott Fenton, 16-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C(𝑁 − 1)) = 𝑁) | ||
Theorem | 4bc3eq4 13115 | The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.) |
⊢ (4C3) = 4 | ||
Theorem | 4bc2eq6 13116 | The value of four choose two. (Contributed by Scott Fenton, 9-Jan-2017.) |
⊢ (4C2) = 6 | ||
Syntax | chash 13117 | Extend the definition of a class to include the set size function. |
class # | ||
Definition | df-hash 13118 | Define the set size function #, which gives the cardinality of a finite set as a member of ℕ0, and assigns all infinite sets the value +∞. For example, (#‘{0, 1, 2}) = 3 (ex-hash 27310). (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ # = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ∘ card) ∪ ((V ∖ Fin) × {+∞})) | ||
Theorem | hashkf 13119 | The finite part of the size function maps all finite sets to their cardinality, as members of ℕ0. (Contributed by Mario Carneiro, 13-Sep-2013.) (Revised by Mario Carneiro, 26-Dec-2014.) |
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) & ⊢ 𝐾 = (𝐺 ∘ card) ⇒ ⊢ 𝐾:Fin⟶ℕ0 | ||
Theorem | hashgval 13120* | The value of the # function in terms of the mapping 𝐺 from ω to ℕ0. The proof avoids the use of ax-ac 9281. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 26-Dec-2014.) |
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ⇒ ⊢ (𝐴 ∈ Fin → (𝐺‘(card‘𝐴)) = (#‘𝐴)) | ||
Theorem | hashginv 13121* | ◡𝐺 maps the size function's value to card. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ⇒ ⊢ (𝐴 ∈ Fin → (◡𝐺‘(#‘𝐴)) = (card‘𝐴)) | ||
Theorem | hashinf 13122 | The value of the # function on an infinite set. (Contributed by Mario Carneiro, 13-Jul-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (#‘𝐴) = +∞) | ||
Theorem | hashbnd 13123 | If 𝐴 has size bounded by an integer 𝐵, then 𝐴 is finite. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ℕ0 ∧ (#‘𝐴) ≤ 𝐵) → 𝐴 ∈ Fin) | ||
Theorem | hashfxnn0 13124 | The size function is a function into the extended nonnegative integers. (Contributed by Mario Carneiro, 13-Sep-2013.) (Revised by AV, 10-Dec-2020.) |
⊢ #:V⟶ℕ0* | ||
Theorem | hashf 13125 | The size function maps all finite sets to their cardinality, as members of ℕ0, and infinite sets to +∞. TODO-AV: mark as OBSOLETE and replace it by hashfxnn0 13124? (Contributed by Mario Carneiro, 13-Sep-2013.) (Revised by Mario Carneiro, 13-Jul-2014.) (Proof shortened by AV, 24-Oct-2021.) |
⊢ #:V⟶(ℕ0 ∪ {+∞}) | ||
Theorem | hashfOLD 13126 | Obsolete version of hashf 13125 as of 24-Oct-2021. The size function maps all finite sets to their cardinality, as members of ℕ0, and infinite sets to +∞. (Contributed by Mario Carneiro, 13-Sep-2013.) (Revised by Mario Carneiro, 13-Jul-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ #:V⟶(ℕ0 ∪ {+∞}) | ||
Theorem | hashxnn0 13127 | The value of the hash function for a set is an extended nonnegative integer. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 10-Dec-2020.) |
⊢ (𝑀 ∈ 𝑉 → (#‘𝑀) ∈ ℕ0*) | ||
Theorem | hashresfn 13128 | Restriction of the domain of the size function. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (# ↾ 𝐴) Fn 𝐴 | ||
Theorem | dmhashres 13129 | Restriction of the domain of the size function. (Contributed by Thierry Arnoux, 12-Jan-2017.) |
⊢ dom (# ↾ 𝐴) = 𝐴 | ||
Theorem | hashnn0pnf 13130 | The value of the hash function for a set is either a nonnegative integer or positive infinity. TODO-AV: mark as OBSOLETE and replace it by hashxnn0 13127? (Contributed by Alexander van der Vekens, 6-Dec-2017.) |
⊢ (𝑀 ∈ 𝑉 → ((#‘𝑀) ∈ ℕ0 ∨ (#‘𝑀) = +∞)) | ||
Theorem | hashnnn0genn0 13131 | If the size of a set is not a nonnegative integer, it is greater than or equal to any nonnegative integer. (Contributed by Alexander van der Vekens, 6-Dec-2017.) |
⊢ ((𝑀 ∈ 𝑉 ∧ (#‘𝑀) ∉ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ≤ (#‘𝑀)) | ||
Theorem | hashnemnf 13132 | The size of a set is never minus infinity. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
⊢ (𝐴 ∈ 𝑉 → (#‘𝐴) ≠ -∞) | ||
Theorem | hashv01gt1 13133 | The size of a set is either 0 or 1 or greater than 1. (Contributed by Alexander van der Vekens, 29-Dec-2017.) |
⊢ (𝑀 ∈ 𝑉 → ((#‘𝑀) = 0 ∨ (#‘𝑀) = 1 ∨ 1 < (#‘𝑀))) | ||
Theorem | hashfz1 13134 | The set (1...𝑁) has 𝑁 elements. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ (𝑁 ∈ ℕ0 → (#‘(1...𝑁)) = 𝑁) | ||
Theorem | hashen 13135 | Two finite sets have the same number of elements iff they are equinumerous. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘𝐴) = (#‘𝐵) ↔ 𝐴 ≈ 𝐵)) | ||
Theorem | hasheni 13136 | Equinumerous sets have the same number of elements (even if they are not finite). (Contributed by Mario Carneiro, 15-Apr-2015.) |
⊢ (𝐴 ≈ 𝐵 → (#‘𝐴) = (#‘𝐵)) | ||
Theorem | hasheqf1o 13137* | The size of two finite sets is equal if and only if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 17-Dec-2017.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘𝐴) = (#‘𝐵) ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)) | ||
Theorem | fiinfnf1o 13138* | There is no bijection between a finite set and an infinite set. (Contributed by Alexander van der Vekens, 25-Dec-2017.) |
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ¬ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) | ||
Theorem | focdmex 13139 | The codomain of an onto function is a set if its domain is a set. (Contributed by AV, 4-May-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ V) | ||
Theorem | hasheqf1oi 13140* | The size of two sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 25-Dec-2017.) (Revised by AV, 4-May-2021.) |
⊢ (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (#‘𝐴) = (#‘𝐵))) | ||
Theorem | hasheqf1oiOLD 13141* | Obsolete version of hasheqf1oi 13140 as of 4-May-2021. (Contributed by Alexander van der Vekens, 25-Dec-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (#‘𝐴) = (#‘𝐵))) | ||
Theorem | hashf1rn 13142 | The size of a finite set which is a one-to-one function is equal to the size of the function's range. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 4-May-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (#‘𝐹) = (#‘ran 𝐹)) | ||
Theorem | hashf1rnOLD 13143 | Obsolete version of hashf1rn 13142 as of 4-May-2021. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by Alexander van der Vekens, 4-Feb-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹:𝐴–1-1→𝐵 → (#‘𝐹) = (#‘ran 𝐹))) | ||
Theorem | hasheqf1od 13144 | The size of two sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by AV, 4-May-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) ⇒ ⊢ (𝜑 → (#‘𝐴) = (#‘𝐵)) | ||
Theorem | fz1eqb 13145 | Two possibly-empty 1-based finite sets of sequential integers are equal iff their endpoints are equal. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 29-Mar-2014.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((1...𝑀) = (1...𝑁) ↔ 𝑀 = 𝑁)) | ||
Theorem | hashcard 13146 | The size function of the cardinality function. (Contributed by Mario Carneiro, 19-Sep-2013.) (Revised by Mario Carneiro, 4-Nov-2013.) |
⊢ (𝐴 ∈ Fin → (#‘(card‘𝐴)) = (#‘𝐴)) | ||
Theorem | hashcl 13147 | Closure of the # function. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 13-Jul-2014.) |
⊢ (𝐴 ∈ Fin → (#‘𝐴) ∈ ℕ0) | ||
Theorem | hashxrcl 13148 | Extended real closure of the # function. (Contributed by Mario Carneiro, 22-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (#‘𝐴) ∈ ℝ*) | ||
Theorem | hashclb 13149 | Reverse closure of the # function. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ (#‘𝐴) ∈ ℕ0)) | ||
Theorem | nfile 13150 | The size of any infinite set is always greater than or equal to the size of any set. (Contributed by AV, 13-Nov-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ Fin) → (#‘𝐴) ≤ (#‘𝐵)) | ||
Theorem | hashvnfin 13151 | A set of finite size is a finite set. (Contributed by Alexander van der Vekens, 8-Dec-2017.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((#‘𝑆) = 𝑁 → 𝑆 ∈ Fin)) | ||
Theorem | hashnfinnn0 13152 | The size of an infinite set is not a nonnegative integer. (Contributed by Alexander van der Vekens, 21-Dec-2017.) (Proof shortened by Alexander van der Vekens, 18-Jan-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (#‘𝐴) ∉ ℕ0) | ||
Theorem | isfinite4 13153 | A finite set is equinumerous to the range of integers from one up to the hash value of the set. In other words, counting objects with natural numbers works if and only if it is a finite collection. (Contributed by Richard Penner, 26-Feb-2020.) |
⊢ (𝐴 ∈ Fin ↔ (1...(#‘𝐴)) ≈ 𝐴) | ||
Theorem | hasheq0 13154 | Two ways of saying a finite set is empty. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 27-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → ((#‘𝐴) = 0 ↔ 𝐴 = ∅)) | ||
Theorem | hashneq0 13155 | Two ways of saying a set is not empty. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
⊢ (𝐴 ∈ 𝑉 → (0 < (#‘𝐴) ↔ 𝐴 ≠ ∅)) | ||
Theorem | hashgt0n0 13156 | If the size of a set is greater than 0, the set is not empty. (Contributed by AV, 5-Aug-2018.) (Prove shortened by AV, 18-Nov-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 0 < (#‘𝐴)) → 𝐴 ≠ ∅) | ||
Theorem | hashnncl 13157 | Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) | ||
Theorem | hash0 13158 | The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.) |
⊢ (#‘∅) = 0 | ||
Theorem | hashsng 13159 | The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 13-Feb-2013.) |
⊢ (𝐴 ∈ 𝑉 → (#‘{𝐴}) = 1) | ||
Theorem | hashen1 13160 | A set with only one element is equinumerous to the ordinal number 1. (Contributed by AV, 14-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → ((#‘𝐴) = 1 ↔ 𝐴 ≈ 1𝑜)) | ||
Theorem | hashrabrsn 13161* | The size of a restricted class abstraction restricted to a singleton is a nonnegative integer. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |
⊢ (#‘{𝑥 ∈ {𝐴} ∣ 𝜑}) ∈ ℕ0 | ||
Theorem | hashrabsn01 13162* | The size of a restricted class abstraction restricted to a singleton is either 0 or 1. (Contributed by Alexander van der Vekens, 3-Sep-2018.) |
⊢ ((#‘{𝑥 ∈ {𝐴} ∣ 𝜑}) = 𝑁 → (𝑁 = 0 ∨ 𝑁 = 1)) | ||
Theorem | hashrabsn1 13163* | If the size of a restricted class abstraction restricted to a singleton is 1, the condition of the class abstraction must hold for the singleton. (Contributed by Alexander van der Vekens, 3-Sep-2018.) |
⊢ ((#‘{𝑥 ∈ {𝐴} ∣ 𝜑}) = 1 → [𝐴 / 𝑥]𝜑) | ||
Theorem | hashfn 13164 | A function is equinumerous to its domain. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ (𝐹 Fn 𝐴 → (#‘𝐹) = (#‘𝐴)) | ||
Theorem | fseq1hash 13165 | The value of the size function on a finite 1-based sequence. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 12-Mar-2015.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (1...𝑁)) → (#‘𝐹) = 𝑁) | ||
Theorem | hashgadd 13166 | 𝐺 maps ordinal addition to integer addition. (Contributed by Paul Chapman, 30-Nov-2012.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐺‘(𝐴 +𝑜 𝐵)) = ((𝐺‘𝐴) + (𝐺‘𝐵))) | ||
Theorem | hashgval2 13167 | A short expression for the 𝐺 function of hashgf1o 12770. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ (# ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) | ||
Theorem | hashdom 13168 | Dominance relation for the size function. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 22-Apr-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → ((#‘𝐴) ≤ (#‘𝐵) ↔ 𝐴 ≼ 𝐵)) | ||
Theorem | hashdomi 13169 | Non-strict order relation of the # function on the full cardinal poset. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ (𝐴 ≼ 𝐵 → (#‘𝐴) ≤ (#‘𝐵)) | ||
Theorem | hashsdom 13170 | Strict dominance relation for the size function. (Contributed by Mario Carneiro, 18-Aug-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘𝐴) < (#‘𝐵) ↔ 𝐴 ≺ 𝐵)) | ||
Theorem | hashun 13171 | The size of the union of disjoint finite sets is the sum of their sizes. (Contributed by Paul Chapman, 30-Nov-2012.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (#‘(𝐴 ∪ 𝐵)) = ((#‘𝐴) + (#‘𝐵))) | ||
Theorem | hashun2 13172 | The size of the union of finite sets is less than or equal to the sum of their sizes. (Contributed by Mario Carneiro, 23-Sep-2013.) (Proof shortened by Mario Carneiro, 27-Jul-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (#‘(𝐴 ∪ 𝐵)) ≤ ((#‘𝐴) + (#‘𝐵))) | ||
Theorem | hashun3 13173 | The size of the union of finite sets is the sum of their sizes minus the size of the intersection. (Contributed by Mario Carneiro, 6-Aug-2017.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (#‘(𝐴 ∪ 𝐵)) = (((#‘𝐴) + (#‘𝐵)) − (#‘(𝐴 ∩ 𝐵)))) | ||
Theorem | hashinfxadd 13174 | The extended real addition of the size of an infinite set with the size of an arbitrary set yields plus infinity. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (#‘𝐴) ∉ ℕ0) → ((#‘𝐴) +𝑒 (#‘𝐵)) = +∞) | ||
Theorem | hashunx 13175 | The size of the union of disjoint sets is the result of the extended real addition of their sizes, analogous to hashun 13171. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (#‘(𝐴 ∪ 𝐵)) = ((#‘𝐴) +𝑒 (#‘𝐵))) | ||
Theorem | hashge0 13176 | The cardinality of a set is greater than or equal to zero. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
⊢ (𝐴 ∈ 𝑉 → 0 ≤ (#‘𝐴)) | ||
Theorem | hashgt0 13177 | The cardinality of a nonempty set is greater than zero. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → 0 < (#‘𝐴)) | ||
Theorem | hashge1 13178 | The cardinality of a nonempty set is greater or equal to one. (Contributed by Thierry Arnoux, 20-Jun-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → 1 ≤ (#‘𝐴)) | ||
Theorem | 1elfz0hash 13179 | 1 is an element of the finite set of sequential nonnegative integers bounded by the size of a nonempty finite set. (Contributed by AV, 9-May-2020.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → 1 ∈ (0...(#‘𝐴))) | ||
Theorem | hashnn0n0nn 13180 | If a nonnegative integer is the size of a set which contains at least one element, this integer is a positive integer. (Contributed by Alexander van der Vekens, 9-Jan-2018.) |
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑌 ∈ ℕ0) ∧ ((#‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉)) → 𝑌 ∈ ℕ) | ||
Theorem | hashunsng 13181 | The size of the union of a finite set with a disjoint singleton is one more than the size of the set. (Contributed by Paul Chapman, 30-Nov-2012.) |
⊢ (𝐵 ∈ 𝑉 → ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ 𝐴) → (#‘(𝐴 ∪ {𝐵})) = ((#‘𝐴) + 1))) | ||
Theorem | hashprg 13182 | The size of an unordered pair. (Contributed by Mario Carneiro, 27-Sep-2013.) (Revised by Mario Carneiro, 5-May-2016.) (Revised by AV, 18-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≠ 𝐵 ↔ (#‘{𝐴, 𝐵}) = 2)) | ||
Theorem | hashprgOLD 13183 | Obsolete version of hashprg 13182 as of 18-Sep-2021. (Contributed by Mario Carneiro, 27-Sep-2013.) (Revised by Mario Carneiro, 5-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 ↔ (#‘{𝐴, 𝐵}) = 2)) | ||
Theorem | elprchashprn2 13184 | If one element of an unordered pair is not a set, the size of the unordered pair is not 2. (Contributed by Alexander van der Vekens, 7-Oct-2017.) |
⊢ (¬ 𝑀 ∈ V → ¬ (#‘{𝑀, 𝑁}) = 2) | ||
Theorem | hashprb 13185 | The size of an unordered pair is 2 if and only if its elements are different sets. (Contributed by Alexander van der Vekens, 17-Jan-2018.) |
⊢ ((𝑀 ∈ V ∧ 𝑁 ∈ V ∧ 𝑀 ≠ 𝑁) ↔ (#‘{𝑀, 𝑁}) = 2) | ||
Theorem | hashprdifel 13186 | The elements of an unordered pair of size 2 are different sets. (Contributed by AV, 27-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} ⇒ ⊢ ((#‘𝑆) = 2 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵)) | ||
Theorem | prhash2ex 13187 | There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 13196, numbers are used instead of sets because their representation is shorter (and more comprehensive). (Contributed by AV, 29-Jan-2020.) |
⊢ (#‘{0, 1}) = 2 | ||
Theorem | hashle00 13188 | If the size of a set is less than or equal to zero, the set must be empty. (Contributed by Alexander van der Vekens, 6-Jan-2018.) (Proof shortened by AV, 24-Oct-2021.) |
⊢ (𝑉 ∈ 𝑊 → ((#‘𝑉) ≤ 0 ↔ 𝑉 = ∅)) | ||
Theorem | hashgt0elex 13189* | If the size of a set is greater than zero, the set must contain at least one element. (Contributed by Alexander van der Vekens, 6-Jan-2018.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 0 < (#‘𝑉)) → ∃𝑥 𝑥 ∈ 𝑉) | ||
Theorem | hashgt0elexb 13190* | The size of a set is greater than zero if and only if the set contains at least one element. (Contributed by Alexander van der Vekens, 18-Jan-2018.) |
⊢ (𝑉 ∈ 𝑊 → (0 < (#‘𝑉) ↔ ∃𝑥 𝑥 ∈ 𝑉)) | ||
Theorem | hashp1i 13191 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 𝐴 ∈ ω & ⊢ 𝐵 = suc 𝐴 & ⊢ (#‘𝐴) = 𝑀 & ⊢ (𝑀 + 1) = 𝑁 ⇒ ⊢ (#‘𝐵) = 𝑁 | ||
Theorem | hash1 13192 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (#‘1𝑜) = 1 | ||
Theorem | hash2 13193 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (#‘2𝑜) = 2 | ||
Theorem | hash3 13194 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (#‘3𝑜) = 3 | ||
Theorem | hash4 13195 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (#‘4𝑜) = 4 | ||
Theorem | pr0hash2ex 13196 | There is (at least) one set with two different elements: the unordered pair containing the empty set and the singleton containing the empty set. (Contributed by AV, 29-Jan-2020.) |
⊢ (#‘{∅, {∅}}) = 2 | ||
Theorem | hashss 13197 | The size of a subset is less than or equal to the size of its superset. (Contributed by Alexander van der Vekens, 14-Jul-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (#‘𝐵) ≤ (#‘𝐴)) | ||
Theorem | prsshashgt1 13198 | The size of a superset of a proper unordered pair is greater than 1. (Contributed by AV, 6-Feb-2021.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ∈ 𝑈) → ({𝐴, 𝐵} ⊆ 𝐶 → 2 ≤ (#‘𝐶))) | ||
Theorem | hashin 13199 | The size of the intersection of a set and a class is less than or equal to the size of the set. (Contributed by AV, 4-Jan-2021.) |
⊢ (𝐴 ∈ 𝑉 → (#‘(𝐴 ∩ 𝐵)) ≤ (#‘𝐴)) | ||
Theorem | hashssdif 13200 | The size of the difference of a finite set and a subset is the set's size minus the subset's. (Contributed by Steve Rodriguez, 24-Oct-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (#‘(𝐴 ∖ 𝐵)) = ((#‘𝐴) − (#‘𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |