HomeTheorem List (p. 428 of 466)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 428 of 466) | < 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-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | resabs1i 42701 | Absorption law for restriction. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
| ⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵) | ||
| Theorem | nel1nelin 42702 | Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
| ⊢ (¬ 𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐵 ∩ 𝐶)) | ||
| Theorem | nel2nelin 42703 | Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
| ⊢ (¬ 𝐴 ∈ 𝐶 → ¬ 𝐴 ∈ (𝐵 ∩ 𝐶)) | ||
| Theorem | nel1nelini 42704 | Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
| ⊢ ¬ 𝐴 ∈ 𝐵 ⇒ ⊢ ¬ 𝐴 ∈ (𝐵 ∩ 𝐶) | ||
| Theorem | nel2nelini 42705 | Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
| ⊢ ¬ 𝐴 ∈ 𝐶 ⇒ ⊢ ¬ 𝐴 ∈ (𝐵 ∩ 𝐶) | ||
| Theorem | eliunid 42706* | Membership in indexed union. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
| ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) | ||
| Theorem | reximddv3 42707* | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
| ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) | ||
| Theorem | reximdd 42708 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) | ||
| Theorem | unfid 42709 | The union of two finite sets is finite. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ Fin) | ||
| Theorem | feq1dd 42710 | Equality deduction for functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) | ||
| Theorem | fnresdmss 42711 | A function does not change when restricted to a set that contains its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐹 ↾ 𝐵) = 𝐹) | ||
| Theorem | fmptsnxp 42712* | Maps-to notation and Cartesian product for a singleton function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ {𝐴} ↦ 𝐵) = ({𝐴} × {𝐵})) | ||
| Theorem | fvmpt2bd 42713* | Value of a function given by the maps-to notation. Deduction version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐹‘𝑥) = 𝐵) | ||
| Theorem | rnmptfi 42714* | The range of a function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (𝐵 ∈ Fin → ran 𝐴 ∈ Fin) | ||
| Theorem | fresin2 42715 | Restriction of a function with respect to the intersection with its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ↾ (𝐶 ∩ 𝐴)) = (𝐹 ↾ 𝐶)) | ||
| Theorem | ffi 42716 | A function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ Fin) → 𝐹 ∈ Fin) | ||
| Theorem | suprnmpt 42717* | An explicit bound for the range of a bounded function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐶 = sup(ran 𝐹, ℝ, < ) ⇒ ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) | ||
| Theorem | rnffi 42718 | The range of a function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ Fin) → ran 𝐹 ∈ Fin) | ||
| Theorem | mptelpm 42719* | A function in maps-to notation is a partial map . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ (𝜑 → 𝐴 ⊆ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐶 ↑pm 𝐷)) | ||
| Theorem | rnmptpr 42720* | Range of a function defined on an unordered pair. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝐹 = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐶) & ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ (𝜑 → ran 𝐹 = {𝐷, 𝐸}) | ||
| Theorem | resmpti 42721* | Restriction of the mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ 𝐵 ⊆ 𝐴 ⇒ ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶) | ||
| Theorem | founiiun 42722* | Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝐹:𝐴–onto→𝐵 → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) | ||
| Theorem | rnresun 42723 | Distribution law for range of a restriction over a union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ran (𝐹 ↾ (𝐴 ∪ 𝐵)) = (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵)) | ||
| Theorem | dffo3f 42724* | An onto mapping expressed in terms of function values. As dffo3 6987 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) | ||
| Theorem | elrnmptf 42725 | The range of a function in maps-to notation. Same as elrnmpt 5868, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) | ||
| Theorem | rnmptssrn 42726* | Inclusion relation for two ranges expressed in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐶 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ran (𝑦 ∈ 𝐶 ↦ 𝐷)) | ||
| Theorem | disjf1 42727* | A 1 to 1 mapping built from disjoint, nonempty sets. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1→𝑉) | ||
| Theorem | rnsnf 42728 | The range of a function whose domain is a singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:{𝐴}⟶𝐵) ⇒ ⊢ (𝜑 → ran 𝐹 = {(𝐹‘𝐴)}) | ||
| Theorem | wessf1ornlem 42729* | Given a function 𝐹 on a well-ordered domain 𝐴 there exists a subset of 𝐴 such that 𝐹 restricted to such subset is injective and onto the range of 𝐹 (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹) | ||
| Theorem | wessf1orn 42730* | Given a function 𝐹 on a well-ordered domain 𝐴 there exists a subset of 𝐴 such that 𝐹 restricted to such subset is injective and onto the range of 𝐹 (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 We 𝐴) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹) | ||
| Theorem | foelrnf 42731* | Property of a surjective function. As foelrn 6991 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥)) | ||
| Theorem | nelrnres 42732 | If 𝐴 is not in the range, it is not in the range of any restriction. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (¬ 𝐴 ∈ ran 𝐵 → ¬ 𝐴 ∈ ran (𝐵 ↾ 𝐶)) | ||
| Theorem | disjrnmpt2 42733* | Disjointness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran 𝐹 𝑦) | ||
| Theorem | elrnmpt1sf 42734* | Elementhood in an image set. Same as elrnmpt1s 5869, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶) ⇒ ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹) | ||
| Theorem | founiiun0 42735* | Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) | ||
| Theorem | disjf1o 42736* | A bijection built from disjoint sets. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅} & ⊢ 𝐷 = (ran 𝐹 ∖ {∅}) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶–1-1-onto→𝐷) | ||
| Theorem | fompt 42737* | Express being onto for a mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝐹:𝐴–onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = 𝐶)) | ||
| Theorem | disjinfi 42738* | Only a finite number of disjoint sets can have a nonempty intersection with a finite set 𝐶. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ (𝜑 → 𝐶 ∈ Fin) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin) | ||
| Theorem | fvovco 42739 | Value of the composition of an operator, with a given function. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| ⊢ (𝜑 → 𝐹:𝑋⟶(𝑉 × 𝑊)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝑂 ∘ 𝐹)‘𝑌) = ((1st ‘(𝐹‘𝑌))𝑂(2nd ‘(𝐹‘𝑌)))) | ||
| Theorem | ssnnf1octb 42740* | There exists a bijection between a subset of ℕ and a given nonempty countable set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| ⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → ∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝐴)) | ||
| Theorem | nnf1oxpnn 42741 | There is a bijection between the set of positive integers and the Cartesian product of the set of positive integers with itself. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| ⊢ ∃𝑓 𝑓:ℕ–1-1-onto→(ℕ × ℕ) | ||
| Theorem | rnmptssd 42742* | The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶) | ||
| Theorem | projf1o 42743* | A biijection from a set to a projection in a two dimensional space. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ⟨𝐴, 𝑥⟩) ⇒ ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→({𝐴} × 𝐵)) | ||
| Theorem | fvmap 42744 | Function value for a member of a set exponentiation. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ (𝐴 ↑m 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐴) | ||
| Theorem | fvixp2 42745* | Projection of a factor of an indexed Cartesian product. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) | ||
| Theorem | fidmfisupp 42746 | A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝐹:𝐷⟶𝑅) & ⊢ (𝜑 → 𝐷 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
| Theorem | choicefi 42747* | For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)) | ||
| Theorem | mpct 42748 | The exponentiation of a countable set to a finite set is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝐴 ≼ ω) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → (𝐴 ↑m 𝐵) ≼ ω) | ||
| Theorem | cnmetcoval 42749 | Value of the distance function of the metric space of complex numbers, composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ 𝐷 = (abs ∘ − ) & ⊢ (𝜑 → 𝐹:𝐴⟶(ℂ × ℂ)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝐷 ∘ 𝐹)‘𝐵) = (abs‘((1st ‘(𝐹‘𝐵)) − (2nd ‘(𝐹‘𝐵))))) | ||
| Theorem | fcomptss 42750* | Express composition of two functions as a maps-to applying both in sequence. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ (𝐺‘(𝐹‘𝑥)))) | ||
| Theorem | elmapsnd 42751 | Membership in a set exponentiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐹 Fn {𝐴}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m {𝐴})) | ||
| Theorem | mapss2 42752 | Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) & ⊢ (𝜑 → 𝐶 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶))) | ||
| Theorem | fsneq 42753 | Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝐵 = {𝐴} & ⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → 𝐺 Fn 𝐵) ⇒ ⊢ (𝜑 → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) = (𝐺‘𝐴))) | ||
| Theorem | difmap 42754 | Difference of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) & ⊢ (𝜑 → 𝐶 ≠ ∅) ⇒ ⊢ (𝜑 → ((𝐴 ∖ 𝐵) ↑m 𝐶) ⊆ ((𝐴 ↑m 𝐶) ∖ (𝐵 ↑m 𝐶))) | ||
| Theorem | unirnmap 42755 | Given a subset of a set exponentiation, the base set can be restricted. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑m 𝐴)) ⇒ ⊢ (𝜑 → 𝑋 ⊆ (ran ∪ 𝑋 ↑m 𝐴)) | ||
| Theorem | inmap 42756 | Intersection of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) ⇒ ⊢ (𝜑 → ((𝐴 ↑m 𝐶) ∩ (𝐵 ↑m 𝐶)) = ((𝐴 ∩ 𝐵) ↑m 𝐶)) | ||
| Theorem | fcoss 42757 | Composition of two mappings. Similar to fco 6633, but with a weaker condition on the domain of 𝐹. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐺:𝐷⟶𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐷⟶𝐵) | ||
| Theorem | fsneqrn 42758 | Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝐵 = {𝐴} & ⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → 𝐺 Fn 𝐵) ⇒ ⊢ (𝜑 → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) ∈ ran 𝐺)) | ||
| Theorem | difmapsn 42759 | Difference of two sets exponentiatiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) ⇒ ⊢ (𝜑 → ((𝐴 ↑m {𝐶}) ∖ (𝐵 ↑m {𝐶})) = ((𝐴 ∖ 𝐵) ↑m {𝐶})) | ||
| Theorem | mapssbi 42760 | Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) & ⊢ (𝜑 → 𝐶 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶))) | ||
| Theorem | unirnmapsn 42761 | Equality theorem for a subset of a set exponentiation, where the exponent is a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝐶 = {𝐴} & ⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑m 𝐶)) ⇒ ⊢ (𝜑 → 𝑋 = (ran ∪ 𝑋 ↑m 𝐶)) | ||
| Theorem | iunmapss 42762* | The indexed union of set exponentiations is a subset of the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 ↑m 𝐶) ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐶)) | ||
| Theorem | ssmapsn 42763* | A subset 𝐶 of a set exponentiation to a singleton, is its projection 𝐷 exponentiated to the singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ Ⅎ𝑓𝐷 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ (𝐵 ↑m {𝐴})) & ⊢ 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓 ⇒ ⊢ (𝜑 → 𝐶 = (𝐷 ↑m {𝐴})) | ||
| Theorem | iunmapsn 42764* | The indexed union of set exponentiations to a singleton is equal to the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 ↑m {𝐶}) = (∪ 𝑥 ∈ 𝐴 𝐵 ↑m {𝐶})) | ||
| Theorem | absfico 42765 | Mapping domain and codomain of the absolute value function. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ abs:ℂ⟶(0[,)+∞) | ||
| Theorem | icof 42766 | The set of left-closed right-open intervals of extended reals maps to subsets of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ [,):(ℝ* × ℝ*)⟶𝒫 ℝ* | ||
| Theorem | elpmrn 42767 | The range of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → ran 𝐹 ⊆ 𝐴) | ||
| Theorem | imaexi 42768 | The image of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ (𝐴 “ 𝐵) ∈ V | ||
| Theorem | axccdom 42769* | Relax the constraint on ax-cc to dominance instead of equinumerosity. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝑋 ≼ ω) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧 ∈ 𝑋 (𝑓‘𝑧) ∈ 𝑧)) | ||
| Theorem | dmmptdf 42770* | The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 = 𝐵) | ||
| Theorem | elpmi2 42771 | The domain of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → dom 𝐹 ⊆ 𝐵) | ||
| Theorem | dmrelrnrel 42772* | A relation preserving function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → (𝐹‘𝐵)𝑆(𝐹‘𝐶)) | ||
| Theorem | fvcod 42773 | Value of a function composition. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝐴 ∈ dom 𝐺) & ⊢ 𝐻 = (𝐹 ∘ 𝐺) ⇒ ⊢ (𝜑 → (𝐻‘𝐴) = (𝐹‘(𝐺‘𝐴))) | ||
| Theorem | elrnmpoid 42774* | Membership in the range of an operation class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) ∈ ran 𝐹) | ||
| Theorem | axccd 42775* | An alternative version of the axiom of countable choice. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝐴 ≈ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥) | ||
| Theorem | axccd2 42776* | An alternative version of the axiom of countable choice. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝐴 ≼ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥) | ||
| Theorem | funimassd 42777* | Sufficient condition for the image of a function being a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Fun 𝐹) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 “ 𝐴) ⊆ 𝐵) | ||
| Theorem | fimassd 42778 | The image of a class is a subset of its codomain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝐹 “ 𝑋) ⊆ 𝐵) | ||
| Theorem | feqresmptf 42779* | Express a restricted function as a mapping. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) | ||
| Theorem | elrnmpt1d 42780 | Elementhood in an image set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐵 ∈ ran 𝐹) | ||
| Theorem | dmresss 42781 | The domain of a restriction is a subset of the original domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ dom (𝐴 ↾ 𝐵) ⊆ dom 𝐴 | ||
| Theorem | dmmptssf 42782 | The domain of a mapping is a subset of its base class. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
| Theorem | dmmptdf2 42783 | The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐵 & ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 = 𝐵) | ||
| Theorem | dmuz 42784 | Domain of the upper integers function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ dom ℤ≥ = ℤ | ||
| Theorem | fmptd2f 42785* | Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) | ||
| Theorem | mpteq1df 42786 | An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof shortened by SN, 11-Nov-2024.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
| Theorem | mpteq1dfOLD 42787 | Obsolete version of mpteq1df 42786 as of 11-Nov-2024. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
| Theorem | mptexf 42788 | If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 7106. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V | ||
| Theorem | fvmpt4 42789* | Value of a function given by the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) | ||
| Theorem | fmptf 42790* | Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝐵 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) | ||
| Theorem | resimass 42791 | The image of a restriction is a subset of the original image. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ ((𝐴 ↾ 𝐵) “ 𝐶) ⊆ (𝐴 “ 𝐶) | ||
| Theorem | mptssid 42792 | The mapping operation expressed with its actual domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐵) | ||
| Theorem | mptfnd 42793 | The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.) (Revised by Thierry Arnoux, 10-May-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) | ||
| Theorem | mpteq12daOLD 42794 | Obsolete version of mpteq12da 5160 as of 11-Nov-2024. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
| Theorem | rnmptlb 42795* | Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) | ||
| Theorem | rnmptbddlem 42796* | Boundness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) | ||
| Theorem | rnmptbdd 42797* | Boundness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) | ||
| Theorem | mptima2 42798* | Image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ 𝐶 ↦ 𝐵)) | ||
| Theorem | funimaeq 42799* | Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝐴 ⊆ dom 𝐹) & ⊢ (𝜑 → 𝐴 ⊆ dom 𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹 “ 𝐴) = (𝐺 “ 𝐴)) | ||
| Theorem | rnmptssf 42800* | The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |