![]() |
Metamath
Proof Explorer Theorem List (p. 136 of 437) | < 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: | ![]() (1-28347) |
![]() (28348-29872) |
![]() (29873-43639) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | prhash2ex 13501 | There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 13510, 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 13502 | 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 13503* | 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 13504* | 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 13505 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ ω & ⊢ 𝐵 = suc 𝐴 & ⊢ (♯‘𝐴) = 𝑀 & ⊢ (𝑀 + 1) = 𝑁 ⇒ ⊢ (♯‘𝐵) = 𝑁 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash1 13506 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (♯‘1o) = 1 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2 13507 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (♯‘2o) = 2 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash3 13508 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (♯‘3o) = 3 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash4 13509 | Size of a finite ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (♯‘4o) = 4 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pr0hash2ex 13510 | 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 13511 | 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 13512 | The size of a superset of a proper unordered pair is greater than 1. (Contributed by AV, 6-Feb-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ∈ 𝑈) → ({𝐴, 𝐵} ⊆ 𝐶 → 2 ≤ (♯‘𝐶))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashin 13513 | 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 13514 | 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 13515 | 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 13516 | 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 13517 | 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 13518 | The size of a singleton is either 0 or 1. (Contributed by AV, 23-Feb-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((♯‘{𝐴}) = 0 ∨ (♯‘{𝐴}) = 1) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashsnle1 13519 | The size of a singleton is less than or equal to 1. (Contributed by AV, 23-Feb-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (♯‘{𝐴}) ≤ 1 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashsnlei 13520 | 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 13521* | 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 13522* | The size of a set is 1 in terms of existential uniqueness. (Contributed by Alexander van der Vekens, 8-Feb-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 1 ↔ ∃!𝑎 𝑎 ∈ 𝑉)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash1n0 13523 | If the size of a set is 1 the set is not empty. (Contributed by AV, 23-Dec-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ 𝑉 ∧ (♯‘𝐴) = 1) → 𝐴 ≠ ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashgt12el 13524* | In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑎 ≠ 𝑏) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashgt12el2 13525* | In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉) ∧ 𝐴 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashunlei 13526 | 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 13527 | 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 13528 | 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 13529 | 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 13530 | Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (♯‘(𝐴..^𝐵)) = (𝐵 − 𝐴)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfzo0 13531 | Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐵 ∈ ℕ0 → (♯‘(0..^𝐵)) = 𝐵) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfzp1 13532 | Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐵 ∈ (ℤ≥‘𝐴) → (♯‘((𝐴 + 1)...𝐵)) = (𝐵 − 𝐴)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfz0 13533 | 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 13534 | Lemma for hashxp 13535. (Contributed by Paul Chapman, 30-Nov-2012.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐵 ∈ Fin ⇒ ⊢ (𝐴 ∈ Fin → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashxp 13535 | 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 13536 | 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) → (♯‘(𝐴 ↑𝑚 𝐵)) = ((♯‘𝐴)↑(♯‘𝐵))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashpw 13537 | 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 13538 | 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 13539 | 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 13540 | The number of elements of a finite function expressed by a restriction. (Contributed by AV, 15-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((Fun 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴) → (♯‘𝐴) = ((♯‘(𝐴 ↾ 𝐵)) + (♯‘(dom 𝐴 ∖ 𝐵)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashimarn 13541 | 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 13542 | 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 | resunimafz0 13543 | TODO-AV: Revise using 𝐹 ∈ Word dom 𝐼? Formerly part of proof of eupth2lem3 27640: 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 13544 | 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 13545 | 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 13546 | 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 13547 | 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 13548 | 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 13549 | 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 13550* | Lemma for hashbc 13551: inductive step. (Contributed by Mario Carneiro, 13-Jul-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) & ⊢ (𝜑 → ∀𝑗 ∈ ℤ ((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗})) & ⊢ (𝜑 → 𝐾 ∈ ℤ) ⇒ ⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashbc 13551* | 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 13552* | 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 13553* | Lemma for hashf1 13555. (Contributed by Mario Carneiro, 17-Apr-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) & ⊢ (𝜑 → ((♯‘𝐴) + 1) ≤ (♯‘𝐵)) & ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵) ⇒ ⊢ (𝜑 → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ≈ (𝐵 ∖ ran 𝐹)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashf1lem2 13554* | Lemma for hashf1 13555. (Contributed by Mario Carneiro, 17-Apr-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) & ⊢ (𝜑 → ((♯‘𝐴) + 1) ≤ (♯‘𝐵)) ⇒ ⊢ (𝜑 → (♯‘{𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵}) = (((♯‘𝐵) − (♯‘𝐴)) · (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashf1 13555* | 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 13556* | 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 13557 | Two ways to write a strictly increasing function on the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) → (𝐹 Isom < , < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ≤ (𝐴, 𝐵))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | leisorel 13558 | Version of isorel 6848 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ≤ 𝐷 ↔ (𝐹‘𝐶) ≤ (𝐹‘𝐷))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fz1isolem 13559* | Lemma for fz1iso 13560. (Contributed by Mario Carneiro, 2-Apr-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω) & ⊢ 𝐵 = (ℕ ∩ (◡ < “ {((♯‘𝐴) + 1)})) & ⊢ 𝐶 = (ω ∩ (◡𝐺‘((♯‘𝐴) + 1))) & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) ⇒ ⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fz1iso 13560* | 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 13561* | Any set that is not finite contains subsets of arbitrarily large finite cardinality. Cf. isinf 8461. (Contributed by Thierry Arnoux, 5-Jul-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ℕ ∃𝑥 ∈ 𝒫 𝐴(♯‘𝑥) = 𝑛) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | seqcoll 13562* | 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 13563* | 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 | hashprlei 13564 | An unordered pair has at most two elements. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ({𝐴, 𝐵} ∈ Fin ∧ (♯‘{𝐴, 𝐵}) ≤ 2) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2pr 13565* | A set of size two is an unordered pair. (Contributed by Alexander van der Vekens, 8-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 2) → ∃𝑎∃𝑏 𝑉 = {𝑎, 𝑏}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2prde 13566* | 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 13567* | 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 13568* | A set of size two is a proper unordered pair. (Contributed by AV, 1-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 ∈ 𝑊 → ((♯‘𝑉) = 2 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | prprrab 13569 | 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 13570 | The cardinality of a set with two distinct elements. (Contributed by Thierry Arnoux, 27-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝑃 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 2 ≤ (♯‘𝑃)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2prd 13571 | 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 13572 | 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 13573* | 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 13574* | 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 13575* | 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 13576* | A set with size at least 2 has at least 2 different elements. (Contributed by AV, 18-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐷 ∈ 𝑉 ∧ 2 ≤ (♯‘𝐷)) → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge2el2difr 13577* | A set with at least 2 different elements has size at least 2. (Contributed by AV, 14-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐷 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦) → 2 ≤ (♯‘𝐷)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge2el2difb 13578* | A set has size at least 2 iff it has at least 2 different elements. (Contributed by AV, 14-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐷 ∈ 𝑉 → (2 ≤ (♯‘𝐷) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 𝑥 ≠ 𝑦)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashdmpropge2 13579 | 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 13580 | An unordered triple has at most three elements. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ({𝐴, 𝐵, 𝐶} ∈ Fin ∧ (♯‘{𝐴, 𝐵, 𝐶}) ≤ 3) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashtpg 13581 | 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 | hashge3el3dif 13582* | A set with size at least 3 has at least 3 different elements. In contrast to hashge2el2dif 13576, 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 13583* | An element of the set of subsets with two elements is a proper unordered pair. (Contributed by AV, 1-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑃 ∈ {𝑧 ∈ 𝒫 𝑉 ∣ (♯‘𝑧) = 2} ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝑥 ≠ 𝑦 ∧ 𝑃 = {𝑥, 𝑦})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2sspr 13584* | 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 13585* | 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 13586* | A set of size three is an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 3) → ∃𝑎∃𝑏∃𝑐 𝑉 = {𝑎, 𝑏, 𝑐}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash1to3 13587* | 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 | fundmge2nop0 13588 | A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fundmge2nop 13589 (with the less restrictive requirement that (𝐺 ∖ {∅}) needs to be a function instead of 𝐺) is useful for proofs for extensible structures, see structn0fun 16267. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 7-Jun-2021.) (Proof shortened by AV, 15-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((Fun (𝐺 ∖ {∅}) ∧ 2 ≤ (♯‘dom 𝐺)) → ¬ 𝐺 ∈ (V × V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fundmge2nop 13589 | A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 12-Oct-2020.) (Proof shortened by AV, 9-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((Fun 𝐺 ∧ 2 ≤ (♯‘dom 𝐺)) → ¬ 𝐺 ∈ (V × V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fun2dmnop0 13590 | A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fun2dmnop 13591 (with the less restrictive requirement that (𝐺 ∖ {∅}) needs to be a function instead of 𝐺) is useful for proofs for extensible structures, see structn0fun 16267. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((Fun (𝐺 ∖ {∅}) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → ¬ 𝐺 ∈ (V × V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fun2dmnop 13591 | A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 9-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((Fun 𝐺 ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → ¬ 𝐺 ∈ (V × V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashdifsnp1 13592 | If the size of a set is a nonnegative integer increased by 1, the size of the set with one of its elements removed is this nonnegative integer. (Contributed by Alexander van der Vekens, 7-Jan-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0) → ((♯‘𝑉) = (𝑌 + 1) → (♯‘(𝑉 ∖ {𝑁})) = 𝑌)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fi1uzind 13593* | Properties of an ordered pair with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (represented as orderd pairs of vertices and edges) with a finite number of vertices, usually with 𝐿 = 0 (see opfi1ind 13598) or 𝐿 = 1. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐹 ∈ V & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ 𝑛 ∈ 𝑣) → [(𝑣 ∖ {𝑛}) / 𝑎][𝐹 / 𝑏]𝜌) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ (([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (♯‘𝑣) = 𝐿) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ ([𝑣 / 𝑎][𝑒 / 𝑏]𝜌 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ (([𝑉 / 𝑎][𝐸 / 𝑏]𝜌 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (♯‘𝑉)) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1uzind 13594* | Properties of a binary relation with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (as binary relation between the set of vertices and an edge function) with a finite number of vertices, usually with 𝐿 = 0 (see brfi1ind 13595) or 𝐿 = 1. (Contributed by Alexander van der Vekens, 7-Jan-2018.) (Proof shortened by AV, 23-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Rel 𝐺 & ⊢ 𝐹 ∈ V & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 𝐿) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (♯‘𝑉)) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1ind 13595* | Properties of a binary relation with a finite first component, proven by finite induction on the size of the first component. (Contributed by Alexander van der Vekens, 7-Jan-2018.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Rel 𝐺 & ⊢ 𝐹 ∈ V & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1indALT 13596* | Alternate proof of brfi1ind 13595, which does not use brfi1uzind 13594. (Contributed by Alexander van der Vekens, 7-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Rel 𝐺 & ⊢ 𝐹 ∈ V & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((𝑣𝐺𝑒 ∧ 𝑛 ∈ 𝑣) → (𝑣 ∖ {𝑛})𝐺𝐹) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((𝑣𝐺𝑒 ∧ (♯‘𝑣) = 0) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (𝑣𝐺𝑒 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((𝑉𝐺𝐸 ∧ 𝑉 ∈ Fin) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opfi1uzind 13597* | Properties of an ordered pair with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (represented as orderd pairs of vertices and edges) with a finite number of vertices, usually with 𝐿 = 0 (see opfi1ind 13598) or 𝐿 = 1. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ 𝑛 ∈ 𝑣) → 〈(𝑣 ∖ {𝑛}), 𝐹〉 ∈ 𝐺) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (♯‘𝑣) = 𝐿) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((〈𝑉, 𝐸〉 ∈ 𝐺 ∧ 𝑉 ∈ Fin ∧ 𝐿 ≤ (♯‘𝑉)) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opfi1ind 13598* | Properties of an ordered pair with a finite first component, proven by finite induction on the size of the first component. This theorem can be applied for graphs (represented as orderd pairs of vertices and edges) with a finite number of vertices, e.g. fusgrfis 26677. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V & ⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜓 ↔ 𝜑)) & ⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝜓 ↔ 𝜃)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ 𝑛 ∈ 𝑣) → 〈(𝑣 ∖ {𝑛}), 𝐹〉 ∈ 𝐺) & ⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = 𝐹) → (𝜃 ↔ 𝜒)) & ⊢ ((〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (♯‘𝑣) = 0) → 𝜓) & ⊢ ((((𝑦 + 1) ∈ ℕ0 ∧ (〈𝑣, 𝑒〉 ∈ 𝐺 ∧ (♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ 𝜒) → 𝜓) ⇒ ⊢ ((〈𝑉, 𝐸〉 ∈ 𝐺 ∧ 𝑉 ∈ Fin) → 𝜑) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
This section is about words (or strings) over a set (alphabet) defined as finite sequences of symbols (or characters) being elements of the alphabet. Although it is often required that the underlying set/alphabet be nonempty, finite and not a proper class, these restrictions are not made in the current definition df-word 13600, see, for example, s1cli 13695: 〈“𝐴”〉 ∈ Word V. Note that the empty word ∅ (i.e. the empty set) is the only word over an empty alphabet, see 0wrd0 13628. The set Word 𝑆 of words over 𝑆 is the free monoid over 𝑆, where the monoid law is concatenation and the monoid unit is the empty word. Besides the definition of words themselves, several operations on words are defined in this section:
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cword 13599 | Syntax for the Word operator. | ||||||||||||||||||||||||||||||||||||||||||||||||||
class Word 𝑆 | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-word 13600* | Define the class of words over a set. A word (sometimes also called a string) is a finite sequence of symbols from a set (alphabet) 𝑆. Definition in Section 9.1 of [AhoHopUll] p. 318. The domain is forced to be an initial segment of ℕ0 so that two words with the same symbols in the same order be equal. The set Word 𝑆 is sometimes denoted by S*, using the Kleene star, although the Kleene star, or Kleene closure, is sometimes reserved to denote an operation on languages. The set Word 𝑆 is the free monoid over 𝑆, where the monoid law is concatenation and the monoid unit is the empty word (see frmdval 17775). (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |