Home | Metamath
Proof Explorer Theorem List (p. 436 of 450) | < 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: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | imarnf1pr 43501 | The image of the range of a function 𝐹 under a function 𝐸 if 𝐹 is a function from a pair into the domain of 𝐸. (Contributed by Alexander van der Vekens, 2-Feb-2018.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (((𝐹:{𝑋, 𝑌}⟶dom 𝐸 ∧ 𝐸:dom 𝐸⟶𝑅) ∧ ((𝐸‘(𝐹‘𝑋)) = 𝐴 ∧ (𝐸‘(𝐹‘𝑌)) = 𝐵)) → (𝐸 “ ran 𝐹) = {𝐴, 𝐵})) | ||
Theorem | funop1 43502* | A function is an ordered pair iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.) |
⊢ (∃𝑥∃𝑦 𝐹 = 〈𝑥, 𝑦〉 → (Fun 𝐹 ↔ ∃𝑥∃𝑦 𝐹 = {〈𝑥, 𝑦〉})) | ||
Theorem | fun2dmnopgexmpl 43503 | A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 21-Sep-2020.) (Avoid depending on this detail.) |
⊢ (𝐺 = {〈0, 1〉, 〈1, 1〉} → ¬ 𝐺 ∈ (V × V)) | ||
Theorem | opabresex0d 43504* | A collection of ordered pairs, the class of all possible second components being a set, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 1-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝜃) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → {𝑦 ∣ 𝜃} ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥𝑅𝑦 ∧ 𝜓)} ∈ V) | ||
Theorem | opabbrfex0d 43505* | A collection of ordered pairs, the class of all possible second components being a set, is a set. (Contributed by AV, 15-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝜃) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → {𝑦 ∣ 𝜃} ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} ∈ V) | ||
Theorem | opabresexd 43506* | A collection of ordered pairs, the second component being a function, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 15-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥𝑅𝑦 ∧ 𝜓)} ∈ V) | ||
Theorem | opabbrfexd 43507* | A collection of ordered pairs, the second component being a function, is a set. (Contributed by AV, 15-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} ∈ V) | ||
Theorem | f1oresf1orab 43508* | Build a bijection by restricting the domain of a bijection. (Contributed by AV, 1-Aug-2022.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) → (𝜒 ↔ 𝑥 ∈ 𝐷)) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | f1oresf1o 43509* | Build a bijection by restricting the domain of a bijection. (Contributed by AV, 31-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ (𝜑 → (∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦 ↔ (𝑦 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | f1oresf1o2 43510* | Build a bijection by restricting the domain of a bijection. (Contributed by AV, 31-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → (𝑥 ∈ 𝐷 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | fvmptrab 43511* | 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 6799, 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 43512* | Value of a function mapping a set to a class abstraction restricting the value of another function. See also fvmptrabfv 6799. (Suggested by BJ, 18-Feb-2022.) (Contributed by AV, 18-Feb-2022.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ (𝐺‘𝑌) ∣ 𝜑}) & ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜓)) & ⊢ (𝑌 ∈ dom 𝐺 → 𝑋 ∈ dom 𝐹) ⇒ ⊢ (𝐹‘𝑋) = {𝑦 ∈ (𝐺‘𝑌) ∣ 𝜓} | ||
Theorem | leltletr 43513 | Transitive law, weaker form of lelttr 10731. (Contributed by AV, 14-Oct-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶)) | ||
Theorem | cnambpcma 43514 | ((a-b)+c)-a = c-a holds for complex numbers a,b,c. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) + 𝐶) − 𝐴) = (𝐶 − 𝐵)) | ||
Theorem | cnapbmcpd 43515 | ((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 43516 | 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 43517 | Addition and subtraction on one side of "less than or equal to". (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ ((𝐴 + 𝐵) − 𝐶) ≤ 𝐴)) | ||
Theorem | 2leaddle2 43518 | 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 43519 | Variant of trichotomy law for 'less than'. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (¬ 𝐵 < 𝐴 ∧ ¬ 𝐵 = 𝐴))) | ||
Theorem | p1lep2 43520 | 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 43521 | 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 43522 | An integer minus 1 is positive under certain circumstances. (Contributed by Alexander van der Vekens, 9-Jun-2018.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝐽 ∈ ℝ ∧ 0 ≤ 𝐽 ∧ 𝐽 < ((𝐿 − 𝑁) − 1)) → (𝐿 − 1) ∈ ℕ)) | ||
Theorem | readdcnnred 43523 | The sum of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ)) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∉ ℝ) | ||
Theorem | resubcnnred 43524 | The difference of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ∉ ℝ) | ||
Theorem | recnmulnred 43525 | The product of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ)) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∉ ℝ) | ||
Theorem | cndivrenred 43526 | The quotient of an imaginary number and a real number is not a real number. (Contributed by AV, 23-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ)) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (𝐵 / 𝐴) ∉ ℝ) | ||
Theorem | sqrtnegnre 43527 | The square root of a negative number is not a real number. (Contributed by AV, 28-Feb-2023.) |
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → (√‘𝑋) ∉ ℝ) | ||
Theorem | nn0resubcl 43528 | Closure law for subtraction of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 − 𝐵) ∈ ℝ) | ||
Theorem | zgeltp1eq 43529 | 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 43530 | 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 43531 | Add 1 to a 2 digit number with carry. This is a special case of decsucc 12140, 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 43532 | 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 43533 | Negated extended trichotomy law for 'less than' and 'less than or equal to'. (Contributed by AV, 18-Jul-2020.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴)) | ||
Theorem | ssfz12 43534 | Subset relationship for finite sets of sequential integers. (Contributed by Alexander van der Vekens, 16-Mar-2018.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿) → ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) | ||
Theorem | elfz2z 43535 | 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 43536 | 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 43537 | 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 43538 | 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 43539 | 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 43540 | 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 43541 | 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 43542 | Join a predecessor to the beginning of an open integer interval. Generalization of fzo0sn0fzo1 13127. (Contributed by AV, 14-Jul-2020.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁) → (𝑀..^𝑁) = ({𝑀} ∪ ((𝑀 + 1)..^𝑁))) | ||
Theorem | fzopredsuc 43543 | 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 43544 | 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 43545 | 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 43546 | 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 | fzoopth 43547 | A half-open integer range can represent an ordered pair, analogous to fzopth 12945. (Contributed by Alexander van der Vekens, 1-Jul-2018.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) = (𝐽..^𝐾) ↔ (𝑀 = 𝐽 ∧ 𝑁 = 𝐾))) | ||
Theorem | 2ffzoeq 43548* | 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 | m1mod0mod1 43549 | 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 43550 | 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 43551* | Ordering relation for a strictly monotonic sequence, increasing case. Analogous to monoord 13401 (except that the case 𝑀 = 𝑁 must be excluded). Duplicate of monoords 41584? (Contributed by AV, 12-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) < (𝐹‘𝑁)) | ||
Theorem | fsummsndifre 43552* | 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 43553* | 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 43554* | 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 43555* | 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 43556 | The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝑅 = (𝑆 sSet 〈𝐴, 𝐵〉) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ 𝑅) | ||
Theorem | setsnidel 43557 | The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝑅 = (𝑆 sSet 〈𝐴, 𝐵〉) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ 𝑅) | ||
Theorem | setsv 43558 | 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 6092) for theorems about preimages (sometimes, also "imacnv" is used as in fvimacnvi 6822), and "preimafv" (as in preimafvn0 43560) 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 43565): 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)}). 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 43589) by constructing a surjective function 𝑔:𝐴–onto→𝑃 and an injective function ℎ:𝑃–1-1→𝐵 so that 𝐹 = (ℎ ∘ 𝑔) ( see fundcmpsurinjpreimafv 43588). See also Wikipedia ("Surjective function", 17-Mar-2024, https://en.wikipedia.org/wiki/Surjective_function 43588 (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 43591), see also Wikipedia ("Bijection, injection and surjection", 17-Mar-2024, https://en.wikipedia.org/wiki/Bijection,_injection_and_surjection 43591 (section "Properties"). Finally, it is shown that every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective, a bijective and an injective function (see fundcmpsurbijinj 43590), 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 43586). 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 43589, and 𝐹 = (𝐼 ∘ 𝑂) with 𝑂 = (𝐵 ∘ 𝑆) (a surjective function) is a decomposition into a surjective and an injective function corresponding to fundcmpsurinjimaid 43591. | ||
Theorem | preimafvsnel 43559 | The preimage of a function value at 𝑋 contains 𝑋. (Contributed by AV, 7-Mar-2024.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ (◡𝐹 “ {(𝐹‘𝑋)})) | ||
Theorem | preimafvn0 43560 | The preimage of a function value is not empty. (Contributed by AV, 7-Mar-2024.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (◡𝐹 “ {(𝐹‘𝑋)}) ≠ ∅) | ||
Theorem | uniimafveqt 43561* | 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 43562 | 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 43563* | The class 𝑃 of all preimages of function values is a set. (Contributed by AV, 10-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝑃 ∈ V) | ||
Theorem | elsetpreimafvb 43564* | The characterization of an element of the class 𝑃 of all preimages of function values. (Contributed by AV, 10-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ 𝑃 ↔ ∃𝑥 ∈ 𝐴 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)}))) | ||
Theorem | elsetpreimafv 43565* | An element of the class 𝑃 of all preimages of function values. (Contributed by AV, 8-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ (𝑆 ∈ 𝑃 → ∃𝑥 ∈ 𝐴 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)})) | ||
Theorem | elsetpreimafvssdm 43566* | 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 43567* | 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 43568* | 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 43569* | 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 43570* | 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 43571* | 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 43572* | The elements of the preimage of a function value have the same function values. (Contributed by AV, 5-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ (𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝐹‘𝑋) = (𝐹‘𝑌)) | ||
Theorem | eqfvelsetpreimafv 43573* | 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 43574* | An element of the preimage of a function value expressed as a restricted class abstraction. (Contributed by AV, 9-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆) → 𝑆 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = (𝐹‘𝑋)}) | ||
Theorem | imaelsetpreimafv 43575* | 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 43576* | 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 43577* | 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 43578* | Lemma 1 for fundcmpsurinj 43589. (Contributed by AV, 4-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (◡𝐹 “ {(𝐹‘𝑥)})) ⇒ ⊢ ran 𝐺 = 𝑃 | ||
Theorem | fundcmpsurinjlem2 43579* | Lemma 2 for fundcmpsurinj 43589. (Contributed by AV, 4-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (◡𝐹 “ {(𝐹‘𝑥)})) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐺:𝐴–onto→𝑃) | ||
Theorem | fundcmpsurinjlem3 43580* | Lemma 3 for fundcmpsurinj 43589. (Contributed by AV, 3-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ ((Fun 𝐹 ∧ 𝑋 ∈ 𝑃) → (𝐻‘𝑋) = ∪ (𝐹 “ 𝑋)) | ||
Theorem | imasetpreimafvbijlemf 43581* | Lemma for imasetpreimafvbij 43586: the mapping 𝐻 is a function into the range of function 𝐹. (Contributed by AV, 22-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ (𝐹 Fn 𝐴 → 𝐻:𝑃⟶(𝐹 “ 𝐴)) | ||
Theorem | imasetpreimafvbijlemfv 43582* | Lemma for imasetpreimafvbij 43586: the value of the mapping 𝐻 at a preimage of a value of function 𝐹. (Contributed by AV, 5-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌) → (𝐻‘𝑌) = (𝐹‘𝑋)) | ||
Theorem | imasetpreimafvbijlemfv1 43583* | Lemma for imasetpreimafvbij 43586: 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 43584* | Lemma for imasetpreimafvbij 43586: 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 43585* | Lemma for imasetpreimafvbij 43586: the mapping 𝐻 is a function onto the range of function 𝐹. (Contributed by AV, 22-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐻:𝑃–onto→(𝐹 “ 𝐴)) | ||
Theorem | imasetpreimafvbij 43586* | The mapping 𝐻 is a bijective function betwen 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 43587* | 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 43588* | 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 43589* | Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective and an injective function. (Contributed by AV, 13-Mar-2024.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → ∃𝑔∃ℎ∃𝑝(𝑔:𝐴–onto→𝑝 ∧ ℎ:𝑝–1-1→𝐵 ∧ 𝐹 = (ℎ ∘ 𝑔))) | ||
Theorem | fundcmpsurbijinj 43590* | 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 43591* | 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 43592* | Alternate proof of fundcmpsurinj 43589, based on fundcmpsurinjimaid 43591: 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 43593 | Extend class notation with the partitions of a closed interval of extended reals. |
class RePart | ||
Definition | df-iccp 43594* | Define partitions of a closed interval of extended reals. Such partitions are finite increasing sequences of extended reals. (Contributed by AV, 8-Jul-2020.) |
⊢ RePart = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ* ↑m (0...𝑚)) ∣ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))}) | ||
Theorem | iccpval 43595* | Partition consisting of a fixed number 𝑀 of parts. (Contributed by AV, 9-Jul-2020.) |
⊢ (𝑀 ∈ ℕ → (RePart‘𝑀) = {𝑝 ∈ (ℝ* ↑m (0...𝑀)) ∣ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))}) | ||
Theorem | iccpart 43596* | A special partition. Corresponds to fourierdlem2 42414 in GS's mathbox. (Contributed by AV, 9-Jul-2020.) |
⊢ (𝑀 ∈ ℕ → (𝑃 ∈ (RePart‘𝑀) ↔ (𝑃 ∈ (ℝ* ↑m (0...𝑀)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑃‘𝑖) < (𝑃‘(𝑖 + 1))))) | ||
Theorem | iccpartimp 43597 | Implications for a class being a partition. (Contributed by AV, 11-Jul-2020.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑃 ∈ (RePart‘𝑀) ∧ 𝐼 ∈ (0..^𝑀)) → (𝑃 ∈ (ℝ* ↑m (0...𝑀)) ∧ (𝑃‘𝐼) < (𝑃‘(𝐼 + 1)))) | ||
Theorem | iccpartres 43598 | The restriction of a partition is a partition. (Contributed by AV, 16-Jul-2020.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑃 ∈ (RePart‘(𝑀 + 1))) → (𝑃 ↾ (0...𝑀)) ∈ (RePart‘𝑀)) | ||
Theorem | iccpartxr 43599 | If there is a partition, then all intermediate points and bounds are extended real numbers. (Contributed by AV, 11-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝐼 ∈ (0...𝑀)) ⇒ ⊢ (𝜑 → (𝑃‘𝐼) ∈ ℝ*) | ||
Theorem | iccpartgtprec 43600 | If there is a partition, then all intermediate points and the upper bound are strictly greater than the preceeding intermediate points or lower bound. (Contributed by AV, 11-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑀)) ⇒ ⊢ (𝜑 → (𝑃‘(𝐼 − 1)) < (𝑃‘𝐼)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |