P. 144 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14301-14400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hashnncl 14301	Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
Theorem	hash0 14302	The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.)
⊢ (♯‘∅) = 0
Theorem	hashelne0d 14303	A set with an element has nonzero size. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ¬ (♯‘𝐴) = 0)
Theorem	hashsng 14304	The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 13-Feb-2013.)
⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1)
Theorem	hashen1 14305	A set has size 1 if and only if it is equinumerous to the ordinal 1. (Contributed by AV, 14-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 1 ↔ 𝐴 ≈ 1o))
Theorem	hash1elsn 14306	A set of size 1 with a known element is the singleton of that element. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → (♯‘𝐴) = 1)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 = {𝐵})
Theorem	hashrabrsn 14307*	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 14308*	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 14309*	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 14310	A function is equinumerous to its domain. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ (𝐹 Fn 𝐴 → (♯‘𝐹) = (♯‘𝐴))
Theorem	fseq1hash 14311	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 14312	𝐺 maps ordinal addition to integer addition. (Contributed by Paul Chapman, 30-Nov-2012.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)    ⇒   ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐺‘(𝐴 +o 𝐵)) = ((𝐺‘𝐴) + (𝐺‘𝐵)))
Theorem	hashgval2 14313	A short expression for the 𝐺 function of hashgf1o 13906. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ (♯ ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
Theorem	hashdom 14314	Dominance relation for the size function. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 22-Apr-2015.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))
Theorem	hashdomi 14315	Non-strict order relation of the ♯ function on the full cardinal poset. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ (𝐴 ≼ 𝐵 → (♯‘𝐴) ≤ (♯‘𝐵))
Theorem	hashsdom 14316	Strict dominance relation for the size function. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) < (♯‘𝐵) ↔ 𝐴 ≺ 𝐵))
Theorem	hashun 14317	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 14318	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 14319	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 14320	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 14321	The size of the union of disjoint sets is the result of the extended real addition of their sizes, analogous to hashun 14317. (Contributed by Alexander van der Vekens, 21-Dec-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (♯‘(𝐴 ∪ 𝐵)) = ((♯‘𝐴) +𝑒 (♯‘𝐵)))
Theorem	hashge0 14322	The cardinality of a set is greater than or equal to zero. (Contributed by Thierry Arnoux, 2-Mar-2017.)
⊢ (𝐴 ∈ 𝑉 → 0 ≤ (♯‘𝐴))
Theorem	hashgt0 14323	The cardinality of a nonempty set is greater than zero. (Contributed by Thierry Arnoux, 2-Mar-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → 0 < (♯‘𝐴))
Theorem	hashge1 14324	The cardinality of a nonempty set is greater than or equal to one. (Contributed by Thierry Arnoux, 20-Jun-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → 1 ≤ (♯‘𝐴))
Theorem	1elfz0hash 14325	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 14326	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 14327	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	hashunsngx 14328	The size of the union of a set with a disjoint singleton is the extended real addition of the size of the set and 1, analogous to hashunsng 14327. (Contributed by BTernaryTau, 9-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (¬ 𝐵 ∈ 𝐴 → (♯‘(𝐴 ∪ {𝐵})) = ((♯‘𝐴) +𝑒 1)))
Theorem	hashunsnggt 14329	The size of a set is greater than a nonnegative integer N if and only if the size of the union of that set with a disjoint singleton is greater than N + 1. (Contributed by BTernaryTau, 10-Sep-2023.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑁 ∈ ℕ0) ∧ ¬ 𝐵 ∈ 𝐴) → (𝑁 < (♯‘𝐴) ↔ (𝑁 + 1) < (♯‘(𝐴 ∪ {𝐵}))))
Theorem	hashprg 14330	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	elprchashprn2 14331	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 14332	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 14333	The elements of an unordered pair of size 2 are different sets. (Contributed by AV, 27-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    ⇒   ⊢ ((♯‘𝑆) = 2 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵))
Theorem	prhash2ex 14334	There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 14343, 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 14335	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 14336*	If the size of a set is greater than zero, then the set must contain at least one element. (Contributed by Alexander van der Vekens, 6-Jan-2018.)
⊢ ((𝑉 ∈ 𝑊 ∧ 0 < (♯‘𝑉)) → ∃𝑥 𝑥 ∈ 𝑉)
Theorem	hashgt0elexb 14337*	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 14338	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 = suc 𝐴    &   ⊢ (♯‘𝐴) = 𝑀    &   ⊢ (𝑀 + 1) = 𝑁    ⇒   ⊢ (♯‘𝐵) = 𝑁
Theorem	hash1 14339	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (♯‘1o) = 1
Theorem	hash2 14340	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (♯‘2o) = 2
Theorem	hash3 14341	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (♯‘3o) = 3
Theorem	hash4 14342	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (♯‘4o) = 4
Theorem	pr0hash2ex 14343	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 14344	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 14345	The size of a superset of a proper unordered pair is greater than 1. (Contributed by AV, 6-Feb-2021.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ∈ 𝑈) → ({𝐴, 𝐵} ⊆ 𝐶 → 2 ≤ (♯‘𝐶)))
Theorem	hashin 14346	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 14347	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 14348	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 14349	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 14350	The size of the difference of a finite set and a proper pair of its elements is the set's size minus 2. (Contributed by AV, 16-Dec-2020.)
⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶)) → (♯‘(𝐴 ∖ {𝐵, 𝐶})) = ((♯‘𝐴) − 2))
Theorem	hashsn01 14351	The size of a singleton is either 0 or 1. (Contributed by AV, 23-Feb-2021.)
⊢ ((♯‘{𝐴}) = 0 ∨ (♯‘{𝐴}) = 1)
Theorem	hashsnle1 14352	The size of a singleton is less than or equal to 1. (Contributed by AV, 23-Feb-2021.)
⊢ (♯‘{𝐴}) ≤ 1
Theorem	hashsnlei 14353	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 14354*	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 14355*	The size of a set is 1 in terms of existential uniqueness. (Contributed by Alexander van der Vekens, 8-Feb-2018.)
⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 1 ↔ ∃!𝑎 𝑎 ∈ 𝑉))
Theorem	hash1n0 14356	If the size of a set is 1 the set is not empty. (Contributed by AV, 23-Dec-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ (♯‘𝐴) = 1) → 𝐴 ≠ ∅)
Theorem	hashgt12el 14357*	In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.)
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑎 ≠ 𝑏)
Theorem	hashgt12el2 14358*	In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.)
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉) ∧ 𝐴 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)
Theorem	hashgt23el 14359*	A set with more than two elements has at least three different elements. (Contributed by BTernaryTau, 21-Sep-2023.)
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
Theorem	hashunlei 14360	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 14361	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 14362	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 14363	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 14364	Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (♯‘(𝐴..^𝐵)) = (𝐵 − 𝐴))
Theorem	hashfzo0 14365	Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ (𝐵 ∈ ℕ0 → (♯‘(0..^𝐵)) = 𝐵)
Theorem	hashfzp1 14366	Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021.)
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (♯‘((𝐴 + 1)...𝐵)) = (𝐵 − 𝐴))
Theorem	hashfz0 14367	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 14368	Lemma for hashxp 14369. (Contributed by Paul Chapman, 30-Nov-2012.)
⊢ 𝐵 ∈ Fin    ⇒   ⊢ (𝐴 ∈ Fin → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵)))
Theorem	hashxp 14369	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 14370	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.) (Proof shortened by AV, 18-Jul-2022.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 ↑m 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵)))
Theorem	hashpw 14371	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 14372	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	hashres 14373	The number of elements of a finite function restricted to a subset of its domain is equal to the number of elements of that subset. (Contributed by AV, 15-Dec-2021.)
⊢ ((Fun 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴) → (♯‘(𝐴 ↾ 𝐵)) = (♯‘𝐵))
Theorem	hashreshashfun 14374	The number of elements of a finite function expressed by a restriction. (Contributed by AV, 15-Dec-2021.)
⊢ ((Fun 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴) → (♯‘𝐴) = ((♯‘(𝐴 ↾ 𝐵)) + (♯‘(dom 𝐴 ∖ 𝐵))))
Theorem	hashimarn 14375	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 14376	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	hashfundm 14377	The size of a set function is equal to the size of its domain. (Contributed by BTernaryTau, 30-Sep-2023.)
⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (♯‘𝐹) = (♯‘dom 𝐹))
Theorem	hashf1dmrn 14378	The size of the domain of a one-to-one set function is equal to the size of its range. (Contributed by BTernaryTau, 1-Oct-2023.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (♯‘𝐴) = (♯‘ran 𝐹))
Theorem	hashf1dmcdm 14379	The size of the domain of a one-to-one set function is less than or equal to the size of its codomain, if it exists. (Contributed by BTernaryTau, 1-Oct-2023.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → (♯‘𝐴) ≤ (♯‘𝐵))
Theorem	resunimafz0 14380	TODO-AV: Revise using 𝐹 ∈ Word dom 𝐼? Formerly part of proof of eupth2lem3 30323: The union of a restriction by an image over an open range of nonnegative integers and a singleton of an ordered pair is a restriction by an image over an interval of nonnegative integers. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 20-Feb-2021.)
⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    ⇒   ⊢ (𝜑 → (𝐼 ↾ (𝐹 “ (0...𝑁))) = ((𝐼 ↾ (𝐹 “ (0..^𝑁))) ∪ {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩}))
Theorem	fnfz0hash 14381	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 14382	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 14383	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 14384	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 14385	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 14386	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 14387*	Lemma for hashbc 14388: inductive step. (Contributed by Mario Carneiro, 13-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑗 ∈ ℤ ((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}))    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}))
Theorem	hashbc 14388*	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 14389*	The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.) (Proof shortened by AV, 7-Aug-2024.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})
Theorem	hashf1lem1 14390*	Lemma for hashf1 14392. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 14-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → ((♯‘𝐴) + 1) ≤ (♯‘𝐵))    &   ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵)    ⇒   ⊢ (𝜑 → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ≈ (𝐵 ∖ ran 𝐹))
Theorem	hashf1lem2 14391*	Lemma for hashf1 14392. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → ((♯‘𝐴) + 1) ≤ (♯‘𝐵))    ⇒   ⊢ (𝜑 → (♯‘{𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵})))
Theorem	hashf1 14392*	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 14393*	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 14394	Two ways to write a strictly increasing function on the reals. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) → (𝐹 Isom < , < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ≤ (𝐴, 𝐵)))
Theorem	leisorel 14395	Version of isorel 7282 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.)
⊢ ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ≤ 𝐷 ↔ (𝐹‘𝐶) ≤ (𝐹‘𝐷)))
Theorem	fz1isolem 14396*	Lemma for fz1iso 14397. (Contributed by Mario Carneiro, 2-Apr-2014.)
⊢ 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)    &   ⊢ 𝐵 = (ℕ ∩ (◡ < “ {((♯‘𝐴) + 1)}))    &   ⊢ 𝐶 = (ω ∩ (◡𝐺‘((♯‘𝐴) + 1)))    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴))
Theorem	fz1iso 14397*	Any finite ordered set has an order isomorphism to a one-based finite sequence. (Contributed by Mario Carneiro, 2-Apr-2014.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴))
Theorem	ishashinf 14398*	Any set that is not finite contains subsets of arbitrarily large finite cardinality. Cf. isinf 9177. (Contributed by Thierry Arnoux, 5-Jul-2017.)
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ℕ ∃𝑥 ∈ 𝒫 𝐴(♯‘𝑥) = 𝑛)
Theorem	seqcoll 14399*	The function 𝐹 contains a sparse set of nonzero values to be summed. The function 𝐺 is an order isomorphism from the set of nonzero values of 𝐹 to a 1-based finite sequence, and 𝐻 collects these nonzero values together. Under these conditions, the sum over the values in 𝐻 yields the same result as the sum over the original set 𝐹. (Contributed by Mario Carneiro, 2-Apr-2014.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑍 + 𝑘) = 𝑘)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → (𝐹‘𝑘) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))
Theorem	seqcoll2 14400*	The function 𝐹 contains a sparse set of nonzero values to be summed. The function 𝐺 is an order isomorphism from the set of nonzero values of 𝐹 to a 1-based finite sequence, and 𝐻 collects these nonzero values together. Under these conditions, the sum over the values in 𝐻 yields the same result as the sum over the original set 𝐹. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑍 + 𝑘) = 𝑘)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...𝑁) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq1( + , 𝐻)‘(♯‘𝐴)))