![]() |
Metamath
Proof Explorer Theorem List (p. 474 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 | setsnidel 47301 | The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝑅 = (𝑆 sSet 〈𝐴, 𝐵〉) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ 𝑅) | ||
Theorem | setsv 47302 | 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 6259) for theorems about preimages (sometimes, also "imacnv" is used as in fvimacnvi 7071), and "preimafv" (as in preimafvn0 47304) 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 47309): 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)}). 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 47333) by constructing a surjective function 𝑔:𝐴–onto→𝑃 and an injective function ℎ:𝑃–1-1→𝐵 so that 𝐹 = (ℎ ∘ 𝑔) ( see fundcmpsurinjpreimafv 47332). See also Wikipedia ("Surjective function", 17-Mar-2024, https://en.wikipedia.org/wiki/Surjective_function 47332 (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 47335), see also Wikipedia ("Bijection, injection and surjection", 17-Mar-2024, https://en.wikipedia.org/wiki/Bijection,_injection_and_surjection 47335 (section "Properties"). Finally, it is shown that every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective, a bijective and an injective function (see fundcmpsurbijinj 47334), 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 47330). 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 47333, and 𝐹 = (𝐼 ∘ 𝑂) with 𝑂 = (𝐵 ∘ 𝑆) (a surjective function) is a decomposition into a surjective and an injective function corresponding to fundcmpsurinjimaid 47335. | ||
Theorem | preimafvsnel 47303 | The preimage of a function value at 𝑋 contains 𝑋. (Contributed by AV, 7-Mar-2024.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ (◡𝐹 “ {(𝐹‘𝑋)})) | ||
Theorem | preimafvn0 47304 | The preimage of a function value is not empty. (Contributed by AV, 7-Mar-2024.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (◡𝐹 “ {(𝐹‘𝑋)}) ≠ ∅) | ||
Theorem | uniimafveqt 47305* | 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 47306 | 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 47307* | The class 𝑃 of all preimages of function values is a set. (Contributed by AV, 10-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝑃 ∈ V) | ||
Theorem | elsetpreimafvb 47308* | The characterization of an element of the class 𝑃 of all preimages of function values. (Contributed by AV, 10-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ 𝑃 ↔ ∃𝑥 ∈ 𝐴 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)}))) | ||
Theorem | elsetpreimafv 47309* | An element of the class 𝑃 of all preimages of function values. (Contributed by AV, 8-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ (𝑆 ∈ 𝑃 → ∃𝑥 ∈ 𝐴 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)})) | ||
Theorem | elsetpreimafvssdm 47310* | 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 47311* | 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 47312* | 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 47313* | 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 47314* | 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 47315* | 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 47316* | The elements of the preimage of a function value have the same function values. (Contributed by AV, 5-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ (𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝐹‘𝑋) = (𝐹‘𝑌)) | ||
Theorem | eqfvelsetpreimafv 47317* | 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 47318* | An element of the preimage of a function value expressed as a restricted class abstraction. (Contributed by AV, 9-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆) → 𝑆 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = (𝐹‘𝑋)}) | ||
Theorem | imaelsetpreimafv 47319* | 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 47320* | 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 47321* | 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 47322* | Lemma 1 for fundcmpsurinj 47333. (Contributed by AV, 4-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (◡𝐹 “ {(𝐹‘𝑥)})) ⇒ ⊢ ran 𝐺 = 𝑃 | ||
Theorem | fundcmpsurinjlem2 47323* | Lemma 2 for fundcmpsurinj 47333. (Contributed by AV, 4-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (◡𝐹 “ {(𝐹‘𝑥)})) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐺:𝐴–onto→𝑃) | ||
Theorem | fundcmpsurinjlem3 47324* | Lemma 3 for fundcmpsurinj 47333. (Contributed by AV, 3-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ ((Fun 𝐹 ∧ 𝑋 ∈ 𝑃) → (𝐻‘𝑋) = ∪ (𝐹 “ 𝑋)) | ||
Theorem | imasetpreimafvbijlemf 47325* | Lemma for imasetpreimafvbij 47330: the mapping 𝐻 is a function into the range of function 𝐹. (Contributed by AV, 22-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ (𝐹 Fn 𝐴 → 𝐻:𝑃⟶(𝐹 “ 𝐴)) | ||
Theorem | imasetpreimafvbijlemfv 47326* | Lemma for imasetpreimafvbij 47330: the value of the mapping 𝐻 at a preimage of a value of function 𝐹. (Contributed by AV, 5-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌) → (𝐻‘𝑌) = (𝐹‘𝑋)) | ||
Theorem | imasetpreimafvbijlemfv1 47327* | Lemma for imasetpreimafvbij 47330: 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 47328* | Lemma for imasetpreimafvbij 47330: 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 47329* | Lemma for imasetpreimafvbij 47330: the mapping 𝐻 is a function onto the range of function 𝐹. (Contributed by AV, 22-Mar-2024.) |
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} & ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐻:𝑃–onto→(𝐹 “ 𝐴)) | ||
Theorem | imasetpreimafvbij 47330* | 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 47331* | 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 47332* | 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 47333* | Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective and an injective function. (Contributed by AV, 13-Mar-2024.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → ∃𝑔∃ℎ∃𝑝(𝑔:𝐴–onto→𝑝 ∧ ℎ:𝑝–1-1→𝐵 ∧ 𝐹 = (ℎ ∘ 𝑔))) | ||
Theorem | fundcmpsurbijinj 47334* | 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 47335* | 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 47336* | Alternate proof of fundcmpsurinj 47333, based on fundcmpsurinjimaid 47335: 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 47337 | Extend class notation with the partitions of a closed interval of extended reals. |
class RePart | ||
Definition | df-iccp 47338* | 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 47339* | Partition consisting of a fixed number 𝑀 of parts. (Contributed by AV, 9-Jul-2020.) |
⊢ (𝑀 ∈ ℕ → (RePart‘𝑀) = {𝑝 ∈ (ℝ* ↑m (0...𝑀)) ∣ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))}) | ||
Theorem | iccpart 47340* | A special partition. Corresponds to fourierdlem2 46064 in GS's mathbox. (Contributed by AV, 9-Jul-2020.) |
⊢ (𝑀 ∈ ℕ → (𝑃 ∈ (RePart‘𝑀) ↔ (𝑃 ∈ (ℝ* ↑m (0...𝑀)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑃‘𝑖) < (𝑃‘(𝑖 + 1))))) | ||
Theorem | iccpartimp 47341 | Implications for a class being a partition. (Contributed by AV, 11-Jul-2020.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑃 ∈ (RePart‘𝑀) ∧ 𝐼 ∈ (0..^𝑀)) → (𝑃 ∈ (ℝ* ↑m (0...𝑀)) ∧ (𝑃‘𝐼) < (𝑃‘(𝐼 + 1)))) | ||
Theorem | iccpartres 47342 | The restriction of a partition is a partition. (Contributed by AV, 16-Jul-2020.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑃 ∈ (RePart‘(𝑀 + 1))) → (𝑃 ↾ (0...𝑀)) ∈ (RePart‘𝑀)) | ||
Theorem | iccpartxr 47343 | 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 47344 | 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)) < (𝑃‘𝐼)) | ||
Theorem | iccpartipre 47345 | If there is a partition, then all intermediate points are real numbers. (Contributed by AV, 11-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝐼 ∈ (1..^𝑀)) ⇒ ⊢ (𝜑 → (𝑃‘𝐼) ∈ ℝ) | ||
Theorem | iccpartiltu 47346* | If there is a partition, then all intermediate points are strictly less than the upper bound. (Contributed by AV, 12-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (1..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀)) | ||
Theorem | iccpartigtl 47347* | If there is a partition, then all intermediate points are strictly greater than the lower bound. (Contributed by AV, 12-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (1..^𝑀)(𝑃‘0) < (𝑃‘𝑖)) | ||
Theorem | iccpartlt 47348 | If there is a partition, then the lower bound is strictly less than the upper bound. Corresponds to fourierdlem11 46073 in GS's mathbox. (Contributed by AV, 12-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → (𝑃‘0) < (𝑃‘𝑀)) | ||
Theorem | iccpartltu 47349* | If there is a partition, then all intermediate points and the lower bound are strictly less than the upper bound. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀)) | ||
Theorem | iccpartgtl 47350* | If there is a partition, then all intermediate points and the upper bound are strictly greater than the lower bound. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)(𝑃‘0) < (𝑃‘𝑖)) | ||
Theorem | iccpartgt 47351* | If there is a partition, then all intermediate points and the bounds are strictly ordered. (Contributed by AV, 18-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)∀𝑗 ∈ (0...𝑀)(𝑖 < 𝑗 → (𝑃‘𝑖) < (𝑃‘𝑗))) | ||
Theorem | iccpartleu 47352* | If there is a partition, then all intermediate points and the lower and the upper bound are less than or equal to the upper bound. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑃‘𝑖) ≤ (𝑃‘𝑀)) | ||
Theorem | iccpartgel 47353* | If there is a partition, then all intermediate points and the upper and the lower bound are greater than or equal to the lower bound. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑖)) | ||
Theorem | iccpartrn 47354 | If there is a partition, then all intermediate points and bounds are contained in a closed interval of extended reals. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ran 𝑃 ⊆ ((𝑃‘0)[,](𝑃‘𝑀))) | ||
Theorem | iccpartf 47355 | The range of the partition is between its starting point and its ending point. Corresponds to fourierdlem15 46077 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → 𝑃:(0...𝑀)⟶((𝑃‘0)[,](𝑃‘𝑀))) | ||
Theorem | iccpartel 47356 | If there is a partition, then all intermediate points and bounds are contained in a closed interval of extended reals. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝐼 ∈ (0...𝑀)) → (𝑃‘𝐼) ∈ ((𝑃‘0)[,](𝑃‘𝑀))) | ||
Theorem | iccelpart 47357* | An element of any partitioned half-open interval of extended reals is an element of a part of this partition. (Contributed by AV, 18-Jul-2020.) |
⊢ (𝑀 ∈ ℕ → ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) | ||
Theorem | iccpartiun 47358* | A half-open interval of extended reals is the union of the parts of its partition. (Contributed by AV, 18-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ((𝑃‘0)[,)(𝑃‘𝑀)) = ∪ 𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) | ||
Theorem | icceuelpartlem 47359 | Lemma for icceuelpart 47360. (Contributed by AV, 19-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀)) → (𝐼 < 𝐽 → (𝑃‘(𝐼 + 1)) ≤ (𝑃‘𝐽)))) | ||
Theorem | icceuelpart 47360* | An element of a partitioned half-open interval of extended reals is an element of exactly one part of the partition. (Contributed by AV, 19-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ ((𝑃‘0)[,)(𝑃‘𝑀))) → ∃!𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) | ||
Theorem | iccpartdisj 47361* | The segments of a partitioned half-open interval of extended reals are a disjoint collection. (Contributed by AV, 19-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) ⇒ ⊢ (𝜑 → Disj 𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) | ||
Theorem | iccpartnel 47362 | A point of a partition is not an element of any open interval determined by the partition. Corresponds to fourierdlem12 46074 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 8-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑃) ⇒ ⊢ ((𝜑 ∧ 𝐼 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑃‘𝐼)(,)(𝑃‘(𝐼 + 1)))) | ||
Theorem | fargshiftfv 47363* | If a class is a function, then the values of the "shifted function" correspond to the function values of the class. (Contributed by Alexander van der Vekens, 23-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → (𝑋 ∈ (0..^𝑁) → (𝐺‘𝑋) = (𝐹‘(𝑋 + 1)))) | ||
Theorem | fargshiftf 47364* | If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → 𝐺:(0..^(♯‘𝐹))⟶dom 𝐸) | ||
Theorem | fargshiftf1 47365* | If a function is 1-1, then also the shifted function is 1-1. (Contributed by Alexander van der Vekens, 23-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)–1-1→dom 𝐸) → 𝐺:(0..^(♯‘𝐹))–1-1→dom 𝐸) | ||
Theorem | fargshiftfo 47366* | If a function is onto, then also the shifted function is onto. (Contributed by Alexander van der Vekens, 24-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)–onto→dom 𝐸) → 𝐺:(0..^(♯‘𝐹))–onto→dom 𝐸) | ||
Theorem | fargshiftfva 47367* | The values of a shifted function correspond to the value of the original function. (Contributed by Alexander van der Vekens, 24-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → (∀𝑘 ∈ (1...𝑁)(𝐸‘(𝐹‘𝑘)) = ⦋𝑘 / 𝑥⦌𝑃 → ∀𝑙 ∈ (0..^𝑁)(𝐸‘(𝐺‘𝑙)) = ⦋(𝑙 + 1) / 𝑥⦌𝑃)) | ||
Theorem | lswn0 47368 | The last symbol of a not empty word exists. The empty set must be excluded as symbol, because otherwise, it cannot be distinguished between valid cases (∅ is the last symbol) and invalid cases (∅ means that no last symbol exists. This is because of the special definition of a function in set.mm. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∅ ∉ 𝑉 ∧ (♯‘𝑊) ≠ 0) → (lastS‘𝑊) ≠ ∅) | ||
Syntax | wich 47369 | Extend wff notation to include the property of a wff 𝜑 that the setvar variables 𝑥 and 𝑦 are interchangeable. Read this notation as "𝑥 and 𝑦 are interchangeable in wff 𝜑". |
wff [𝑥⇄𝑦]𝜑 | ||
Definition | df-ich 47370* | Define the property of a wff 𝜑 that the setvar variables 𝑥 and 𝑦 are interchangeable. For an alternate definition using implicit substitution and a temporary setvar variable see ichcircshi 47378. Another, equivalent definition using two temporary setvar variables is provided in dfich2 47382. (Contributed by AV, 29-Jul-2023.) |
⊢ ([𝑥⇄𝑦]𝜑 ↔ ∀𝑥∀𝑦([𝑥 / 𝑎][𝑦 / 𝑥][𝑎 / 𝑦]𝜑 ↔ 𝜑)) | ||
Theorem | nfich1 47371 | The first interchangeable setvar variable is not free. (Contributed by AV, 21-Aug-2023.) |
⊢ Ⅎ𝑥[𝑥⇄𝑦]𝜑 | ||
Theorem | nfich2 47372 | The second interchangeable setvar variable is not free. (Contributed by AV, 21-Aug-2023.) |
⊢ Ⅎ𝑦[𝑥⇄𝑦]𝜑 | ||
Theorem | ichv 47373* | Setvar variables are interchangeable in a wff they do not appear in. (Contributed by SN, 23-Nov-2023.) |
⊢ [𝑥⇄𝑦]𝜑 | ||
Theorem | ichf 47374 | Setvar variables are interchangeable in a wff they are not free in. (Contributed by SN, 23-Nov-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ [𝑥⇄𝑦]𝜑 | ||
Theorem | ichid 47375 | A setvar variable is always interchangeable with itself. (Contributed by AV, 29-Jul-2023.) |
⊢ [𝑥⇄𝑥]𝜑 | ||
Theorem | icht 47376 | A theorem is interchangeable. (Contributed by SN, 4-May-2024.) |
⊢ 𝜑 ⇒ ⊢ [𝑥⇄𝑦]𝜑 | ||
Theorem | ichbidv 47377* | Formula building rule for interchangeability (deduction). (Contributed by SN, 4-May-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑥⇄𝑦]𝜓 ↔ [𝑥⇄𝑦]𝜒)) | ||
Theorem | ichcircshi 47378* | The setvar variables are interchangeable if they can be circularily shifted using a third setvar variable, using implicit substitution. (Contributed by AV, 29-Jul-2023.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝑥 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜑)) ⇒ ⊢ [𝑥⇄𝑦]𝜑 | ||
Theorem | ichan 47379 | If two setvar variables are interchangeable in two wffs, then they are interchangeable in the conjunction of these two wffs. Notice that the reverse implication is not necessarily true. Corresponding theorems will hold for other commutative operations, too. (Contributed by AV, 31-Jul-2023.) Use df-ich 47370 instead of dfich2 47382 to reduce axioms. (Revised by SN, 4-May-2024.) |
⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) → [𝑎⇄𝑏](𝜑 ∧ 𝜓)) | ||
Theorem | ichn 47380 | Negation does not affect interchangeability. (Contributed by SN, 30-Aug-2023.) |
⊢ ([𝑎⇄𝑏]𝜑 ↔ [𝑎⇄𝑏] ¬ 𝜑) | ||
Theorem | ichim 47381 | Formula building rule for implication in interchangeability. (Contributed by SN, 4-May-2024.) |
⊢ (([𝑎⇄𝑏]𝜑 ∧ [𝑎⇄𝑏]𝜓) → [𝑎⇄𝑏](𝜑 → 𝜓)) | ||
Theorem | dfich2 47382* | Alternate definition of the property of a wff 𝜑 that the setvar variables 𝑥 and 𝑦 are interchangeable. (Contributed by AV and WL, 6-Aug-2023.) |
⊢ ([𝑥⇄𝑦]𝜑 ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)) | ||
Theorem | ichcom 47383* | The interchangeability of setvar variables is commutative. (Contributed by AV, 20-Aug-2023.) |
⊢ ([𝑥⇄𝑦]𝜓 ↔ [𝑦⇄𝑥]𝜓) | ||
Theorem | ichbi12i 47384* | Equivalence for interchangeable setvar variables. (Contributed by AV, 29-Jul-2023.) |
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝜓 ↔ 𝜒)) ⇒ ⊢ ([𝑥⇄𝑦]𝜓 ↔ [𝑎⇄𝑏]𝜒) | ||
Theorem | icheqid 47385 | In an equality for the same setvar variable, the setvar variable is interchangeable by itself. Special case of ichid 47375 and icheq 47386 without distinct variables restriction. (Contributed by AV, 29-Jul-2023.) |
⊢ [𝑥⇄𝑥]𝑥 = 𝑥 | ||
Theorem | icheq 47386* | In an equality of setvar variables, the setvar variables are interchangeable. (Contributed by AV, 29-Jul-2023.) |
⊢ [𝑥⇄𝑦]𝑥 = 𝑦 | ||
Theorem | ichnfimlem 47387* | Lemma for ichnfim 47388: A substitution for a nonfree variable has no effect. (Contributed by Wolf Lammen, 6-Aug-2023.) Avoid ax-13 2374. (Revised by GG, 1-May-2024.) |
⊢ (∀𝑦Ⅎ𝑥𝜑 → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑)) | ||
Theorem | ichnfim 47388* | If in an interchangeability context 𝑥 is not free in 𝜑, the same holds for 𝑦. (Contributed by Wolf Lammen, 6-Aug-2023.) (Revised by AV, 23-Sep-2023.) |
⊢ ((∀𝑦Ⅎ𝑥𝜑 ∧ [𝑥⇄𝑦]𝜑) → ∀𝑥Ⅎ𝑦𝜑) | ||
Theorem | ichnfb 47389* | If 𝑥 and 𝑦 are interchangeable in 𝜑, they are both free or both not free in 𝜑. (Contributed by Wolf Lammen, 6-Aug-2023.) (Revised by AV, 23-Sep-2023.) |
⊢ ([𝑥⇄𝑦]𝜑 → (∀𝑥Ⅎ𝑦𝜑 ↔ ∀𝑦Ⅎ𝑥𝜑)) | ||
Theorem | ichal 47390* | Move a universal quantifier inside interchangeability. (Contributed by SN, 30-Aug-2023.) |
⊢ (∀𝑥[𝑎⇄𝑏]𝜑 → [𝑎⇄𝑏]∀𝑥𝜑) | ||
Theorem | ich2al 47391 | Two setvar variables are always interchangeable when there are two universal quantifiers. (Contributed by SN, 23-Nov-2023.) |
⊢ [𝑥⇄𝑦]∀𝑥∀𝑦𝜑 | ||
Theorem | ich2ex 47392 | Two setvar variables are always interchangeable when there are two existential quantifiers. (Contributed by SN, 23-Nov-2023.) |
⊢ [𝑥⇄𝑦]∃𝑥∃𝑦𝜑 | ||
Theorem | ichexmpl1 47393* | Example for interchangeable setvar variables in a statement of predicate calculus with equality. (Contributed by AV, 31-Jul-2023.) |
⊢ [𝑎⇄𝑏]∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) | ||
Theorem | ichexmpl2 47394* | Example for interchangeable setvar variables in an arithmetic expression. (Contributed by AV, 31-Jul-2023.) |
⊢ [𝑎⇄𝑏]((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ((𝑎↑2) + (𝑏↑2)) = (𝑐↑2)) | ||
Theorem | ich2exprop 47395* | If the setvar variables are interchangeable in a wff, there is an ordered pair fulfilling the wff iff there is an unordered pair fulfilling the wff. (Contributed by AV, 16-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [𝑎⇄𝑏]𝜑) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏(〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 𝜑))) | ||
Theorem | ichnreuop 47396* | If the setvar variables are interchangeable in a wff, there is never a unique ordered pair with different components fulfilling the wff (because if 〈𝑎, 𝑏〉 fulfils the wff, then also 〈𝑏, 𝑎〉 fulfils the wff). (Contributed by AV, 27-Aug-2023.) |
⊢ ([𝑎⇄𝑏]𝜑 → ¬ ∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)) | ||
Theorem | ichreuopeq 47397* | If the setvar variables are interchangeable in a wff, and there is a unique ordered pair fulfilling the wff, then both setvar variables must be equal. (Contributed by AV, 28-Aug-2023.) |
⊢ ([𝑎⇄𝑏]𝜑 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜑) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑))) | ||
Theorem | sprid 47398 | Two identical representations of the class of all unordered pairs. (Contributed by AV, 21-Nov-2021.) |
⊢ {𝑝 ∣ ∃𝑎 ∈ V ∃𝑏 ∈ V 𝑝 = {𝑎, 𝑏}} = {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} | ||
Theorem | elsprel 47399* | An unordered pair is an element of all unordered pairs. At least one of the two elements of the unordered pair must be a set. Otherwise, the unordered pair would be the empty set, see prprc 4771, which is not an element of all unordered pairs, see spr0nelg 47400. (Contributed by AV, 21-Nov-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}}) | ||
Theorem | spr0nelg 47400* | The empty set is not an element of all unordered pairs. (Contributed by AV, 21-Nov-2021.) |
⊢ ∅ ∉ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |