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	hasheni 14301	Equinumerous sets have the same number of elements (even if they are not finite). (Contributed by Mario Carneiro, 15-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 → (♯‘𝐴) = (♯‘𝐵))
Theorem	hasheqf1o 14302*	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 14303*	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	hasheqf1oi 14304*	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	hashf1rn 14305	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	hasheqf1od 14306	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 14307	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 14308	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 14309	Closure of the ♯ function. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 13-Jul-2014.)
⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
Theorem	hashxrcl 14310	Extended real closure of the ♯ function. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (♯‘𝐴) ∈ ℝ*)
Theorem	hashclb 14311	Reverse closure of the ♯ function. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ (♯‘𝐴) ∈ ℕ0))
Theorem	nfile 14312	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 14313	A set of finite size is a finite set. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((♯‘𝑆) = 𝑁 → 𝑆 ∈ Fin))
Theorem	hashnfinnn0 14314	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 14315	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 14316	Two ways of saying a set is empty. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 27-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅))
Theorem	hashneq0 14317	Two ways of saying a set is not empty. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
⊢ (𝐴 ∈ 𝑉 → (0 < (♯‘𝐴) ↔ 𝐴 ≠ ∅))
Theorem	hashgt0n0 14318	If the size of a set is greater than 0, the set is not empty. (Contributed by AV, 5-Aug-2018.) (Proof shortened by AV, 18-Nov-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 0 < (♯‘𝐴)) → 𝐴 ≠ ∅)
Theorem	hashnncl 14319	Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
Theorem	hash0 14320	The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.)
⊢ (♯‘∅) = 0
Theorem	hashelne0d 14321	A set with an element has nonzero size. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ¬ (♯‘𝐴) = 0)
Theorem	hashsng 14322	The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 13-Feb-2013.)
⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1)
Theorem	hashen1 14323	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 14324	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 14325*	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 14326*	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 14327*	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 14328	A function is equinumerous to its domain. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ (𝐹 Fn 𝐴 → (♯‘𝐹) = (♯‘𝐴))
Theorem	fseq1hash 14329	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 14330	𝐺 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 14331	A short expression for the 𝐺 function of hashgf1o 13924. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ (♯ ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
Theorem	hashdom 14332	Dominance relation for the size function. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 22-Apr-2015.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))
Theorem	hashdomi 14333	Non-strict order relation of the ♯ function on the full cardinal poset. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ (𝐴 ≼ 𝐵 → (♯‘𝐴) ≤ (♯‘𝐵))
Theorem	hashsdom 14334	Strict dominance relation for the size function. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) < (♯‘𝐵) ↔ 𝐴 ≺ 𝐵))
Theorem	hashun 14335	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 14336	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 14337	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 14338	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 14339	The size of the union of disjoint sets is the result of the extended real addition of their sizes, analogous to hashun 14335. (Contributed by Alexander van der Vekens, 21-Dec-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (♯‘(𝐴 ∪ 𝐵)) = ((♯‘𝐴) +𝑒 (♯‘𝐵)))
Theorem	hashge0 14340	The cardinality of a set is greater than or equal to zero. (Contributed by Thierry Arnoux, 2-Mar-2017.)
⊢ (𝐴 ∈ 𝑉 → 0 ≤ (♯‘𝐴))
Theorem	hashgt0 14341	The cardinality of a nonempty set is greater than zero. (Contributed by Thierry Arnoux, 2-Mar-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → 0 < (♯‘𝐴))
Theorem	hashge1 14342	The cardinality of a nonempty set is greater than or equal to one. (Contributed by Thierry Arnoux, 20-Jun-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → 1 ≤ (♯‘𝐴))
Theorem	1elfz0hash 14343	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 14344	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 14345	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 14346	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 14345. (Contributed by BTernaryTau, 9-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (¬ 𝐵 ∈ 𝐴 → (♯‘(𝐴 ∪ {𝐵})) = ((♯‘𝐴) +𝑒 1)))
Theorem	hashunsnggt 14347	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 14348	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 14349	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 14350	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 14351	The elements of an unordered pair of size 2 are different sets. (Contributed by AV, 27-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    ⇒   ⊢ ((♯‘𝑆) = 2 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵))
Theorem	prhash2ex 14352	There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 14361, 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 14353	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 14354*	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 14355*	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 14356	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 = suc 𝐴    &   ⊢ (♯‘𝐴) = 𝑀    &   ⊢ (𝑀 + 1) = 𝑁    ⇒   ⊢ (♯‘𝐵) = 𝑁
Theorem	hash1 14357	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (♯‘1o) = 1
Theorem	hash2 14358	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (♯‘2o) = 2
Theorem	hash3 14359	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (♯‘3o) = 3
Theorem	hash4 14360	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (♯‘4o) = 4
Theorem	pr0hash2ex 14361	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 14362	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 14363	The size of a superset of a proper unordered pair is greater than 1. (Contributed by AV, 6-Feb-2021.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ∈ 𝑈) → ({𝐴, 𝐵} ⊆ 𝐶 → 2 ≤ (♯‘𝐶)))
Theorem	hashin 14364	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 14365	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 14366	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 14367	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 14368	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 14369	The size of a singleton is either 0 or 1. (Contributed by AV, 23-Feb-2021.)
⊢ ((♯‘{𝐴}) = 0 ∨ (♯‘{𝐴}) = 1)
Theorem	hashsnle1 14370	The size of a singleton is less than or equal to 1. (Contributed by AV, 23-Feb-2021.)
⊢ (♯‘{𝐴}) ≤ 1
Theorem	hashsnlei 14371	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 14372*	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 14373*	The size of a set is 1 in terms of existential uniqueness. (Contributed by Alexander van der Vekens, 8-Feb-2018.)
⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 1 ↔ ∃!𝑎 𝑎 ∈ 𝑉))
Theorem	hash1n0 14374	If the size of a set is 1 the set is not empty. (Contributed by AV, 23-Dec-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ (♯‘𝐴) = 1) → 𝐴 ≠ ∅)
Theorem	hashgt12el 14375*	In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.)
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑎 ≠ 𝑏)
Theorem	hashgt12el2 14376*	In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.)
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉) ∧ 𝐴 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)
Theorem	hashgt23el 14377*	A set with more than two elements has at least three different elements. (Contributed by BTernaryTau, 21-Sep-2023.)
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
Theorem	hashunlei 14378	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 14379	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 14380	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 14381	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 14382	Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (♯‘(𝐴..^𝐵)) = (𝐵 − 𝐴))
Theorem	hashfzo0 14383	Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ (𝐵 ∈ ℕ0 → (♯‘(0..^𝐵)) = 𝐵)
Theorem	hashfzp1 14384	Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021.)
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (♯‘((𝐴 + 1)...𝐵)) = (𝐵 − 𝐴))
Theorem	hashfz0 14385	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 14386	Lemma for hashxp 14387. (Contributed by Paul Chapman, 30-Nov-2012.)
⊢ 𝐵 ∈ Fin    ⇒   ⊢ (𝐴 ∈ Fin → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵)))
Theorem	hashxp 14387	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 14388	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 14389	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 14390	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 14391	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 14392	The number of elements of a finite function expressed by a restriction. (Contributed by AV, 15-Dec-2021.)
⊢ ((Fun 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴) → (♯‘𝐴) = ((♯‘(𝐴 ↾ 𝐵)) + (♯‘(dom 𝐴 ∖ 𝐵))))
Theorem	hashimarn 14393	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 14394	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 14395	The size of a set function is equal to the size of its domain. (Contributed by BTernaryTau, 30-Sep-2023.)
⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (♯‘𝐹) = (♯‘dom 𝐹))
Theorem	hashf1dmrn 14396	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 14397	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 14398	TODO-AV: Revise using 𝐹 ∈ Word dom 𝐼? Formerly part of proof of eupth2lem3 30321: 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 14399	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 14400	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))