Home | Metamath
Proof Explorer Theorem List (p. 131 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 | focdmex 13001 | 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 13002* | 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 13003* | Obsolete version of hasheqf1oi 13002 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 13004 | 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 13005 | Obsolete version of hashf1rn 13004 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 13006 | 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 13007 | 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 13008 | 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 13009 | Closure of the # function. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 13-Jul-2014.) |
⊢ (𝐴 ∈ Fin → (#‘𝐴) ∈ ℕ0) | ||
Theorem | hashxrcl 13010 | Extended real closure of the # function. (Contributed by Mario Carneiro, 22-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (#‘𝐴) ∈ ℝ*) | ||
Theorem | hashclb 13011 | Reverse closure of the # function. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ (#‘𝐴) ∈ ℕ0)) | ||
Theorem | hashvnfin 13012 | A set of finite size is a finite set. (Contributed by Alexander van der Vekens, 8-Dec-2017.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((#‘𝑆) = 𝑁 → 𝑆 ∈ Fin)) | ||
Theorem | hashnfinnn0 13013 | 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 13014 | 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 13015 | 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 13016 | Two ways of saying a set is not empty. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
⊢ (𝐴 ∈ 𝑉 → (0 < (#‘𝐴) ↔ 𝐴 ≠ ∅)) | ||
Theorem | hashgt0n0 13017 | 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 13018 | Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) | ||
Theorem | hash0 13019 | The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.) |
⊢ (#‘∅) = 0 | ||
Theorem | hashsng 13020 | The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 13-Feb-2013.) |
⊢ (𝐴 ∈ 𝑉 → (#‘{𝐴}) = 1) | ||
Theorem | hashen1 13021 | A set with only one element is equinumerous to the ordinal number 1. (Contributed by AV, 14-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → ((#‘𝐴) = 1 ↔ 𝐴 ≈ 1𝑜)) | ||
Theorem | hashrabrsn 13022* | 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 13023* | 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 13024* | 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 13025 | A function is equinumerous to its domain. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ (𝐹 Fn 𝐴 → (#‘𝐹) = (#‘𝐴)) | ||
Theorem | fseq1hash 13026 | 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 13027 | 𝐺 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 13028 | A short expression for the 𝐺 function of hashgf1o 12632. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ (# ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) | ||
Theorem | hashdom 13029 | Dominance relation for the size function. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 22-Apr-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → ((#‘𝐴) ≤ (#‘𝐵) ↔ 𝐴 ≼ 𝐵)) | ||
Theorem | hashdomi 13030 | Non-strict order relation of the # function on the full cardinal poset. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ (𝐴 ≼ 𝐵 → (#‘𝐴) ≤ (#‘𝐵)) | ||
Theorem | hashsdom 13031 | Strict dominance relation for the size function. (Contributed by Mario Carneiro, 18-Aug-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘𝐴) < (#‘𝐵) ↔ 𝐴 ≺ 𝐵)) | ||
Theorem | hashun 13032 | 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 13033 | 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 13034 | 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 13035 | 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 13036 | The size of the union of disjoint sets is the result of the extended real addition of their sizes, analogous to hashun 13032. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (#‘(𝐴 ∪ 𝐵)) = ((#‘𝐴) +𝑒 (#‘𝐵))) | ||
Theorem | hashge0 13037 | The cardinality of a set is greater than or equal to zero. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
⊢ (𝐴 ∈ 𝑉 → 0 ≤ (#‘𝐴)) | ||
Theorem | hashgt0 13038 | The cardinality of a nonempty set is greater than zero. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → 0 < (#‘𝐴)) | ||
Theorem | hashge1 13039 | The cardinality of a nonempty set is greater or equal to one. (Contributed by Thierry Arnoux, 20-Jun-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → 1 ≤ (#‘𝐴)) | ||
Theorem | 1elfz0hash 13040 | 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 13041 | 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 13042 | 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 13043 | 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 13044 | Obsolete version of hashprg 13043 as of 18-Sep-2021. (Contributed by Mario Carneiro, 27-Sep-2013.) (Revised by Mario Carneiro, 5-May-2016.) TODO-AV: to be removed after revision of graph theory! (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 ↔ (#‘{𝐴, 𝐵}) = 2)) | ||
Theorem | elprchashprn2 13045 | 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 13046 | 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 13047 | The elements of an unordered pair of size 2 are different sets. (Contributed by AV, 27-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} ⇒ ⊢ ((#‘𝑆) = 2 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵)) | ||
Theorem | prhash2ex 13048 | There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 13057, 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 13049 | 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 13050* | 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 13051* | 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 13052 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 𝐴 ∈ ω & ⊢ 𝐵 = suc 𝐴 & ⊢ (#‘𝐴) = 𝑀 & ⊢ (𝑀 + 1) = 𝑁 ⇒ ⊢ (#‘𝐵) = 𝑁 | ||
Theorem | hash1 13053 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (#‘1𝑜) = 1 | ||
Theorem | hash2 13054 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (#‘2𝑜) = 2 | ||
Theorem | hash3 13055 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (#‘3𝑜) = 3 | ||
Theorem | hash4 13056 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ (#‘4𝑜) = 4 | ||
Theorem | pr0hash2ex 13057 | 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 13058 | 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 13059 | The size of a superset of a proper unordered pair is greater than 1. (Contributed by AV, 6-Feb-2021.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ∈ 𝑈) → ({𝐴, 𝐵} ⊆ 𝐶 → 2 ≤ (#‘𝐶))) | ||
Theorem | hashin 13060 | 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 13061 | 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 ∧ 𝐵 ⊆ 𝐴) → (#‘(𝐴 ∖ 𝐵)) = ((#‘𝐴) − (#‘𝐵))) | ||
Theorem | hashdif 13062 | The size of the difference of a finite set and another set is the first set's size minus that of the intersection of both. (Contributed by Steve Rodriguez, 24-Oct-2015.) |
⊢ (𝐴 ∈ Fin → (#‘(𝐴 ∖ 𝐵)) = ((#‘𝐴) − (#‘(𝐴 ∩ 𝐵)))) | ||
Theorem | hashdifsn 13063 | The size of the difference of a finite set and a singleton subset is the set's size minus 1. (Contributed by Alexander van der Vekens, 6-Jan-2018.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) → (#‘(𝐴 ∖ {𝐵})) = ((#‘𝐴) − 1)) | ||
Theorem | hashdifpr 13064 | The size of the difference of a finite set and a proper ordered pair subset is the set's size minus 2. (Contributed by AV, 16-Dec-2020.) |
⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶)) → (#‘(𝐴 ∖ {𝐵, 𝐶})) = ((#‘𝐴) − 2)) | ||
Theorem | hashsn01 13065 | The size of a singleton is either 0 or 1. (Contributed by AV, 23-Feb-2021.) |
⊢ ((#‘{𝐴}) = 0 ∨ (#‘{𝐴}) = 1) | ||
Theorem | hashsnle1 13066 | The size of a singleton is less than or equal to 1. (Contributed by AV, 23-Feb-2021.) |
⊢ (#‘{𝐴}) ≤ 1 | ||
Theorem | hashsnlei 13067 | Get an upper bound on a concretely specified finite set. Base case: singleton set. (Contributed by Mario Carneiro, 11-Feb-2015.) (Proof shortened by AV, 23-Feb-2021.) |
⊢ ({𝐴} ∈ Fin ∧ (#‘{𝐴}) ≤ 1) | ||
Theorem | hash1snb 13068* | The size of a set is 1 if and only if it is a singleton (containing a set). (Contributed by Alexander van der Vekens, 7-Dec-2017.) |
⊢ (𝑉 ∈ 𝑊 → ((#‘𝑉) = 1 ↔ ∃𝑎 𝑉 = {𝑎})) | ||
Theorem | euhash1 13069* | The size of a set is 1 in terms of existential uniqueness. (Contributed by Alexander van der Vekens, 8-Feb-2018.) |
⊢ (𝑉 ∈ 𝑊 → ((#‘𝑉) = 1 ↔ ∃!𝑎 𝑎 ∈ 𝑉)) | ||
Theorem | hashgt12el 13070* | In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (#‘𝑉)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑎 ≠ 𝑏) | ||
Theorem | hashgt12el2 13071* | In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (#‘𝑉) ∧ 𝐴 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏) | ||
Theorem | hashunlei 13072 | Get an upper bound on a concretely specified finite set. Induction step: union of two finite bounded sets. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐶 = (𝐴 ∪ 𝐵) & ⊢ (𝐴 ∈ Fin ∧ (#‘𝐴) ≤ 𝐾) & ⊢ (𝐵 ∈ Fin ∧ (#‘𝐵) ≤ 𝑀) & ⊢ 𝐾 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 & ⊢ (𝐾 + 𝑀) = 𝑁 ⇒ ⊢ (𝐶 ∈ Fin ∧ (#‘𝐶) ≤ 𝑁) | ||
Theorem | hashsslei 13073 | Get an upper bound on a concretely specified finite set. Transfer boundedness to a subset. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝐵 ⊆ 𝐴 & ⊢ (𝐴 ∈ Fin ∧ (#‘𝐴) ≤ 𝑁) & ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ (𝐵 ∈ Fin ∧ (#‘𝐵) ≤ 𝑁) | ||
Theorem | hashfz 13074 | Value of the numeric cardinality of a nonempty integer range. (Contributed by Stefan O'Rear, 12-Sep-2014.) (Proof shortened by Mario Carneiro, 15-Apr-2015.) |
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (#‘(𝐴...𝐵)) = ((𝐵 − 𝐴) + 1)) | ||
Theorem | fzsdom2 13075 | Condition for finite ranges to have a strict dominance relation. (Contributed by Stefan O'Rear, 12-Sep-2014.) (Revised by Mario Carneiro, 15-Apr-2015.) |
⊢ (((𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐶 ∈ ℤ) ∧ 𝐵 < 𝐶) → (𝐴...𝐵) ≺ (𝐴...𝐶)) | ||
Theorem | hashfzo 13076 | Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (#‘(𝐴..^𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | hashfzo0 13077 | Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ (𝐵 ∈ ℕ0 → (#‘(0..^𝐵)) = 𝐵) | ||
Theorem | hashfzp1 13078 | Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021.) |
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (#‘((𝐴 + 1)...𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | hashfz0 13079 | Value of the numeric cardinality of a nonempty range of nonnegative integers. (Contributed by Alexander van der Vekens, 21-Jul-2018.) |
⊢ (𝐵 ∈ ℕ0 → (#‘(0...𝐵)) = (𝐵 + 1)) | ||
Theorem | hashxplem 13080 | Lemma for hashxp 13081. (Contributed by Paul Chapman, 30-Nov-2012.) |
⊢ 𝐵 ∈ Fin ⇒ ⊢ (𝐴 ∈ Fin → (#‘(𝐴 × 𝐵)) = ((#‘𝐴) · (#‘𝐵))) | ||
Theorem | hashxp 13081 | The size of the Cartesian product of two finite sets is the product of their sizes. (Contributed by Paul Chapman, 30-Nov-2012.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (#‘(𝐴 × 𝐵)) = ((#‘𝐴) · (#‘𝐵))) | ||
Theorem | hashmap 13082 | The size of the set exponential of two finite sets is the exponential of their sizes. (This is the original motivation behind the notation for set exponentiation.) (Contributed by Mario Carneiro, 5-Aug-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (#‘(𝐴 ↑𝑚 𝐵)) = ((#‘𝐴)↑(#‘𝐵))) | ||
Theorem | hashpw 13083 | The size of the power set of a finite set is 2 raised to the power of the size of the set. (Contributed by Paul Chapman, 30-Nov-2012.) (Proof shortened by Mario Carneiro, 5-Aug-2014.) |
⊢ (𝐴 ∈ Fin → (#‘𝒫 𝐴) = (2↑(#‘𝐴))) | ||
Theorem | hashfun 13084 | A finite set is a function iff it is equinumerous to its domain. (Contributed by Mario Carneiro, 26-Sep-2013.) (Revised by Mario Carneiro, 12-Mar-2015.) |
⊢ (𝐹 ∈ Fin → (Fun 𝐹 ↔ (#‘𝐹) = (#‘dom 𝐹))) | ||
Theorem | hashimarn 13085 | The size of the image of a one-to-one function 𝐸 under the range of a function 𝐹 which is a one-to-one function into the domain of 𝐸 equals the size of the function 𝐹. (Contributed by Alexander van der Vekens, 4-Feb-2018.) (Proof shortened by AV, 4-May-2021.) |
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) → (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 → (#‘(𝐸 “ ran 𝐹)) = (#‘𝐹))) | ||
Theorem | hashimarni 13086 | If the size of the image of a one-to-one function 𝐸 under the range of a function 𝐹 which is a one-to-one function into the domain of 𝐸 is a nonnegative integer, the size of the function 𝐹 is the same nonnegative integer. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ 𝐸 ∈ 𝑉) → ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃 = (𝐸 “ ran 𝐹) ∧ (#‘𝑃) = 𝑁) → (#‘𝐹) = 𝑁)) | ||
Theorem | fnfz0hash 13087 | The size of a function on a finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 25-Jun-2018.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (0...𝑁)) → (#‘𝐹) = (𝑁 + 1)) | ||
Theorem | ffz0hash 13088 | The size of a function on a finite set of sequential nonnegative integers equals the upper bound of the sequence increased by 1. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Proof shortened by AV, 11-Apr-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶𝐵) → (#‘𝐹) = (𝑁 + 1)) | ||
Theorem | fnfz0hashnn0 13089 | The size of a function on a finite set of sequential nonnegative integers is a nonnegative integer. (Contributed by AV, 10-Apr-2021.) |
⊢ (𝐹 Fn (0...𝑁) → (#‘𝐹) ∈ ℕ0) | ||
Theorem | ffzo0hash 13090 | The size of a function on a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 25-Mar-2018.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (0..^𝑁)) → (#‘𝐹) = 𝑁) | ||
Theorem | fnfzo0hash 13091 | The size of a function on a half-open range of nonnegative integers equals the upper bound of this range. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Proof shortened by AV, 11-Apr-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0..^𝑁)⟶𝐵) → (#‘𝐹) = 𝑁) | ||
Theorem | fnfzo0hashnn0 13092 | The value of the size function on a half-open range of nonnegative integers is a nonnegative integer. (Contributed by AV, 10-Apr-2021.) |
⊢ (𝐹 Fn (0..^𝑁) → (#‘𝐹) ∈ ℕ0) | ||
Theorem | hashbclem 13093* | Lemma for hashbc 13094: inductive step. (Contributed by Mario Carneiro, 13-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) & ⊢ (𝜑 → ∀𝑗 ∈ ℤ ((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗})) & ⊢ (𝜑 → 𝐾 ∈ ℤ) ⇒ ⊢ (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾})) | ||
Theorem | hashbc 13094* | The binomial coefficient counts the number of subsets of a finite set of a given size. This is Metamath 100 proof #58 (formula for the number of combinations). (Contributed by Mario Carneiro, 13-Jul-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐾 ∈ ℤ) → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})) | ||
Theorem | hashfacen 13095* | The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷}) | ||
Theorem | hashf1lem1 13096* | Lemma for hashf1 13098. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) & ⊢ (𝜑 → ((#‘𝐴) + 1) ≤ (#‘𝐵)) & ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵) ⇒ ⊢ (𝜑 → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ≈ (𝐵 ∖ ran 𝐹)) | ||
Theorem | hashf1lem2 13097* | Lemma for hashf1 13098. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) & ⊢ (𝜑 → ((#‘𝐴) + 1) ≤ (#‘𝐵)) ⇒ ⊢ (𝜑 → (#‘{𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}))) | ||
Theorem | hashf1 13098* | The permutation number ∣ 𝐴 ∣ ! · ( ∣ 𝐵 ∣ C ∣ 𝐴 ∣ ) = ∣ 𝐵 ∣ ! / ( ∣ 𝐵 ∣ − ∣ 𝐴 ∣ )! counts the number of injections from 𝐴 to 𝐵. (Contributed by Mario Carneiro, 21-Jan-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(#‘𝐴)) · ((#‘𝐵)C(#‘𝐴)))) | ||
Theorem | hashfac 13099* | A factorial counts the number of bijections on a finite set. (Contributed by Mario Carneiro, 21-Jan-2015.) (Proof shortened by Mario Carneiro, 17-Apr-2015.) |
⊢ (𝐴 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐴}) = (!‘(#‘𝐴))) | ||
Theorem | leiso 13100 | Two ways to write a strictly increasing function on the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) → (𝐹 Isom < , < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ≤ (𝐴, 𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |