| Metamath
Proof Explorer Theorem List (p. 474 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | f1oresf1orab 47301* | Build a bijection by restricting the domain of a bijection. (Contributed by AV, 1-Aug-2022.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) → (𝜒 ↔ 𝑥 ∈ 𝐷)) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) | ||
| Theorem | f1oresf1o 47302* | Build a bijection by restricting the domain of a bijection. (Contributed by AV, 31-Jul-2022.) |
| ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ (𝜑 → (∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦 ↔ (𝑦 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) | ||
| Theorem | f1oresf1o2 47303* | Build a bijection by restricting the domain of a bijection. (Contributed by AV, 31-Jul-2022.) |
| ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → (𝑥 ∈ 𝐷 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) | ||
| Theorem | fvmptrab 47304* | Value of a function mapping a set to a class abstraction restricting a class depending on the argument of the function. More general version of fvmptrabfv 7048, but relying on the fact that out-of-domain arguments evaluate to the empty set, which relies on set.mm's particular encoding. (Contributed by AV, 14-Feb-2022.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑀 ∣ 𝜑}) & ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑋 → 𝑀 = 𝑁) & ⊢ (𝑋 ∈ 𝑉 → 𝑁 ∈ V) & ⊢ (𝑋 ∉ 𝑉 → 𝑁 = ∅) ⇒ ⊢ (𝐹‘𝑋) = {𝑦 ∈ 𝑁 ∣ 𝜓} | ||
| Theorem | fvmptrabdm 47305* | Value of a function mapping a set to a class abstraction restricting the value of another function. See also fvmptrabfv 7048. (Suggested by BJ, 18-Feb-2022.) (Contributed by AV, 18-Feb-2022.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ (𝐺‘𝑌) ∣ 𝜑}) & ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜓)) & ⊢ (𝑌 ∈ dom 𝐺 → 𝑋 ∈ dom 𝐹) ⇒ ⊢ (𝐹‘𝑋) = {𝑦 ∈ (𝐺‘𝑌) ∣ 𝜓} | ||
| Theorem | cnambpcma 47306 | ((a-b)+c)-a = c-a holds for complex numbers a,b,c. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) + 𝐶) − 𝐴) = (𝐶 − 𝐵)) | ||
| Theorem | cnapbmcpd 47307 | ((a+b)-c)+d = ((a+d)+b)-c holds for complex numbers a,b,c,d. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 + 𝐵) − 𝐶) + 𝐷) = (((𝐴 + 𝐷) + 𝐵) − 𝐶)) | ||
| Theorem | addsubeq0 47308 | The sum of two complex numbers is equal to the difference of these two complex numbers iff the subtrahend is 0. (Contributed by AV, 8-May-2023.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 − 𝐵) ↔ 𝐵 = 0)) | ||
| Theorem | leaddsuble 47309 | Addition and subtraction on one side of "less than or equal to". (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ ((𝐴 + 𝐵) − 𝐶) ≤ 𝐴)) | ||
| Theorem | 2leaddle2 47310 | If two real numbers are less than a third real number, the sum of the real numbers is less than twice the third real number. (Contributed by Alexander van der Vekens, 21-May-2018.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐶) → (𝐴 + 𝐵) < (2 · 𝐶))) | ||
| Theorem | ltnltne 47311 | Variant of trichotomy law for 'less than'. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (¬ 𝐵 < 𝐴 ∧ ¬ 𝐵 = 𝐴))) | ||
| Theorem | p1lep2 47312 | A real number increasd by 1 is less than or equal to the number increased by 2. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
| ⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ≤ (𝑁 + 2)) | ||
| Theorem | ltsubsubaddltsub 47313 | If the result of subtracting two numbers is greater than a number, the result of adding one of these subtracted numbers to the number is less than the result of subtracting the other subtracted number only. (Contributed by Alexander van der Vekens, 9-Jun-2018.) |
| ⊢ ((𝐽 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ)) → (𝐽 < ((𝐿 − 𝑀) − 𝑁) ↔ (𝐽 + 𝑀) < (𝐿 − 𝑁))) | ||
| Theorem | zm1nn 47314 | An integer minus 1 is positive under certain circumstances. (Contributed by Alexander van der Vekens, 9-Jun-2018.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝐽 ∈ ℝ ∧ 0 ≤ 𝐽 ∧ 𝐽 < ((𝐿 − 𝑁) − 1)) → (𝐿 − 1) ∈ ℕ)) | ||
| Theorem | readdcnnred 47315 | The sum of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ)) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∉ ℝ) | ||
| Theorem | resubcnnred 47316 | The difference of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ∉ ℝ) | ||
| Theorem | recnmulnred 47317 | The product of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ)) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∉ ℝ) | ||
| Theorem | cndivrenred 47318 | The quotient of an imaginary number and a real number is not a real number. (Contributed by AV, 23-Jan-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ)) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (𝐵 / 𝐴) ∉ ℝ) | ||
| Theorem | sqrtnegnre 47319 | The square root of a negative number is not a real number. (Contributed by AV, 28-Feb-2023.) |
| ⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → (√‘𝑋) ∉ ℝ) | ||
| Theorem | nn0resubcl 47320 | Closure law for subtraction of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 − 𝐵) ∈ ℝ) | ||
| Theorem | zgeltp1eq 47321 | If an integer is between another integer and its successor, the integer is equal to the other integer. (Contributed by AV, 30-May-2020.) |
| ⊢ ((𝐼 ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 ≤ 𝐼 ∧ 𝐼 < (𝐴 + 1)) → 𝐼 = 𝐴)) | ||
| Theorem | 1t10e1p1e11 47322 | 11 is 1 times 10 to the power of 1, plus 1. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
| ⊢ ;11 = ((1 · (;10↑1)) + 1) | ||
| Theorem | deccarry 47323 | Add 1 to a 2 digit number with carry. This is a special case of decsucc 12774, but in closed form. As observed by ML, this theorem allows for carrying the 1 down multiple decimal constructors, so we can carry the 1 multiple times down a multi-digit number, e.g., by applying this theorem three times we get (;;999 + 1) = ;;;1000. (Contributed by AV, 4-Aug-2020.) (Revised by ML, 8-Aug-2020.) (Proof shortened by AV, 10-Sep-2021.) |
| ⊢ (𝐴 ∈ ℕ → (;𝐴9 + 1) = ;(𝐴 + 1)0) | ||
| Theorem | eluzge0nn0 47324 | If an integer is greater than or equal to a nonnegative integer, then it is a nonnegative integer. (Contributed by Alexander van der Vekens, 27-Aug-2018.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (0 ≤ 𝑀 → 𝑁 ∈ ℕ0)) | ||
| Theorem | nltle2tri 47325 | Negated extended trichotomy law for 'less than' and 'less than or equal to'. (Contributed by AV, 18-Jul-2020.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴)) | ||
| Theorem | ssfz12 47326 | Subset relationship for finite sets of sequential integers. (Contributed by Alexander van der Vekens, 16-Mar-2018.) |
| ⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿) → ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) | ||
| Theorem | elfz2z 47327 | Membership of an integer in a finite set of sequential integers starting at 0. (Contributed by Alexander van der Vekens, 25-May-2018.) |
| ⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ (0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) | ||
| Theorem | 2elfz3nn0 47328 | If there are two elements in a finite set of sequential integers starting at 0, these two elements as well as the upper bound are nonnegative integers. (Contributed by Alexander van der Vekens, 7-Apr-2018.) |
| ⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) | ||
| Theorem | fz0addcom 47329 | The addition of two members of a finite set of sequential integers starting at 0 is commutative. (Contributed by Alexander van der Vekens, 22-May-2018.) (Revised by Alexander van der Vekens, 9-Jun-2018.) |
| ⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
| Theorem | 2elfz2melfz 47330 | If the sum of two integers of a 0-based finite set of sequential integers is greater than the upper bound, the difference between one of the integers and the difference between the upper bound and the other integer is in the 0-based finite set of sequential integers with the first integer as upper bound. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.) |
| ⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝑁 < (𝐴 + 𝐵) → (𝐵 − (𝑁 − 𝐴)) ∈ (0...𝐴))) | ||
| Theorem | fz0addge0 47331 | The sum of two integers in 0-based finite sets of sequential integers is greater than or equal to zero. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
| ⊢ ((𝐴 ∈ (0...𝑀) ∧ 𝐵 ∈ (0...𝑁)) → 0 ≤ (𝐴 + 𝐵)) | ||
| Theorem | elfzlble 47332 | Membership of an integer in a finite set of sequential integers with the integer as upper bound and a lower bound less than or equal to the integer. (Contributed by AV, 21-Oct-2018.) |
| ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑁 ∈ ((𝑁 − 𝑀)...𝑁)) | ||
| Theorem | elfzelfzlble 47333 | Membership of an element of a finite set of sequential integers in a finite set of sequential integers with the same upper bound and a lower bound less than the upper bound. (Contributed by AV, 21-Oct-2018.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁) ∧ 𝑁 < (𝑀 + 𝐾)) → 𝐾 ∈ ((𝑁 − 𝑀)...𝑁)) | ||
| Theorem | fzopred 47334 | Join a predecessor to the beginning of an open integer interval. Generalization of fzo0sn0fzo1 13794. (Contributed by AV, 14-Jul-2020.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁) → (𝑀..^𝑁) = ({𝑀} ∪ ((𝑀 + 1)..^𝑁))) | ||
| Theorem | fzopredsuc 47335 | Join a predecessor and a successor to the beginning and the end of an open integer interval. This theorem holds even if 𝑁 = 𝑀 (then (𝑀...𝑁) = {𝑀} = ({𝑀} ∪ ∅) ∪ {𝑀}). (Contributed by AV, 14-Jul-2020.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁})) | ||
| Theorem | 1fzopredsuc 47336 | Join 0 and a successor to the beginning and the end of an open integer interval starting at 1. (Contributed by AV, 14-Jul-2020.) |
| ⊢ (𝑁 ∈ ℕ0 → (0...𝑁) = (({0} ∪ (1..^𝑁)) ∪ {𝑁})) | ||
| Theorem | el1fzopredsuc 47337 | An element of an open integer interval starting at 1 joined by 0 and a successor at the beginning and the end is either 0 or an element of the open integer interval or the successor. (Contributed by AV, 14-Jul-2020.) |
| ⊢ (𝑁 ∈ ℕ0 → (𝐼 ∈ (0...𝑁) ↔ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁))) | ||
| Theorem | subsubelfzo0 47338 | Subtracting a difference from a number which is not less than the difference results in a bounded nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.) |
| ⊢ ((𝐴 ∈ (0..^𝑁) ∧ 𝐼 ∈ (0..^𝑁) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → (𝐼 − (𝑁 − 𝐴)) ∈ (0..^𝐴)) | ||
| Theorem | 2ffzoeq 47339* | Two functions over a half-open range of nonnegative integers are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 1-Jul-2018.) |
| ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) | ||
| Theorem | fldivmod 47340 | Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (⌊‘(𝐴 / 𝐵)) = ((𝐴 − (𝐴 mod 𝐵)) / 𝐵)) | ||
| Theorem | ceildivmod 47341 | Expressing the ceiling of a division by the modulo operator. (Contributed by AV, 7-Sep-2025.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (⌈‘(𝐴 / 𝐵)) = ((𝐴 + ((𝐵 − 𝐴) mod 𝐵)) / 𝐵)) | ||
| Theorem | ceil5half3 47342 | The ceiling of half of 5 is 3. (Contributed by AV, 7-Sep-2025.) |
| ⊢ (⌈‘(5 / 2)) = 3 | ||
| Theorem | submodaddmod 47343 | Subtraction and addition modulo a positive integer. (Contributed by AV, 7-Sep-2025.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ)) → (((𝐴 + 𝐵) mod 𝑁) = ((𝐴 − 𝐶) mod 𝑁) ↔ ((𝐴 + (𝐵 + 𝐶)) mod 𝑁) = (𝐴 mod 𝑁))) | ||
| Theorem | difltmodne 47344 | Two nonnegative integers are not equal modulo a positive modulus if their difference is greater than 0 and less then the modulus. (Contributed by AV, 6-Sep-2025.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (1 ≤ (𝐴 − 𝐵) ∧ (𝐴 − 𝐵) < 𝑁)) → (𝐴 mod 𝑁) ≠ (𝐵 mod 𝑁)) | ||
| Theorem | zplusmodne 47345 | A nonnegative integer is not itself plus a positive integer modulo an integer greater than 1 and the positive integer. (Contributed by AV, 6-Sep-2025.) |
| ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐴 + 𝐾) mod 𝑁) ≠ (𝐴 mod 𝑁)) | ||
| Theorem | addmodne 47346 | The sum of a nonnegative integer and a positive integer modulo a number greater than both integers is not equal to the nonnegative integer. (Contributed by AV, 27-Aug-2025.) (Proof shortened by AV, 6-Sep-2025.) |
| ⊢ ((𝑀 ∈ ℕ ∧ (𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀) ∧ (𝐵 ∈ ℕ ∧ 𝐵 < 𝑀)) → ((𝐴 + 𝐵) mod 𝑀) ≠ 𝐴) | ||
| Theorem | plusmod5ne 47347 | A nonnegative integer is not itself plus a positive integer less than 5 modulo 5. (Contributed by AV, 6-Sep-2025.) |
| ⊢ ((𝐴 ∈ (0..^5) ∧ 𝐾 ∈ (1..^5)) → ((𝐴 + 𝐾) mod 5) ≠ 𝐴) | ||
| Theorem | zp1modne 47348 | An integer is not itself plus 1 modulo an integer greater than 1. (Contributed by AV, 6-Sep-2025.) |
| ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℤ) → ((𝐴 + 1) mod 𝑁) ≠ (𝐴 mod 𝑁)) | ||
| Theorem | p1modne 47349 | A nonnegative integer is not itself plus 1 modulo an integer greater than 1 and the nonnegative integer. (Contributed by AV, 6-Sep-2025.) |
| ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ (0..^𝑁)) → ((𝐴 + 1) mod 𝑁) ≠ 𝐴) | ||
| Theorem | m1modne 47350 | A nonnegative integer is not itself minus 1 modulo an integer greater than 1 and the nonnegative integer. (Contributed by AV, 6-Sep-2025.) |
| ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ (0..^𝑁)) → ((𝐴 − 1) mod 𝑁) ≠ 𝐴) | ||
| Theorem | minusmod5ne 47351 | A nonnegative integer is not itself minus a positive integer less than 5 modulo 5. (Contributed by AV, 7-Sep-2025.) |
| ⊢ ((𝐴 ∈ (0..^5) ∧ 𝐾 ∈ (1..^5)) → ((𝐴 − 𝐾) mod 5) ≠ 𝐴) | ||
| Theorem | submodlt 47352 | The difference of an element of a half-open range of nonnegative integers and the upper bound of this range modulo an integer greater than the upper bound. (Contributed by AV, 1-Sep-2025.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (0..^𝐵) ∧ 𝐵 < 𝑁) → ((𝐴 − 𝐵) mod 𝑁) = ((𝑁 + 𝐴) − 𝐵)) | ||
| Theorem | submodneaddmod 47353 | An integer minus 𝐵 is not itself plus 𝐶 modulo an integer greater than the sum of 𝐵 and 𝐶. (Contributed by AV, 6-Sep-2025.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (1 ≤ (𝐵 + 𝐶) ∧ (𝐵 + 𝐶) < 𝑁)) → ((𝐴 + 𝐵) mod 𝑁) ≠ ((𝐴 − 𝐶) mod 𝑁)) | ||
| Theorem | m1modnep2mod 47354 | A nonnegative integer minus 1 is not itself plus 2 modulo an integer greater than 3 and the nonnegative integer. (Contributed by AV, 6-Sep-2025.) |
| ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝐴 ∈ ℤ) → ((𝐴 − 1) mod 𝑁) ≠ ((𝐴 + 2) mod 𝑁)) | ||
| Theorem | minusmodnep2tmod 47355 | A nonnegative integer minus a positive integer 1 or 2 is not itself plus 2 times the positive integer modulo 5. (Contributed by AV, 8-Sep-2025.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (1..^3)) → ((𝐴 − 𝐵) mod 5) ≠ ((𝐴 + (2 · 𝐵)) mod 5)) | ||
| Theorem | m1mod0mod1 47356 | An integer decreased by 1 is 0 modulo a positive integer iff the integer is 1 modulo the same modulus. (Contributed by AV, 6-Jun-2020.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 < 𝑁) → (((𝐴 − 1) mod 𝑁) = 0 ↔ (𝐴 mod 𝑁) = 1)) | ||
| Theorem | elmod2 47357 | An integer modulo 2 is either 0 or 1. (Contributed by AV, 24-May-2020.) (Proof shortened by OpenAI, 3-Jul-2020.) |
| ⊢ (𝑁 ∈ ℤ → (𝑁 mod 2) ∈ {0, 1}) | ||
| Theorem | smonoord 47358* | Ordering relation for a strictly monotonic sequence, increasing case. Analogous to monoord 14073 (except that the case 𝑀 = 𝑁 must be excluded). Duplicate of monoords 45309? (Contributed by AV, 12-Jul-2020.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) < (𝐹‘𝑁)) | ||
| Theorem | fsummsndifre 47359* | A finite sum with one of its integer summands removed is a real number. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
| ⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∖ {𝑋})𝐵 ∈ ℝ) | ||
| Theorem | fsumsplitsndif 47360* | Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ 𝐴 𝐵 = (Σ𝑘 ∈ (𝐴 ∖ {𝑋})𝐵 + ⦋𝑋 / 𝑘⦌𝐵)) | ||
| Theorem | fsummmodsndifre 47361* | A finite sum of summands modulo a positive number with one of its summands removed is a real number. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∖ {𝑋})(𝐵 mod 𝑁) ∈ ℝ) | ||
| Theorem | fsummmodsnunz 47362* | A finite sum of summands modulo a positive number with an additional summand is an integer. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∪ {𝑧})(𝐵 mod 𝑁) ∈ ℤ) | ||
| Theorem | setsidel 47363 | The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.) |
| ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝑅 = (𝑆 sSet 〈𝐴, 𝐵〉) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ 𝑅) | ||
| Theorem | setsnidel 47364 | The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.) |
| ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝑅 = (𝑆 sSet 〈𝐴, 𝐵〉) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ 𝑅) | ||
| Theorem | setsv 47365 | The value of the structure replacement function is a set. (Contributed by AV, 10-Nov-2021.) |
| ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet 〈𝐴, 𝐵〉) ∈ V) | ||
According to Wikipedia ("Image (mathematics)", 17-Mar-2024, https://en.wikipedia.org/wiki/ImageSupport_(mathematics)): "... evaluating a given function 𝑓 at each element of a given subset 𝐴 of its domain produces a set, called the "image of 𝐴 under (or through) 𝑓". Similarly, the inverse image (or preimage) of a given subset 𝐵 of the codomain of 𝑓 is the set of all elements of the domain that map to the members of 𝐵." The preimage of a set 𝐵 under a function 𝑓 is often denoted as "f^-1 (B)", but in set.mm, the idiom (◡𝑓 “ 𝐵) is used. As a special case, the idiom for the preimage of a function value at 𝑋 under a function 𝐹 is (◡𝐹 “ {(𝐹‘𝑋)}) (according to Wikipedia, the preimage of a singleton is also called a "fiber"). We use the label fragment "preima" (as in mptpreima 6258) for theorems about preimages (sometimes, also "imacnv" is used as in fvimacnvi 7072), and "preimafv" (as in preimafvn0 47367) for theorems about preimages of a function value. In this section, 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} will be the set of all preimages of function values of a function 𝐹, that means 𝑆 ∈ 𝑃 is a preimage of a function value (see, for example, elsetpreimafv 47372): 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)}). With the help of such a set, it is shown that every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective and an injective function (see fundcmpsurinj 47396) by constructing a surjective function 𝑔:𝐴–onto→𝑃 and an injective function ℎ:𝑃–1-1→𝐵 so that 𝐹 = (ℎ ∘ 𝑔) ( see fundcmpsurinjpreimafv 47395). See also Wikipedia ("Surjective function", 17-Mar-2024, https://en.wikipedia.org/wiki/Surjective_function 47395 (section "Composition and decomposition"). This is different from the decomposition of 𝐹 into the surjective function 𝑔:𝐴–onto→(𝐹 “ 𝐴) (with (𝑔‘𝑥) = (𝐹‘𝑥) for 𝑥 ∈ 𝐴) and the injective function ℎ = ( I ↾ (𝐹 “ 𝐴)), ( see fundcmpsurinjimaid 47398), see also Wikipedia ("Bijection, injection and surjection", 17-Mar-2024, https://en.wikipedia.org/wiki/Bijection,_injection_and_surjection 47398 (section "Properties"). Finally, it is shown that every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective, a bijective and an injective function (see fundcmpsurbijinj 47397), by showing that there is a bijection between the set of all preimages of values of a function and the range of the function (see imasetpreimafvbij 47393). From this, both variants of decompositions of a function into a surjective and an injective function can be derived: Let 𝐹 = ((𝐼 ∘ 𝐵) ∘ 𝑆) be a decomposition of a function into a surjective, a bijective and an injective function, then 𝐹 = (𝐽 ∘ 𝑆) with 𝐽 = (𝐼 ∘ 𝐵) (an injective function) is a decomposition into a surjective and an injective function corresponding to fundcmpsurinj 47396, and 𝐹 = (𝐼 ∘ 𝑂) with 𝑂 = (𝐵 ∘ 𝑆) (a surjective function) is a decomposition into a surjective and an injective function corresponding to fundcmpsurinjimaid 47398. | ||
| Theorem | preimafvsnel 47366 | The preimage of a function value at 𝑋 contains 𝑋. (Contributed by AV, 7-Mar-2024.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ (◡𝐹 “ {(𝐹‘𝑋)})) | ||
| Theorem | preimafvn0 47367 | The preimage of a function value is not empty. (Contributed by AV, 7-Mar-2024.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (◡𝐹 “ {(𝐹‘𝑋)}) ≠ ∅) | ||
| Theorem | uniimafveqt 47368* | The union of the image of a subset 𝑆 of the domain of a function with elements having the same function value is the function value at one of the elements of 𝑆. (Contributed by AV, 5-Mar-2024.) |
| ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (∀𝑥 ∈ 𝑆 (𝐹‘𝑥) = (𝐹‘𝑋) → ∪ (𝐹 “ 𝑆) = (𝐹‘𝑋))) | ||
| Theorem | uniimaprimaeqfv 47369 | The union of the image of the preimage of a function value is the function value. (Contributed by AV, 12-Mar-2024.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∪ (𝐹 “ (◡𝐹 “ {(𝐹‘𝑋)})) = (𝐹‘𝑋)) | ||
| Theorem | setpreimafvex 47370* | The class 𝑃 of all preimages of function values is a set. (Contributed by AV, 10-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝑃 ∈ V) | ||
| Theorem | elsetpreimafvb 47371* | The characterization of an element of the class 𝑃 of all preimages of function values. (Contributed by AV, 10-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ 𝑃 ↔ ∃𝑥 ∈ 𝐴 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)}))) | ||
| Theorem | elsetpreimafv 47372* | An element of the class 𝑃 of all preimages of function values. (Contributed by AV, 8-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ (𝑆 ∈ 𝑃 → ∃𝑥 ∈ 𝐴 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)})) | ||
| Theorem | elsetpreimafvssdm 47373* | An element of the class 𝑃 of all preimages of function values is a subset of the domain of the function. (Contributed by AV, 8-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃) → 𝑆 ⊆ 𝐴) | ||
| Theorem | fvelsetpreimafv 47374* | There is an element in a preimage 𝑆 of function values so that 𝑆 is the preimage of the function value at this element. (Contributed by AV, 8-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃) → ∃𝑥 ∈ 𝑆 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)})) | ||
| Theorem | preimafvelsetpreimafv 47375* | The preimage of a function value is an element of the class 𝑃 of all preimages of function values. (Contributed by AV, 10-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → (◡𝐹 “ {(𝐹‘𝑋)}) ∈ 𝑃) | ||
| Theorem | preimafvsspwdm 47376* | The class 𝑃 of all preimages of function values is a subset of the power set of the domain of the function. (Contributed by AV, 5-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ (𝐹 Fn 𝐴 → 𝑃 ⊆ 𝒫 𝐴) | ||
| Theorem | 0nelsetpreimafv 47377* | The empty set is not an element of the class 𝑃 of all preimages of function values. (Contributed by AV, 6-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ (𝐹 Fn 𝐴 → ∅ ∉ 𝑃) | ||
| Theorem | elsetpreimafvbi 47378* | An element of the preimage of a function value is an element of the domain of the function with the same value as another element of the preimage. (Contributed by AV, 9-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆) → (𝑌 ∈ 𝑆 ↔ (𝑌 ∈ 𝐴 ∧ (𝐹‘𝑌) = (𝐹‘𝑋)))) | ||
| Theorem | elsetpreimafveqfv 47379* | The elements of the preimage of a function value have the same function values. (Contributed by AV, 5-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ (𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝐹‘𝑋) = (𝐹‘𝑌)) | ||
| Theorem | eqfvelsetpreimafv 47380* | If an element of the domain of the function has the same function value as an element of the preimage of a function value, then it is an element of the same preimage. (Contributed by AV, 9-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆) → ((𝑌 ∈ 𝐴 ∧ (𝐹‘𝑌) = (𝐹‘𝑋)) → 𝑌 ∈ 𝑆)) | ||
| Theorem | elsetpreimafvrab 47381* | An element of the preimage of a function value expressed as a restricted class abstraction. (Contributed by AV, 9-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆) → 𝑆 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = (𝐹‘𝑋)}) | ||
| Theorem | imaelsetpreimafv 47382* | The image of an element of the preimage of a function value is the singleton consisting of the function value at one of its elements. (Contributed by AV, 5-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆) → (𝐹 “ 𝑆) = {(𝐹‘𝑋)}) | ||
| Theorem | uniimaelsetpreimafv 47383* | The union of the image of an element of the preimage of a function value is an element of the range of the function. (Contributed by AV, 5-Mar-2024.) (Revised by AV, 22-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃) → ∪ (𝐹 “ 𝑆) ∈ ran 𝐹) | ||
| Theorem | elsetpreimafveq 47384* | If two preimages of function values contain elements with identical function values, then both preimages are equal. (Contributed by AV, 8-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ (𝑆 ∈ 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑋) = (𝐹‘𝑌) → 𝑆 = 𝑅)) | ||
| Theorem | fundcmpsurinjlem1 47385* | Lemma 1 for fundcmpsurinj 47396. (Contributed by AV, 4-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (◡𝐹 “ {(𝐹‘𝑥)})) ⇒ ⊢ ran 𝐺 = 𝑃 | ||
| Theorem | fundcmpsurinjlem2 47386* | Lemma 2 for fundcmpsurinj 47396. (Contributed by AV, 4-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (◡𝐹 “ {(𝐹‘𝑥)})) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐺:𝐴–onto→𝑃) | ||
| Theorem | fundcmpsurinjlem3 47387* | Lemma 3 for fundcmpsurinj 47396. (Contributed by AV, 3-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ ((Fun 𝐹 ∧ 𝑋 ∈ 𝑃) → (𝐻‘𝑋) = ∪ (𝐹 “ 𝑋)) | ||
| Theorem | imasetpreimafvbijlemf 47388* | Lemma for imasetpreimafvbij 47393: the mapping 𝐻 is a function into the range of function 𝐹. (Contributed by AV, 22-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ (𝐹 Fn 𝐴 → 𝐻:𝑃⟶(𝐹 “ 𝐴)) | ||
| Theorem | imasetpreimafvbijlemfv 47389* | Lemma for imasetpreimafvbij 47393: the value of the mapping 𝐻 at a preimage of a value of function 𝐹. (Contributed by AV, 5-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌) → (𝐻‘𝑌) = (𝐹‘𝑋)) | ||
| Theorem | imasetpreimafvbijlemfv1 47390* | Lemma for imasetpreimafvbij 47393: for a preimage of a value of function 𝐹 there is an element of the preimage so that the value of the mapping 𝐻 at this preimage is the function value at this element. (Contributed by AV, 5-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝑃) → ∃𝑦 ∈ 𝑋 (𝐻‘𝑋) = (𝐹‘𝑦)) | ||
| Theorem | imasetpreimafvbijlemf1 47391* | Lemma for imasetpreimafvbij 47393: the mapping 𝐻 is an injective function into the range of function 𝐹. (Contributed by AV, 9-Mar-2024.) (Revised by AV, 22-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ (𝐹 Fn 𝐴 → 𝐻:𝑃–1-1→(𝐹 “ 𝐴)) | ||
| Theorem | imasetpreimafvbijlemfo 47392* | Lemma for imasetpreimafvbij 47393: the mapping 𝐻 is a function onto the range of function 𝐹. (Contributed by AV, 22-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐻:𝑃–onto→(𝐹 “ 𝐴)) | ||
| Theorem | imasetpreimafvbij 47393* | The mapping 𝐻 is a bijective function between the set 𝑃 of all preimages of values of function 𝐹 and the range of 𝐹. (Contributed by AV, 22-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐻:𝑃–1-1-onto→(𝐹 “ 𝐴)) | ||
| Theorem | fundcmpsurbijinjpreimafv 47394* | Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective function onto 𝑃, a bijective function from 𝑃 and an injective function into the codomain of 𝐹. (Contributed by AV, 22-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → ∃𝑔∃ℎ∃𝑖((𝑔:𝐴–onto→𝑃 ∧ ℎ:𝑃–1-1-onto→(𝐹 “ 𝐴) ∧ 𝑖:(𝐹 “ 𝐴)–1-1→𝐵) ∧ 𝐹 = ((𝑖 ∘ ℎ) ∘ 𝑔))) | ||
| Theorem | fundcmpsurinjpreimafv 47395* | Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective function onto 𝑃 and an injective function from 𝑃. (Contributed by AV, 12-Mar-2024.) (Proof shortened by AV, 22-Mar-2024.) |
| ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → ∃𝑔∃ℎ(𝑔:𝐴–onto→𝑃 ∧ ℎ:𝑃–1-1→𝐵 ∧ 𝐹 = (ℎ ∘ 𝑔))) | ||
| Theorem | fundcmpsurinj 47396* | Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective and an injective function. (Contributed by AV, 13-Mar-2024.) |
| ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → ∃𝑔∃ℎ∃𝑝(𝑔:𝐴–onto→𝑝 ∧ ℎ:𝑝–1-1→𝐵 ∧ 𝐹 = (ℎ ∘ 𝑔))) | ||
| Theorem | fundcmpsurbijinj 47397* | Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective, a bijective and an injective function. (Contributed by AV, 23-Mar-2024.) |
| ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → ∃𝑔∃ℎ∃𝑖∃𝑝∃𝑞((𝑔:𝐴–onto→𝑝 ∧ ℎ:𝑝–1-1-onto→𝑞 ∧ 𝑖:𝑞–1-1→𝐵) ∧ 𝐹 = ((𝑖 ∘ ℎ) ∘ 𝑔))) | ||
| Theorem | fundcmpsurinjimaid 47398* | Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective function onto the image (𝐹 “ 𝐴) of the domain of 𝐹 and an injective function from the image (𝐹 “ 𝐴). (Contributed by AV, 17-Mar-2024.) |
| ⊢ 𝐼 = (𝐹 “ 𝐴) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) & ⊢ 𝐻 = ( I ↾ 𝐼) ⇒ ⊢ (𝐹:𝐴⟶𝐵 → (𝐺:𝐴–onto→𝐼 ∧ 𝐻:𝐼–1-1→𝐵 ∧ 𝐹 = (𝐻 ∘ 𝐺))) | ||
| Theorem | fundcmpsurinjALT 47399* | Alternate proof of fundcmpsurinj 47396, based on fundcmpsurinjimaid 47398: Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective and an injective function. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by AV, 13-Mar-2024.) |
| ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → ∃𝑔∃ℎ∃𝑝(𝑔:𝐴–onto→𝑝 ∧ ℎ:𝑝–1-1→𝐵 ∧ 𝐹 = (ℎ ∘ 𝑔))) | ||
Based on the theorems of the fourierdlem* series of GS's mathbox. | ||
| Syntax | ciccp 47400 | Extend class notation with the partitions of a closed interval of extended reals. |
| class RePart | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |