![]() |
Metamath
Proof Explorer Theorem List (p. 471 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fsetsnf1 47001* | The mapping of an element of a class to a singleton function is an injection. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {〈𝑆, 𝑏〉}} & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {〈𝑆, 𝑥〉}) ⇒ ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵–1-1→𝐴) | ||
Theorem | fsetsnfo 47002* | The mapping of an element of a class to a singleton function is a surjection. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {〈𝑆, 𝑏〉}} & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {〈𝑆, 𝑥〉}) ⇒ ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵–onto→𝐴) | ||
Theorem | fsetsnf1o 47003* | The mapping of an element of a class to a singleton function is a bijection. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {〈𝑆, 𝑏〉}} & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {〈𝑆, 𝑥〉}) ⇒ ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵–1-1-onto→𝐴) | ||
Theorem | fsetsnprcnex 47004* | The class of all functions from a (proper) singleton into a proper class 𝐵 is not a set. (Contributed by AV, 13-Sep-2024.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∉ V) → {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} ∉ V) | ||
Theorem | cfsetssfset 47005 | The class of constant functions is a subclass of the class of functions. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} ⇒ ⊢ 𝐹 ⊆ {𝑓 ∣ 𝑓:𝐴⟶𝐵} | ||
Theorem | cfsetsnfsetfv 47006* | The function value of the mapping of the class of singleton functions into the class of constant functions. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} & ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵} & ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺) → (𝐻‘𝑋) = (𝑎 ∈ 𝐴 ↦ (𝑋‘𝑌))) | ||
Theorem | cfsetsnfsetf 47007* | The mapping of the class of singleton functions into the class of constant functions is a function. (Contributed by AV, 14-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} & ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵} & ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺⟶𝐹) | ||
Theorem | cfsetsnfsetf1 47008* | The mapping of the class of singleton functions into the class of constant functions is an injection. (Contributed by AV, 14-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} & ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵} & ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺–1-1→𝐹) | ||
Theorem | cfsetsnfsetfo 47009* | The mapping of the class of singleton functions into the class of constant functions is a surjection. (Contributed by AV, 14-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} & ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵} & ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺–onto→𝐹) | ||
Theorem | cfsetsnfsetf1o 47010* | The mapping of the class of singleton functions into the class of constant functions is a bijection. (Contributed by AV, 14-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} & ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵} & ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺–1-1-onto→𝐹) | ||
Theorem | fsetprcnexALT 47011* | First version of proof for fsetprcnex 8900, which was much more complicated. (Contributed by AV, 14-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∉ V) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∉ V) | ||
Theorem | fcoreslem1 47012 | Lemma 1 for fcores 47016. (Contributed by AV, 17-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) ⇒ ⊢ (𝜑 → 𝑃 = (◡𝐹 “ 𝐸)) | ||
Theorem | fcoreslem2 47013 | Lemma 2 for fcores 47016. (Contributed by AV, 17-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) ⇒ ⊢ (𝜑 → ran 𝑋 = 𝐸) | ||
Theorem | fcoreslem3 47014 | Lemma 3 for fcores 47016. (Contributed by AV, 13-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) ⇒ ⊢ (𝜑 → 𝑋:𝑃–onto→𝐸) | ||
Theorem | fcoreslem4 47015 | Lemma 4 for fcores 47016. (Contributed by AV, 17-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) ⇒ ⊢ (𝜑 → (𝑌 ∘ 𝑋) Fn 𝑃) | ||
Theorem | fcores 47016 | Every composite function (𝐺 ∘ 𝐹) can be written as composition of restrictions of the composed functions (to their minimum domains). (Contributed by GL and AV, 17-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑌 ∘ 𝑋)) | ||
Theorem | fcoresf1lem 47017 | Lemma for fcoresf1 47018. (Contributed by AV, 18-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) ⇒ ⊢ ((𝜑 ∧ 𝑍 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑍) = (𝑌‘(𝑋‘𝑍))) | ||
Theorem | fcoresf1 47018 | If a composition is injective, then the restrictions of its components to the minimum domains are injective. (Contributed by GL and AV, 18-Sep-2024.) (Revised by AV, 7-Oct-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) & ⊢ (𝜑 → (𝐺 ∘ 𝐹):𝑃–1-1→𝐷) ⇒ ⊢ (𝜑 → (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1→𝐷)) | ||
Theorem | fcoresf1b 47019 | A composition is injective iff the restrictions of its components to the minimum domains are injective. (Contributed by GL and AV, 7-Oct-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) ⇒ ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 ↔ (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1→𝐷))) | ||
Theorem | fcoresfo 47020 | If a composition is surjective, then the restriction of its first component to the minimum domain is surjective. (Contributed by AV, 17-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) & ⊢ (𝜑 → (𝐺 ∘ 𝐹):𝑃–onto→𝐷) ⇒ ⊢ (𝜑 → 𝑌:𝐸–onto→𝐷) | ||
Theorem | fcoresfob 47021 | A composition is surjective iff the restriction of its first component to the minimum domain is surjective. (Contributed by GL and AV, 7-Oct-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) ⇒ ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–onto→𝐷 ↔ 𝑌:𝐸–onto→𝐷)) | ||
Theorem | fcoresf1ob 47022 | A composition is bijective iff the restriction of its first component to the minimum domain is bijective and the restriction of its second component to the minimum domain is injective. (Contributed by GL and AV, 7-Oct-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) ⇒ ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1-onto→𝐷 ↔ (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1-onto→𝐷))) | ||
Theorem | f1cof1blem 47023 | Lemma for f1cof1b 47026 and focofob 47029. (Contributed by AV, 18-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) & ⊢ (𝜑 → ran 𝐹 = 𝐶) ⇒ ⊢ (𝜑 → ((𝑃 = 𝐴 ∧ 𝐸 = 𝐶) ∧ (𝑋 = 𝐹 ∧ 𝑌 = 𝐺))) | ||
Theorem | 3f1oss1 47024 | The composition of three bijections as bijection from the image of the domain onto the image of the range of the middle bijection. (Contributed by AV, 15-Aug-2025.) |
⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸)) → ((𝐻 ∘ 𝐺) ∘ ◡𝐹):(𝐹 “ 𝐶)–1-1-onto→(𝐻 “ 𝐷)) | ||
Theorem | 3f1oss2 47025 | The composition of three bijections as bijection from the image of the converse of the domain onto the image of the converse of the range of the middle bijection. (Contributed by AV, 15-Aug-2025.) |
⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐻:𝐸–1-1-onto→𝐼) ∧ (𝐶 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐼)) → ((◡𝐻 ∘ 𝐺) ∘ 𝐹):(◡𝐹 “ 𝐶)–1-1-onto→(◡𝐻 “ 𝐷)) | ||
Theorem | f1cof1b 47026 | If the range of 𝐹 equals the domain of 𝐺, then the composition (𝐺 ∘ 𝐹) is injective iff 𝐹 and 𝐺 are both injective. (Contributed by GL and AV, 19-Sep-2024.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐶⟶𝐷 ∧ ran 𝐹 = 𝐶) → ((𝐺 ∘ 𝐹):𝐴–1-1→𝐷 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷))) | ||
Theorem | funfocofob 47027 | If the domain of a function 𝐺 is a subset of the range of a function 𝐹, then the composition (𝐺 ∘ 𝐹) is surjective iff 𝐺 is surjective. (Contributed by GL and AV, 29-Sep-2024.) |
⊢ ((Fun 𝐹 ∧ 𝐺:𝐴⟶𝐵 ∧ 𝐴 ⊆ ran 𝐹) → ((𝐺 ∘ 𝐹):(◡𝐹 “ 𝐴)–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵)) | ||
Theorem | fnfocofob 47028 | If the domain of a function 𝐺 equals the range of a function 𝐹, then the composition (𝐺 ∘ 𝐹) is surjective iff 𝐺 is surjective. (Contributed by GL and AV, 29-Sep-2024.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺:𝐵⟶𝐶 ∧ ran 𝐹 = 𝐵) → ((𝐺 ∘ 𝐹):𝐴–onto→𝐶 ↔ 𝐺:𝐵–onto→𝐶)) | ||
Theorem | focofob 47029 | If the domain of a function 𝐺 equals the range of a function 𝐹, then the composition (𝐺 ∘ 𝐹) is surjective iff 𝐺 and 𝐹 as function to the domain of 𝐺 are both surjective. Symmetric version of fnfocofob 47028 including the fact that 𝐹 is a surjection onto its range. (Contributed by GL and AV, 20-Sep-2024.) (Proof shortened by AV, 29-Sep-2024.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐶⟶𝐷 ∧ ran 𝐹 = 𝐶) → ((𝐺 ∘ 𝐹):𝐴–onto→𝐷 ↔ (𝐹:𝐴–onto→𝐶 ∧ 𝐺:𝐶–onto→𝐷))) | ||
Theorem | f1ocof1ob 47030 | If the range of 𝐹 equals the domain of 𝐺, then the composition (𝐺 ∘ 𝐹) is bijective iff 𝐹 and 𝐺 are both bijective. (Contributed by GL and AV, 7-Oct-2024.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐶⟶𝐷 ∧ ran 𝐹 = 𝐶) → ((𝐺 ∘ 𝐹):𝐴–1-1-onto→𝐷 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐺:𝐶–1-1-onto→𝐷))) | ||
Theorem | f1ocof1ob2 47031 | If the range of 𝐹 equals the domain of 𝐺, then the composition (𝐺 ∘ 𝐹) is bijective iff 𝐹 and 𝐺 are both bijective. Symmetric version of f1ocof1ob 47030 including the fact that 𝐹 is a surjection onto its range. (Contributed by GL and AV, 20-Sep-2024.) (Proof shortened by AV, 7-Oct-2024.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐶⟶𝐷 ∧ ran 𝐹 = 𝐶) → ((𝐺 ∘ 𝐹):𝐴–1-1-onto→𝐷 ↔ (𝐹:𝐴–1-1-onto→𝐶 ∧ 𝐺:𝐶–1-1-onto→𝐷))) | ||
Syntax | caiota 47032 | Extend class notation with an alternative for Russell's definition of a description binder (inverted iota). |
class (℩'𝑥𝜑) | ||
Theorem | aiotajust 47033* | Soundness justification theorem for df-aiota 47034. (Contributed by AV, 24-Aug-2022.) |
⊢ ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∩ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} | ||
Definition | df-aiota 47034* |
Alternate version of Russell's definition of a description binder, which
can be read as "the unique 𝑥 such that 𝜑", where 𝜑
ordinarily contains 𝑥 as a free variable. Our definition
is
meaningful only when there is exactly one 𝑥 such that 𝜑 is true
(see aiotaval 47044); otherwise, it is not a set (see aiotaexb 47038), or even
more concrete, it is the universe V (see aiotavb 47039). Since this
is an alternative for df-iota 6515, we call this symbol ℩'
alternate iota in the following.
The advantage of this definition is the clear distinguishability of the defined and undefined cases: the alternate iota over a wff is defined iff it is a set (see aiotaexb 47038). With the original definition, there is no corresponding theorem (∃!𝑥𝜑 ↔ (℩𝑥𝜑) ≠ ∅), because ∅ can be a valid unique set satisfying a wff (see, for example, iota0def 46987). Only the right to left implication would hold, see (negated) iotanul 6540. For defined cases, however, both definitions df-iota 6515 and df-aiota 47034 are equivalent, see reuaiotaiota 47037. (Proposed by BJ, 13-Aug-2022.) (Contributed by AV, 24-Aug-2022.) |
⊢ (℩'𝑥𝜑) = ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} | ||
Theorem | dfaiota2 47035* | Alternate definition of the alternate version of Russell's definition of a description binder. Definition 8.18 in [Quine] p. 56. (Contributed by AV, 24-Aug-2022.) |
⊢ (℩'𝑥𝜑) = ∩ {𝑦 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)} | ||
Theorem | reuabaiotaiota 47036* | The iota and the alternate iota over a wff 𝜑 are equal iff there is a unique satisfying value of {𝑥 ∣ 𝜑} = {𝑦}. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑦{𝑥 ∣ 𝜑} = {𝑦} ↔ (℩𝑥𝜑) = (℩'𝑥𝜑)) | ||
Theorem | reuaiotaiota 47037 | The iota and the alternate iota over a wff 𝜑 are equal iff there is a unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑥𝜑 ↔ (℩𝑥𝜑) = (℩'𝑥𝜑)) | ||
Theorem | aiotaexb 47038 | The alternate iota over a wff 𝜑 is a set iff there is a unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑥𝜑 ↔ (℩'𝑥𝜑) ∈ V) | ||
Theorem | aiotavb 47039 | The alternate iota over a wff 𝜑 is the universe iff there is no unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.) |
⊢ (¬ ∃!𝑥𝜑 ↔ (℩'𝑥𝜑) = V) | ||
Theorem | aiotaint 47040 | This is to df-aiota 47034 what iotauni 6537 is to df-iota 6515 (it uses intersection like df-aiota 47034, similar to iotauni 6537 using union like df-iota 6515; we could also prove an analogous result using union here too, in the same way that we have iotaint 6538). (Contributed by BJ, 31-Aug-2024.) |
⊢ (∃!𝑥𝜑 → (℩'𝑥𝜑) = ∩ {𝑥 ∣ 𝜑}) | ||
Theorem | dfaiota3 47041 | Alternate definition of ℩': this is to df-aiota 47034 what dfiota4 6554 is to df-iota 6515. operation using the if operator. It is simpler than df-aiota 47034 and uses no dummy variables, so it would be the preferred definition if ℩' becomes the description binder used in set.mm. (Contributed by BJ, 31-Aug-2024.) |
⊢ (℩'𝑥𝜑) = if(∃!𝑥𝜑, ∩ {𝑥 ∣ 𝜑}, V) | ||
Theorem | iotan0aiotaex 47042 | If the iota over a wff 𝜑 is not empty, the alternate iota over 𝜑 is a set. (Contributed by AV, 25-Aug-2022.) |
⊢ ((℩𝑥𝜑) ≠ ∅ → (℩'𝑥𝜑) ∈ V) | ||
Theorem | aiotaexaiotaiota 47043 | The alternate iota over a wff 𝜑 is a set iff the iota and the alternate iota over 𝜑 are equal. (Contributed by AV, 25-Aug-2022.) |
⊢ ((℩'𝑥𝜑) ∈ V ↔ (℩𝑥𝜑) = (℩'𝑥𝜑)) | ||
Theorem | aiotaval 47044* | Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of (alternate) iota. (Contributed by AV, 24-Aug-2022.) |
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩'𝑥𝜑) = 𝑦) | ||
Theorem | aiota0def 47045* | Example for a defined alternate iota being the empty set, i.e., ∀𝑦𝑥 ⊆ 𝑦 is a wff satisfied by a unique value 𝑥, namely 𝑥 = ∅ (the empty set is the one and only set which is a subset of every set). This corresponds to iota0def 46987. (Contributed by AV, 25-Aug-2022.) |
⊢ (℩'𝑥∀𝑦 𝑥 ⊆ 𝑦) = ∅ | ||
Theorem | aiota0ndef 47046* | Example for an undefined alternate iota being no set, i.e., ∀𝑦𝑦 ∈ 𝑥 is a wff not satisfied by a (unique) value 𝑥 (there is no set, and therefore certainly no unique set, which contains every set). This is different from iota0ndef 46988, where the iota still is a set (the empty set). (Contributed by AV, 25-Aug-2022.) |
⊢ (℩'𝑥∀𝑦 𝑦 ∈ 𝑥) ∉ V | ||
Theorem | r19.32 47047 | Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers, analogous to r19.32v 3189. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | rexsb 47048* | An equivalent expression for restricted existence, analogous to exsb 2359. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | rexrsb 47049* | An equivalent expression for restricted existence, analogous to exsb 2359. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 = 𝑦 → 𝜑)) | ||
Theorem | 2rexsb 47050* | An equivalent expression for double restricted existence, analogous to rexsb 47048. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) | ||
Theorem | 2rexrsb 47051* | An equivalent expression for double restricted existence, analogous to 2exsb 2360. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) | ||
Theorem | cbvral2 47052* | Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvral2v 3365. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑤𝜒 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvrex2 47053* | Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvrex2v 3366. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑤𝜒 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) | ||
Theorem | ralndv1 47054 | Example for a theorem about a restricted universal quantification in which the restricting class depends on (actually is) the bound variable: All sets containing themselves contain the universal class. (Contributed by AV, 24-Jun-2023.) |
⊢ ∀𝑥 ∈ 𝑥 V ∈ 𝑥 | ||
Theorem | ralndv2 47055 | Second example for a theorem about a restricted universal quantification in which the restricting class depends on the bound variable: all subsets of a set are sets. (Contributed by AV, 24-Jun-2023.) |
⊢ ∀𝑥 ∈ 𝒫 𝑥𝑥 ∈ V | ||
Theorem | reuf1odnf 47056* | There is exactly one element in each of two isomorphic sets. Variant of reuf1od 47057 with no distinct variable condition for 𝜒. (Contributed by AV, 19-Mar-2023.) |
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐵) & ⊢ ((𝜑 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑧 → (𝜓 ↔ 𝜃)) & ⊢ Ⅎ𝑥𝜒 ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | reuf1od 47057* | There is exactly one element in each of two isomorphic sets. (Contributed by AV, 19-Mar-2023.) |
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐵) & ⊢ ((𝜑 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐵 𝜓 ↔ ∃!𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | euoreqb 47058* | There is a set which is equal to one of two other sets iff the other sets are equal. (Contributed by AV, 24-Jan-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∃!𝑥 ∈ 𝑉 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | 2reu3 47059* | Double restricted existential uniqueness, analogous to 2eu3 2651. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∃*𝑥 ∈ 𝐴 𝜑 ∨ ∃*𝑦 ∈ 𝐵 𝜑) → ((∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝜑) ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))) | ||
Theorem | 2reu7 47060* | Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 2655. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑)) | ||
Theorem | 2reu8 47061* | Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2656. Curiously, we can put ∃! on either of the internal conjuncts but not both. We can also commute ∃!𝑥 ∈ 𝐴∃!𝑦 ∈ 𝐵 using 2reu7 47060. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑) ↔ ∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 (∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜑)) | ||
Theorem | 2reu8i 47062* | Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, see also 2reu8 47061. The involved wffs depend on the setvar variables as follows: ph(x,y), ta(v,y), ch(x,w), th(v,w), et(x,b), ps(a,b), ze(a,w). (Contributed by AV, 1-Apr-2023.) |
⊢ (𝑥 = 𝑣 → (𝜑 ↔ 𝜏)) & ⊢ (𝑥 = 𝑣 → (𝜒 ↔ 𝜃)) & ⊢ (𝑦 = 𝑤 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑏 → (𝜑 ↔ 𝜂)) & ⊢ (𝑥 = 𝑎 → (𝜒 ↔ 𝜁)) & ⊢ (((𝜒 → 𝑦 = 𝑤) ∧ 𝜁) → 𝑦 = 𝑤) & ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜂 → (𝑏 = 𝑦 ∧ (𝜓 → 𝑎 = 𝑥))))) | ||
Theorem | 2reuimp0 47063* | Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification. The involved wffs depend on the setvar variables as follows: ph(a,b), th(a,c), ch(d,b), ta(d,c), et(a,e), ps(a,f) (Contributed by AV, 13-Mar-2023.) |
⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜃)) & ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒)) & ⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏)) & ⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂)) & ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓)) ⇒ ⊢ (∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑 → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓))) | ||
Theorem | 2reuimp 47064* | Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification if the class of the quantified elements is not empty. (Contributed by AV, 13-Mar-2023.) |
⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜃)) & ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒)) & ⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏)) & ⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂)) & ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓)) ⇒ ⊢ ((𝑉 ≠ ∅ ∧ ∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑) → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ((𝜒 ∧ (𝜏 → 𝑏 = 𝑐)) → (𝜓 → (𝜂 ∧ (𝑎 = 𝑑 ∧ 𝑒 = 𝑓))))) | ||
The current definition of the value (𝐹‘𝐴) of a function 𝐹 at an argument 𝐴 (see df-fv 6570) assures that this value is always a set, see fex 7245. This is because this definition can be applied to any classes 𝐹 and 𝐴, and evaluates to the empty set when it is not meaningful (as shown by ndmfv 6941 and fvprc 6898). Although it is very convenient for many theorems on functions and their proofs, there are some cases in which from (𝐹‘𝐴) = ∅ alone it cannot be decided/derived whether (𝐹‘𝐴) is meaningful (𝐹 is actually a function which is defined for 𝐴 and really has the function value ∅ at 𝐴) or not. Therefore, additional assumptions are required, such as ∅ ∉ ran 𝐹, ∅ ∈ ran 𝐹 or Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 (see, for example, ndmfvrcl 6942). To avoid such an ambiguity, an alternative definition (𝐹'''𝐴) (see df-afv 47069) would be possible which evaluates to the universal class ((𝐹'''𝐴) = V) if it is not meaningful (see afvnfundmuv 47088, ndmafv 47089, afvprc 47093 and nfunsnafv 47091), and which corresponds to the current definition ((𝐹‘𝐴) = (𝐹'''𝐴)) if it is (see afvfundmfveq 47087). That means (𝐹'''𝐴) = V → (𝐹‘𝐴) = ∅ (see afvpcfv0 47095), but (𝐹‘𝐴) = ∅ → (𝐹'''𝐴) = V is not generally valid. In the theory of partial functions, it is a common case that 𝐹 is not defined at 𝐴, which also would result in (𝐹'''𝐴) = V. In this context we say (𝐹'''𝐴) "is not defined" instead of "is not meaningful". With this definition the following intuitive equivalence holds: (𝐹'''𝐴) ∈ V <-> "(𝐹'''𝐴) is meaningful/defined". An interesting question would be if (𝐹‘𝐴) could be replaced by (𝐹'''𝐴) in most of the theorems based on function values. If we look at the (currently 19) proofs using the definition df-fv 6570 of (𝐹‘𝐴), we see that analogues for the following 8 theorems can be proven using the alternative definition: fveq1 6905-> afveq1 47083, fveq2 6906-> afveq2 47084, nffv 6916-> nfafv 47085, csbfv12 6954-> csbafv12g , fvres 6925-> afvres 47121, rlimdm 15583-> rlimdmafv 47126, tz6.12-1 6929-> tz6.12-1-afv 47123, fveu 6895-> afveu 47102. Three theorems proved by directly using df-fv 6570 are within a mathbox (fvsb 44447) or not used (isumclim3 15791, avril1 30491). However, the remaining 8 theorems proved by directly using df-fv 6570 are used more or less often: * fvex 6919: used in about 1750 proofs. * tz6.12-1 6929: root theorem of many theorems which have not a strict analogue, and which are used many times: fvprc 6898 (used in about 127 proofs), tz6.12i 6934 (used - indirectly via fvbr0 6935 and fvrn0 6936- in 18 proofs, and in fvclss 7260 used in fvclex 7981 used in fvresex 7982, which is not used!), dcomex 10484 (used in 4 proofs), ndmfv 6941 (used in 86 proofs) and nfunsn 6948 (used by dffv2 7003 which is not used). * fv2 6901: only used by elfv 6904, which is only used by fv3 6924, which is not used. * dffv3 6902: used by dffv4 6903 (the previous "df-fv"), which now is only used in deprecated (usage discouraged) theorems or within mathboxes (csbfv12gALTVD 44896), by shftval 15109 (itself used in 9 proofs), by dffv5 35905 (mathbox) and by fvco2 7005, which has the analogue afvco2 47125. * fvopab5 7048: used only by ajval 30889 (not used) and by adjval 31918 (used - indirectly - in 9 proofs). * zsum 15750: used (via isum 15751, sum0 15753 and fsumsers 15760) in more than 90 proofs. * isumshft 15871: used in pserdv2 26488 and (via logtayl 26716) 4 other proofs. * ovtpos 8264: used in 14 proofs. As a result of this analysis we can say that the current definition of a function value is crucial for Metamath and cannot be exchanged easily with an alternative definition. While fv2 6901, dffv3 6902, fvopab5 7048, zsum 15750, isumshft 15871 and ovtpos 8264 are not critical or are, hopefully, also valid for the alternative definition, fvex 6919 and tz6.12-1 6929 (and the theorems based on them) are essential for the current definition of function values. With the same arguments, an alternative definition of operation values ((𝐴𝑂𝐵)) could be meaningful to avoid ambiguities, see df-aov 47070. For additional details, see https://groups.google.com/g/metamath/c/cteNUppB6A4 47070. | ||
Syntax | wdfat 47065 | Extend the definition of a wff to include the "defined at" predicate. Read: "(the function) 𝐹 is defined at (the argument) 𝐴". In a previous version, the token "def@" was used. However, since the @ is used (informally) as a replacement for $ in commented out sections that may be deleted some day. While there is no violation of any standard to use the @ in a token, it could make the search for such commented-out sections slightly more difficult. (See remark of Norman Megill at https://groups.google.com/g/metamath/c/cteNUppB6A4). |
wff 𝐹 defAt 𝐴 | ||
Syntax | cafv 47066 | Extend the definition of a class to include the value of a function. Read: "the value of 𝐹 at 𝐴 " or "𝐹 of 𝐴". In a previous version, the symbol " ' " was used. However, since the similarity with the symbol ‘ used for the current definition of a function's value (see df-fv 6570), which, by the way, was intended to visualize that in many cases ‘ and " ' " are exchangeable, makes reading the theorems, especially those which use both definitions as dfafv2 47081, very difficult, 3 apostrophes ''' are used now so that it's easier to distinguish from df-fv 6570 and df-ima 5701. And not three backticks ( three times ‘) since that would be annoying to escape in a comment. (See remark of Norman Megill and Gerard Lang at https://groups.google.com/g/metamath/c/cteNUppB6A4 5701). |
class (𝐹'''𝐴) | ||
Syntax | caov 47067 | Extend class notation to include the value of an operation 𝐹 (such as +) for two arguments 𝐴 and 𝐵. Note that the syntax is simply three class symbols in a row surrounded by a pair of parentheses in contrast to the current definition, see df-ov 7433. |
class ((𝐴𝐹𝐵)) | ||
Definition | df-dfat 47068 | Definition of the predicate that determines if some class 𝐹 is defined as function for an argument 𝐴 or, in other words, if the function value for some class 𝐹 for an argument 𝐴 is defined. We say that 𝐹 is defined at 𝐴 if a 𝐹 is a function restricted to the member 𝐴 of its domain. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))) | ||
Definition | df-afv 47069* | Alternative definition of the value of a function, (𝐹'''𝐴), also known as function application. In contrast to (𝐹‘𝐴) = ∅ (see df-fv 6570 and ndmfv 6941), (𝐹'''𝐴) = V if F is not defined for A! (Contributed by Alexander van der Vekens, 25-May-2017.) (Revised by BJ/AV, 25-Aug-2022.) |
⊢ (𝐹'''𝐴) = (℩'𝑥𝐴𝐹𝑥) | ||
Definition | df-aov 47070 | Define the value of an operation. In contrast to df-ov 7433, the alternative definition for a function value (see df-afv 47069) is used. By this, the value of the operation applied to two arguments is the universal class if the operation is not defined for these two arguments. There are still no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐴𝐹𝐵)) = (𝐹'''〈𝐴, 𝐵〉) | ||
Theorem | ralbinrald 47071* | Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.) |
⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → 𝑥 = 𝑋) & ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ 𝜃)) | ||
Theorem | nvelim 47072 | If a class is the universal class it doesn't belong to any class, generalization of nvel 5321. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝐴 = V → ¬ 𝐴 ∈ 𝐵) | ||
Theorem | alneu 47073 | If a statement holds for all sets, there is not a unique set for which the statement holds. (Contributed by Alexander van der Vekens, 28-Nov-2017.) |
⊢ (∀𝑥𝜑 → ¬ ∃!𝑥𝜑) | ||
Theorem | eu2ndop1stv 47074* | If there is a unique second component in an ordered pair contained in a given set, the first component must be a set. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
⊢ (∃!𝑦〈𝐴, 𝑦〉 ∈ 𝑉 → 𝐴 ∈ V) | ||
Theorem | dfateq12d 47075 | Equality deduction for "defined at". (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 defAt 𝐴 ↔ 𝐺 defAt 𝐵)) | ||
Theorem | nfdfat 47076 | Bound-variable hypothesis builder for "defined at". To prove a deduction version of this theorem is not easily possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of "defined at" is based on are not available (e.g., for Fun/Rel, dom, ⊆, etc.). (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝐹 defAt 𝐴 | ||
Theorem | dfdfat2 47077* | Alternate definition of the predicate "defined at" not using the Fun predicate. (Contributed by Alexander van der Vekens, 22-Jul-2017.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ ∃!𝑦 𝐴𝐹𝑦)) | ||
Theorem | fundmdfat 47078 | A function is defined at any element of its domain. (Contributed by AV, 2-Sep-2022.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → 𝐹 defAt 𝐴) | ||
Theorem | dfatprc 47079 | A function is not defined at a proper class. (Contributed by AV, 1-Sep-2022.) |
⊢ (¬ 𝐴 ∈ V → ¬ 𝐹 defAt 𝐴) | ||
Theorem | dfatelrn 47080 | The value of a function 𝐹 at a set 𝐴 is in the range of the function 𝐹 if 𝐹 is defined at 𝐴. (Contributed by AV, 1-Sep-2022.) |
⊢ (𝐹 defAt 𝐴 → (𝐹‘𝐴) ∈ ran 𝐹) | ||
Theorem | dfafv2 47081 | Alternative definition of (𝐹'''𝐴) using (𝐹‘𝐴) directly. (Contributed by Alexander van der Vekens, 22-Jul-2017.) (Revised by AV, 25-Aug-2022.) |
⊢ (𝐹'''𝐴) = if(𝐹 defAt 𝐴, (𝐹‘𝐴), V) | ||
Theorem | afveq12d 47082 | Equality deduction for function value, analogous to fveq12d 6913. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹'''𝐴) = (𝐺'''𝐵)) | ||
Theorem | afveq1 47083 | Equality theorem for function value, analogous to fveq1 6905. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
⊢ (𝐹 = 𝐺 → (𝐹'''𝐴) = (𝐺'''𝐴)) | ||
Theorem | afveq2 47084 | Equality theorem for function value, analogous to fveq1 6905. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
⊢ (𝐴 = 𝐵 → (𝐹'''𝐴) = (𝐹'''𝐵)) | ||
Theorem | nfafv 47085 | Bound-variable hypothesis builder for function value, analogous to nffv 6916. To prove a deduction version of this analogous to nffvd 6918 is not easily possible because a deduction version of nfdfat 47076 cannot be shown easily. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(𝐹'''𝐴) | ||
Theorem | csbafv12g 47086 | Move class substitution in and out of a function value, analogous to csbfv12 6954, with a direct proof proposed by Mario Carneiro, analogous to csbov123 7474. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐹'''𝐵) = (⦋𝐴 / 𝑥⦌𝐹'''⦋𝐴 / 𝑥⦌𝐵)) | ||
Theorem | afvfundmfveq 47087 | If a class is a function restricted to a member of its domain, then the function value for this member is equal for both definitions. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (𝐹 defAt 𝐴 → (𝐹'''𝐴) = (𝐹‘𝐴)) | ||
Theorem | afvnfundmuv 47088 | If a set is not in the domain of a class or the class is not a function restricted to the set, then the function value for this set is the universe. (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ (¬ 𝐹 defAt 𝐴 → (𝐹'''𝐴) = V) | ||
Theorem | ndmafv 47089 | The value of a class outside its domain is the universe, compare with ndmfv 6941. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹'''𝐴) = V) | ||
Theorem | afvvdm 47090 | If the function value of a class for an argument is a set, the argument is contained in the domain of the class. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) ∈ 𝐵 → 𝐴 ∈ dom 𝐹) | ||
Theorem | nfunsnafv 47091 | If the restriction of a class to a singleton is not a function, its value is the universe, compare with nfunsn 6948. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ Fun (𝐹 ↾ {𝐴}) → (𝐹'''𝐴) = V) | ||
Theorem | afvvfunressn 47092 | If the function value of a class for an argument is a set, the class restricted to the singleton of the argument is a function. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) ∈ 𝐵 → Fun (𝐹 ↾ {𝐴})) | ||
Theorem | afvprc 47093 | A function's value at a proper class is the universe, compare with fvprc 6898. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (¬ 𝐴 ∈ V → (𝐹'''𝐴) = V) | ||
Theorem | afvvv 47094 | If a function's value at an argument is a set, the argument is also a set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) ∈ 𝐵 → 𝐴 ∈ V) | ||
Theorem | afvpcfv0 47095 | If the value of the alternative function at an argument is the universe, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) = V → (𝐹‘𝐴) = ∅) | ||
Theorem | afvnufveq 47096 | The value of the alternative function at a set as argument equals the function's value at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) ≠ V → (𝐹'''𝐴) = (𝐹‘𝐴)) | ||
Theorem | afvvfveq 47097 | The value of the alternative function at a set as argument equals the function's value at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) ∈ 𝐵 → (𝐹'''𝐴) = (𝐹‘𝐴)) | ||
Theorem | afv0fv0 47098 | If the value of the alternative function at an argument is the empty set, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹'''𝐴) = ∅ → (𝐹‘𝐴) = ∅) | ||
Theorem | afvfvn0fveq 47099 | If the function's value at an argument is not the empty set, it equals the value of the alternative function at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ ((𝐹‘𝐴) ≠ ∅ → (𝐹'''𝐴) = (𝐹‘𝐴)) | ||
Theorem | afv0nbfvbi 47100 | The function's value at an argument is an element of a set if and only if the value of the alternative function at this argument is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
⊢ (∅ ∉ 𝐵 → ((𝐹'''𝐴) ∈ 𝐵 ↔ (𝐹‘𝐴) ∈ 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |