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	hashprb 14301	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 14302	The elements of an unordered pair of size 2 are different sets. (Contributed by AV, 27-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    ⇒   ⊢ ((♯‘𝑆) = 2 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵))
Theorem	prhash2ex 14303	There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 14312, 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 14304	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 14305*	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 14306*	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 14307	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 = suc 𝐴    &   ⊢ (♯‘𝐴) = 𝑀    &   ⊢ (𝑀 + 1) = 𝑁    ⇒   ⊢ (♯‘𝐵) = 𝑁
Theorem	hash1 14308	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (♯‘1o) = 1
Theorem	hash2 14309	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (♯‘2o) = 2
Theorem	hash3 14310	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (♯‘3o) = 3
Theorem	hash4 14311	Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (♯‘4o) = 4
Theorem	pr0hash2ex 14312	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 14313	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 14314	The size of a superset of a proper unordered pair is greater than 1. (Contributed by AV, 6-Feb-2021.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ∈ 𝑈) → ({𝐴, 𝐵} ⊆ 𝐶 → 2 ≤ (♯‘𝐶)))
Theorem	hashin 14315	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 14316	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 14317	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 14318	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 14319	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 14320	The size of a singleton is either 0 or 1. (Contributed by AV, 23-Feb-2021.)
⊢ ((♯‘{𝐴}) = 0 ∨ (♯‘{𝐴}) = 1)
Theorem	hashsnle1 14321	The size of a singleton is less than or equal to 1. (Contributed by AV, 23-Feb-2021.)
⊢ (♯‘{𝐴}) ≤ 1
Theorem	hashsnlei 14322	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 14323*	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 14324*	The size of a set is 1 in terms of existential uniqueness. (Contributed by Alexander van der Vekens, 8-Feb-2018.)
⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 1 ↔ ∃!𝑎 𝑎 ∈ 𝑉))
Theorem	hash1n0 14325	If the size of a set is 1 the set is not empty. (Contributed by AV, 23-Dec-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ (♯‘𝐴) = 1) → 𝐴 ≠ ∅)
Theorem	hashgt12el 14326*	In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.)
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑎 ≠ 𝑏)
Theorem	hashgt12el2 14327*	In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.)
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉) ∧ 𝐴 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)
Theorem	hashgt23el 14328*	A set with more than two elements has at least three different elements. (Contributed by BTernaryTau, 21-Sep-2023.)
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
Theorem	hashunlei 14329	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 14330	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 14331	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 14332	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 14333	Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (♯‘(𝐴..^𝐵)) = (𝐵 − 𝐴))
Theorem	hashfzo0 14334	Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ (𝐵 ∈ ℕ0 → (♯‘(0..^𝐵)) = 𝐵)
Theorem	hashfzp1 14335	Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021.)
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (♯‘((𝐴 + 1)...𝐵)) = (𝐵 − 𝐴))
Theorem	hashfz0 14336	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 14337	Lemma for hashxp 14338. (Contributed by Paul Chapman, 30-Nov-2012.)
⊢ 𝐵 ∈ Fin    ⇒   ⊢ (𝐴 ∈ Fin → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵)))
Theorem	hashxp 14338	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 14339	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 14340	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 14341	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 14342	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 14343	The number of elements of a finite function expressed by a restriction. (Contributed by AV, 15-Dec-2021.)
⊢ ((Fun 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴) → (♯‘𝐴) = ((♯‘(𝐴 ↾ 𝐵)) + (♯‘(dom 𝐴 ∖ 𝐵))))
Theorem	hashimarn 14344	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 14345	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 14346	The size of a set function is equal to the size of its domain. (Contributed by BTernaryTau, 30-Sep-2023.)
⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (♯‘𝐹) = (♯‘dom 𝐹))
Theorem	hashf1dmrn 14347	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 14348	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 14349	TODO-AV: Revise using 𝐹 ∈ Word dom 𝐼? Formerly part of proof of eupth2lem3 30211: 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 14350	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 14351	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 14352	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 14353	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 14354	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 14355	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 14356*	Lemma for hashbc 14357: inductive step. (Contributed by Mario Carneiro, 13-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑗 ∈ ℤ ((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}))    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}))
Theorem	hashbc 14357*	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 14358*	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 14359*	Lemma for hashf1 14361. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 14-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → ((♯‘𝐴) + 1) ≤ (♯‘𝐵))    &   ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵)    ⇒   ⊢ (𝜑 → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ≈ (𝐵 ∖ ran 𝐹))
Theorem	hashf1lem2 14360*	Lemma for hashf1 14361. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)    &   ⊢ (𝜑 → ((♯‘𝐴) + 1) ≤ (♯‘𝐵))    ⇒   ⊢ (𝜑 → (♯‘{𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵})))
Theorem	hashf1 14361*	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 14362*	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 14363	Two ways to write a strictly increasing function on the reals. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) → (𝐹 Isom < , < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ≤ (𝐴, 𝐵)))
Theorem	leisorel 14364	Version of isorel 7260 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.)
⊢ ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ≤ 𝐷 ↔ (𝐹‘𝐶) ≤ (𝐹‘𝐷)))
Theorem	fz1isolem 14365*	Lemma for fz1iso 14366. (Contributed by Mario Carneiro, 2-Apr-2014.)
⊢ 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)    &   ⊢ 𝐵 = (ℕ ∩ (◡ < “ {((♯‘𝐴) + 1)}))    &   ⊢ 𝐶 = (ω ∩ (◡𝐺‘((♯‘𝐴) + 1)))    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴))
Theorem	fz1iso 14366*	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 14367*	Any set that is not finite contains subsets of arbitrarily large finite cardinality. Cf. isinf 9149. (Contributed by Thierry Arnoux, 5-Jul-2017.)
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ℕ ∃𝑥 ∈ 𝒫 𝐴(♯‘𝑥) = 𝑛)
Theorem	seqcoll 14368*	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 14369*	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( + , 𝐻)‘(♯‘𝐴)))
Theorem	phphashd 14370	Corollary of the Pigeonhole Principle using equality. Equivalent of phpeqd 9121 expressed using the hash function. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → (♯‘𝐴) = (♯‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	phphashrd 14371	Corollary of the Pigeonhole Principle using equality. Equivalent of phphashd 14370 with reversed arguments. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → (♯‘𝐴) = (♯‘𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
5.6.11.1  Proper unordered pairs and triples (sets of size 2 and 3)
Theorem	hashprlei 14372	An unordered pair has at most two elements. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ ({𝐴, 𝐵} ∈ Fin ∧ (♯‘{𝐴, 𝐵}) ≤ 2)
Theorem	hash2pr 14373*	A set of size two is an unordered pair. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 2) → ∃𝑎∃𝑏 𝑉 = {𝑎, 𝑏})
Theorem	hash2prde 14374*	A set of size two is an unordered pair of two different elements. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 2) → ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}))
Theorem	hash2exprb 14375*	A set of size two is an unordered pair if and only if it contains two different elements. (Contributed by Alexander van der Vekens, 14-Jan-2018.)
⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 2 ↔ ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏})))
Theorem	hash2prb 14376*	A set of size two is a proper unordered pair. (Contributed by AV, 1-Nov-2020.)
⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 2 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏})))
Theorem	prprrab 14377	The set of proper pairs of elements of a given set expressed in two ways. (Contributed by AV, 24-Nov-2020.)
⊢ {𝑥 ∈ (𝒫 𝐴 ∖ {∅}) ∣ (♯‘𝑥) = 2} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 2}
Theorem	nehash2 14378	The cardinality of a set with two distinct elements. (Contributed by Thierry Arnoux, 27-Aug-2019.)
⊢ (𝜑 → 𝑃 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 2 ≤ (♯‘𝑃))
Theorem	hash2prd 14379	A set of size two is an unordered pair if it contains two different elements. (Contributed by Alexander van der Vekens, 9-Dec-2018.) (Proof shortened by AV, 16-Jun-2022.)
⊢ ((𝑃 ∈ 𝑉 ∧ (♯‘𝑃) = 2) → ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝑃 = {𝑋, 𝑌}))
Theorem	hash2pwpr 14380	If the size of a subset of an unordered pair is 2, the subset is the pair itself. (Contributed by Alexander van der Vekens, 9-Dec-2018.)
⊢ (((♯‘𝑃) = 2 ∧ 𝑃 ∈ 𝒫 {𝑋, 𝑌}) → 𝑃 = {𝑋, 𝑌})
Theorem	hashle2pr 14381*	A nonempty set of size less than or equal to two is an unordered pair of sets. (Contributed by AV, 24-Nov-2021.)
⊢ ((𝑃 ∈ 𝑉 ∧ 𝑃 ≠ ∅) → ((♯‘𝑃) ≤ 2 ↔ ∃𝑎∃𝑏 𝑃 = {𝑎, 𝑏}))
Theorem	hashle2prv 14382*	A nonempty subset of a powerset of a class 𝑉 has size less than or equal to two iff it is an unordered pair of elements of 𝑉. (Contributed by AV, 24-Nov-2021.)
⊢ (𝑃 ∈ (𝒫 𝑉 ∖ {∅}) → ((♯‘𝑃) ≤ 2 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑃 = {𝑎, 𝑏}))
Theorem	pr2pwpr 14383*	The set of subsets of a pair having length 2 is the set of the pair as singleton. (Contributed by AV, 9-Dec-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → {𝑝 ∈ 𝒫 {𝐴, 𝐵} ∣ 𝑝 ≈ 2o} = {{𝐴, 𝐵}})
Theorem	hashge2el2dif 14384*	A set with size at least 2 has at least 2 different elements. (Contributed by AV, 18-Mar-2019.)
⊢ ((𝐷 ∈ 𝑉 ∧ 2 ≤ (♯‘𝐷)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦)
Theorem	hashge2el2difr 14385*	A set with at least 2 different elements has size at least 2. (Contributed by AV, 14-Oct-2020.)
⊢ ((𝐷 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦) → 2 ≤ (♯‘𝐷))
Theorem	hashge2el2difb 14386*	A set has size at least 2 iff it has at least 2 different elements. (Contributed by AV, 14-Oct-2020.)
⊢ (𝐷 ∈ 𝑉 → (2 ≤ (♯‘𝐷) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦))
Theorem	hashdmpropge2 14387	The size of the domain of a class which contains two ordered pairs with different first components is greater than or equal to 2. (Contributed by AV, 12-Nov-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} ⊆ 𝐹)    ⇒   ⊢ (𝜑 → 2 ≤ (♯‘dom 𝐹))
Theorem	hashtplei 14388	An unordered triple has at most three elements. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ ({𝐴, 𝐵, 𝐶} ∈ Fin ∧ (♯‘{𝐴, 𝐵, 𝐶}) ≤ 3)
Theorem	hashtpg 14389	The size of an unordered triple of three different elements. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 18-Sep-2021.)
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) ↔ (♯‘{𝐴, 𝐵, 𝐶}) = 3))
Theorem	hash7g 14390	The size of an unordered set of seven different elements. (Contributed by AV, 2-Aug-2025.)
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐷 ∈ 𝑉 ∧ (𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉)) ∧ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺)) ∧ ((𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ (𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺)) ∧ (𝐶 ≠ 𝐷 ∧ (𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺))) ∧ ((𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺) ∧ (𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺)))) → (♯‘(({𝐴, 𝐵, 𝐶} ∪ {𝐷}) ∪ {𝐸, 𝐹, 𝐺})) = 7)
Theorem	hashge3el3dif 14391*	A set with size at least 3 has at least 3 different elements. In contrast to hashge2el2dif 14384, which has an elementary proof, the dominance relation and 1-1 functions from a set with three elements which are known to be different are used to prove this theorem. Although there is also an elementary proof for this theorem, it might be much longer. After all, this proof should be kept because it can be used as template for proofs for higher cardinalities. (Contributed by AV, 20-Mar-2019.) (Proof modification is discouraged.)
⊢ ((𝐷 ∈ 𝑉 ∧ 3 ≤ (♯‘𝐷)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 ∃𝑧 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧))
Theorem	elss2prb 14392*	An element of the set of subsets with two elements is a proper unordered pair. (Contributed by AV, 1-Nov-2020.)
⊢ (𝑃 ∈ {𝑧 ∈ 𝒫 𝑉 ∣ (♯‘𝑧) = 2} ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦}))
Theorem	hash2sspr 14393*	A subset of size two is an unordered pair of elements of its superset. (Contributed by Alexander van der Vekens, 12-Jul-2017.) (Proof shortened by AV, 4-Nov-2020.)
⊢ ((𝑃 ∈ 𝒫 𝑉 ∧ (♯‘𝑃) = 2) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑃 = {𝑎, 𝑏})
Theorem	exprelprel 14394*	If there is an element of the set of subsets with two elements in a set, an unordered pair of sets is in the set. (Contributed by Alexander van der Vekens, 12-Jul-2018.)
⊢ (∃𝑝 ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}𝑝 ∈ 𝑋 → ∃𝑣 ∈ 𝑉 ∃𝑤 ∈ 𝑉 {𝑣, 𝑤} ∈ 𝑋)
Theorem	hash3tr 14395*	A set of size three is an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018.)
⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 3) → ∃𝑎∃𝑏∃𝑐 𝑉 = {𝑎, 𝑏, 𝑐})
Theorem	hash1to3 14396*	If the size of a set is between 1 and 3 (inclusively), the set is a singleton or an unordered pair or an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018.)
⊢ ((𝑉 ∈ Fin ∧ 1 ≤ (♯‘𝑉) ∧ (♯‘𝑉) ≤ 3) → ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}))
Theorem	hash3tpde 14397*	A set of size three is an unordered triple of three different elements. (Contributed by AV, 21-Jul-2025.)
⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 3) → ∃𝑎∃𝑏∃𝑐((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ∧ 𝑉 = {𝑎, 𝑏, 𝑐}))
Theorem	hash3tpexb 14398*	A set of size three is an unordered triple if and only if it contains three different elements. (Contributed by AV, 21-Jul-2025.)
⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 3 ↔ ∃𝑎∃𝑏∃𝑐((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ∧ 𝑉 = {𝑎, 𝑏, 𝑐})))
Theorem	hash3tpb 14399*	A set of size three is a proper unordered triple. (Contributed by AV, 21-Jul-2025.)
⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 3 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ∧ 𝑉 = {𝑎, 𝑏, 𝑐})))
Theorem	tpf1ofv0 14400*	The value of a one-to-one function onto a triple at 0. (Contributed by AV, 20-Jul-2025.)
⊢ 𝐹 = (𝑥 ∈ (0..^3) ↦ if(𝑥 = 0, 𝐴, if(𝑥 = 1, 𝐵, 𝐶)))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐹‘0) = 𝐴)