![]() |
Metamath
Proof Explorer Theorem List (p. 346 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-restsn10 34501 | Special case of bj-restsn 34497, bj-restsnss 34498, and bj-rest10 34503. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → ({𝑋} ↾t ∅) = {∅}) | ||
Theorem | bj-restsnid 34502 | The elementwise intersection on the singleton on a class by that class is the singleton on that class. Special case of bj-restsn 34497 and bj-restsnss 34498. (Contributed by BJ, 27-Apr-2021.) |
⊢ ({𝐴} ↾t 𝐴) = {𝐴} | ||
Theorem | bj-rest10 34503 | An elementwise intersection on a nonempty family by the empty set is the singleton on the empty set. TODO: this generalizes rest0 21774 and could replace it. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → (𝑋 ≠ ∅ → (𝑋 ↾t ∅) = {∅})) | ||
Theorem | bj-rest10b 34504 | Alternate version of bj-rest10 34503. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ (𝑉 ∖ {∅}) → (𝑋 ↾t ∅) = {∅}) | ||
Theorem | bj-restn0 34505 | An elementwise intersection on a nonempty family is nonempty. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ≠ ∅ → (𝑋 ↾t 𝐴) ≠ ∅)) | ||
Theorem | bj-restn0b 34506 | Alternate version of bj-restn0 34505. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ (𝑉 ∖ {∅}) ∧ 𝐴 ∈ 𝑊) → (𝑋 ↾t 𝐴) ≠ ∅) | ||
Theorem | bj-restpw 34507 | The elementwise intersection on a powerset is the powerset of the intersection. This allows to prove for instance that the topology induced on a subset by the discrete topology is the discrete topology on that subset. See also restdis 21783 (which uses distop 21600 and restopn2 21782). (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝒫 𝑌 ↾t 𝐴) = 𝒫 (𝑌 ∩ 𝐴)) | ||
Theorem | bj-rest0 34508 | An elementwise intersection on a family containing the empty set contains the empty set. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∅ ∈ 𝑋 → ∅ ∈ (𝑋 ↾t 𝐴))) | ||
Theorem | bj-restb 34509 | An elementwise intersection by a set on a family containing a superset of that set contains that set. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑋) → 𝐴 ∈ (𝑋 ↾t 𝐴))) | ||
Theorem | bj-restv 34510 | An elementwise intersection by a subset on a family containing the whole set contains the whole subset. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝐴 ⊆ ∪ 𝑋 ∧ ∪ 𝑋 ∈ 𝑋) → 𝐴 ∈ (𝑋 ↾t 𝐴)) | ||
Theorem | bj-resta 34511 | An elementwise intersection by a set on a family containing that set contains that set. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → (𝐴 ∈ 𝑋 → 𝐴 ∈ (𝑋 ↾t 𝐴))) | ||
Theorem | bj-restuni 34512 | The union of an elementwise intersection by a set is equal to the intersection with that set of the union of the family. See also restuni 21767 and restuni2 21772. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ∪ (𝑋 ↾t 𝐴) = (∪ 𝑋 ∩ 𝐴)) | ||
Theorem | bj-restuni2 34513 | The union of an elementwise intersection on a family of sets by a subset is equal to that subset. See also restuni 21767 and restuni2 21772. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋) → ∪ (𝑋 ↾t 𝐴) = 𝐴) | ||
Theorem | bj-restreg 34514 | A reformulation of the axiom of regularity using elementwise intersection. (RK: might have to be placed later since theorems in this section are to be moved early (in the section related to the algebra of sets).) (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → ∅ ∈ (𝐴 ↾t 𝐴)) | ||
Theorem | bj-raldifsn 34515* | All elements in a set satisfy a given property if and only if all but one satisfy that property and that one also does. Typically, this can be used for characterizations that are proved using different methods for a given element and for all others, for instance zero and nonzero numbers, or the empty set and nonempty sets. (Contributed by BJ, 7-Dec-2021.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ 𝜓))) | ||
Theorem | bj-0int 34516* | If 𝐴 is a collection of subsets of 𝑋, like a Moore collection or a topology, two equivalent ways to say that arbitrary intersections of elements of 𝐴 relative to 𝑋 belong to some class 𝐵: the LHS singles out the empty intersection (the empty intersection relative to 𝑋 is 𝑋 and the intersection of a nonempty family of subsets of 𝑋 is included in 𝑋, so there is no need to intersect it with 𝑋). In typical applications, 𝐵 is 𝐴 itself. (Contributed by BJ, 7-Dec-2021.) |
⊢ (𝐴 ⊆ 𝒫 𝑋 → ((𝑋 ∈ 𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})∩ 𝑥 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝒫 𝐴(𝑋 ∩ ∩ 𝑥) ∈ 𝐵)) | ||
Theorem | bj-mooreset 34517* |
A Moore collection is a set. Therefore, the class Moore of all
Moore sets defined in df-bj-moore 34519 is actually the class of all Moore
collections. This is also illustrated by the lack of sethood condition
in bj-ismoore 34520.
Note that the closed sets of a topology form a Moore collection, so a topology is a set, and this remark also applies to many other families of sets (namely, as soon as the whole set is required to be a set of the family, then the associated kind of family has no proper classes: that this condition suffices to impose sethood can be seen in this proof, which relies crucially on uniexr 7465). Note: if, in the above predicate, we substitute 𝒫 𝑋 for 𝐴, then the last ∈ 𝒫 𝑋 could be weakened to ⊆ 𝑋, and then the predicate would be obviously satisfied since ⊢ ∪ 𝒫 𝑋 = 𝑋 (unipw 5308) , making 𝒫 𝑋 a Moore collection in this weaker sense, for any class 𝑋, even proper, but the addition of this single case does not add anything interesting. Instead, we have the biconditional bj-discrmoore 34526. (Contributed by BJ, 8-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴 → 𝐴 ∈ V) | ||
Syntax | cmoore 34518 | Syntax for the class of Moore collections. |
class Moore | ||
Definition | df-bj-moore 34519* |
Define the class of Moore collections. This is indeed the class of all
Moore collections since these all are sets, as proved in bj-mooreset 34517,
and as illustrated by the lack of sethood condition in bj-ismoore 34520.
This is to df-mre 16849 (defining Moore) what df-top 21499 (defining Top) is to df-topon 21516 (defining TopOn). For the sake of consistency, the function defined at df-mre 16849 should be denoted by "MooreOn". Note: df-mre 16849 singles out the empty intersection. This is not necessary. It could be written instead ⊢ Moore = (𝑥 ∈ V ↦ {𝑦 ∈ 𝒫 𝒫 𝑥 ∣ ∀𝑧 ∈ 𝒫 𝑦(𝑥 ∩ ∩ 𝑧) ∈ 𝑦}) and the equivalence of both definitions is proved by bj-0int 34516. There is no added generality in defining a "Moore predicate" for arbitrary classes, since a Moore class satisfying such a predicate is automatically a set (see bj-mooreset 34517). TODO: move to the main section. For many families of sets, one can define both the function associating to each set the set of families of that kind on it (like df-mre 16849 and df-topon 21516) or the class of all families of that kind, independent of a base set (like df-bj-moore 34519 or df-top 21499). In general, the former will be more useful and the extra generality of the latter is not necessary. Moore collections, however, are particular in that they are more ubiquitous and are used in a wide variety of applications (for many families of sets, the family of families of a given kind is often a Moore collection, for instance). Therefore, in the case of Moore families, having both definitions is useful. (Contributed by BJ, 27-Apr-2021.) |
⊢ Moore = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥} | ||
Theorem | bj-ismoore 34520* | Characterization of Moore collections. Note that there is no sethood hypothesis on 𝐴: it is implied by either side (this is obvious for the LHS, and is the content of bj-mooreset 34517 for the RHS). (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ Moore ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴) | ||
Theorem | bj-ismoored0 34521 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ Moore → ∪ 𝐴 ∈ 𝐴) | ||
Theorem | bj-ismoored 34522 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ Moore) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (∪ 𝐴 ∩ ∩ 𝐵) ∈ 𝐴) | ||
Theorem | bj-ismoored2 34523 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ Moore) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → ∩ 𝐵 ∈ 𝐴) | ||
Theorem | bj-ismooredr 34524* | Sufficient condition to be a Moore collection. Note that there is no sethood hypothesis on 𝐴: it is a consequence of the only hypothesis. (Contributed by BJ, 9-Dec-2021.) |
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ Moore) | ||
Theorem | bj-ismooredr2 34525* | Sufficient condition to be a Moore collection (variant of bj-ismooredr 34524 singling out the empty intersection). Note that there is no sethood hypothesis on 𝐴: it is a consequence of the first hypothesis. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → ∪ 𝐴 ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅)) → ∩ 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ Moore) | ||
Theorem | bj-discrmoore 34526 | The powerclass 𝒫 𝐴 is a Moore collection if and only if 𝐴 is a set. It is then called the discrete Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ Moore) | ||
Theorem | bj-0nmoore 34527 | The empty set is not a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ ¬ ∅ ∈ Moore | ||
Theorem | bj-snmoore 34528 | A singleton is a Moore collection. See bj-snmooreb 34529 for a biconditional version. (Contributed by BJ, 10-Apr-2024.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Moore) | ||
Theorem | bj-snmooreb 34529 | A singleton is a Moore collection, biconditional version. (Contributed by BJ, 9-Dec-2021.) (Proof shortened by BJ, 10-Apr-2024.) |
⊢ (𝐴 ∈ V ↔ {𝐴} ∈ Moore) | ||
Theorem | bj-prmoore 34530 |
A pair formed of two nested sets is a Moore collection. (Note that in
the statement, if 𝐵 is a proper class, we are in the
case of
bj-snmoore 34528). A direct consequence is ⊢ {∅, 𝐴} ∈ Moore.
More generally, any nonempty well-ordered chain of sets that is a set is a Moore collection. We also have the biconditional ⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → ({𝐴, 𝐵} ∈ Moore ↔ (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))). (Contributed by BJ, 11-Apr-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → {𝐴, 𝐵} ∈ Moore) | ||
Theorem | bj-0nelmpt 34531 | The empty set is not an element of a function (given in maps-to notation). (Contributed by BJ, 30-Dec-2020.) |
⊢ ¬ ∅ ∈ (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | bj-mptval 34532 | Value of a function given in maps-to notation. (Contributed by BJ, 30-Dec-2020.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑋 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑋) = 𝑌 ↔ 𝑋(𝑥 ∈ 𝐴 ↦ 𝐵)𝑌))) | ||
Theorem | bj-dfmpoa 34533* | An equivalent definition of df-mpo 7140. (Contributed by BJ, 30-Dec-2020.) |
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈𝑠, 𝑡〉 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑠 = 〈𝑥, 𝑦〉 ∧ 𝑡 = 𝐶)} | ||
Theorem | bj-mpomptALT 34534* | Alternate proof of mpompt 7245. (Contributed by BJ, 30-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) | ||
Syntax | cmpt3 34535 | Syntax for maps-to notation for functions with three arguments. |
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) | ||
Definition | df-bj-mpt3 34536* | Define maps-to notation for functions with three arguments. See df-mpt 5111 and df-mpo 7140 for functions with one and two arguments respectively. This definition is analogous to bj-dfmpoa 34533. (Contributed by BJ, 11-Apr-2020.) |
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) = {〈𝑠, 𝑡〉 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑠 = 〈𝑥, 𝑦, 𝑧〉 ∧ 𝑡 = 𝐷)} | ||
Currying and uncurrying. See also df-cur 7916 and df-unc 7917. Contrary to these, the definitions in this section are parameterized. | ||
Syntax | csethom 34537 | Syntax for the set of set morphisms. |
class Set⟶ | ||
Definition | df-bj-sethom 34538* |
Define the set of functions (morphisms of sets) between two sets. Same
as df-map 8391 with arguments swapped. TODO: prove the same
staple lemmas
as for ↑m.
Remark: one may define Set⟶ = (𝑥 ∈ dom Struct , 𝑦 ∈ dom Struct ↦ {𝑓 ∣ 𝑓:(Base‘𝑥)⟶(Base‘𝑦)}) so that for morphisms between other structures, one could write ... = {𝑓 ∈ (𝑥 Set⟶ 𝑦) ∣ ...}. (Contributed by BJ, 11-Apr-2020.) |
⊢ Set⟶ = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑥⟶𝑦}) | ||
Syntax | ctophom 34539 | Syntax for the set of topological morphisms. |
class Top⟶ | ||
Definition | df-bj-tophom 34540* | Define the set of continuous functions (morphisms of topological spaces) between two topological spaces. Similar to df-cn 21832 (which is in terms of topologies instead of topological spaces). (Contributed by BJ, 10-Feb-2022.) |
⊢ Top⟶ = (𝑥 ∈ TopSp, 𝑦 ∈ TopSp ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (TopOpen‘𝑦)(◡𝑓 “ 𝑢) ∈ (TopOpen‘𝑥)}) | ||
Syntax | cmgmhom 34541 | Syntax for the set of magma morphisms. |
class Mgm⟶ | ||
Definition | df-bj-mgmhom 34542* | Define the set of magma morphisms between two magmas. If domain and codomain are semigroups, monoids, or groups, then one obtains the set of morphisms of these structures. (Contributed by BJ, 10-Feb-2022.) |
⊢ Mgm⟶ = (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))}) | ||
Syntax | ctopmgmhom 34543 | Syntax for the set of topological magma morphisms. |
class TopMgm⟶ | ||
Definition | df-bj-topmgmhom 34544* | Define the set of topological magma morphisms (continuous magma morphisms) between two topological magmas. If domain and codomain are topological semigroups, monoids, or groups, then one obtains the set of morphisms of these structures. This definition is currently stated with topological monoid domain and codomain, since topological magmas are currently not defined in set.mm. (Contributed by BJ, 10-Feb-2022.) |
⊢ TopMgm⟶ = (𝑥 ∈ TopMnd, 𝑦 ∈ TopMnd ↦ ((𝑥 Top⟶ 𝑦) ∩ (𝑥 Mgm⟶ 𝑦))) | ||
Syntax | ccur- 34545 | Syntax for the parameterized currying function. |
class curry_ | ||
Definition | df-bj-cur 34546* | Define currying. See also df-cur 7916. (Contributed by BJ, 11-Apr-2020.) |
⊢ curry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ ((𝑥 × 𝑦) Set⟶ 𝑧) ↦ (𝑎 ∈ 𝑥 ↦ (𝑏 ∈ 𝑦 ↦ (𝑓‘〈𝑎, 𝑏〉))))) | ||
Syntax | cunc- 34547 | Notation for the parameterized uncurrying function. |
class uncurry_ | ||
Definition | df-bj-unc 34548* | Define uncurrying. See also df-unc 7917. (Contributed by BJ, 11-Apr-2020.) |
⊢ uncurry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ (𝑥 Set⟶ (𝑦 Set⟶ 𝑧)) ↦ (𝑎 ∈ 𝑥, 𝑏 ∈ 𝑦 ↦ ((𝑓‘𝑎)‘𝑏)))) | ||
Groundwork for changing the definition, syntax and token for component-setting in extensible structures. See https://github.com/metamath/set.mm/issues/2401 | ||
Syntax | cstrset 34549 | Syntax for component-setting in extensible structures. |
class [𝐵 / 𝐴]struct𝑆 | ||
Definition | df-strset 34550 | Component-setting in extensible structures. Define the extensible structure [𝐵 / 𝐴]struct𝑆, which is like the extensible structure 𝑆 except that the value 𝐵 has been put in the slot 𝐴 (replacing the current value if there was already one). In such expressions, 𝐴 is generally substituted for slot mnemonics like Base or +g or dist. (Contributed by BJ, 13-Feb-2022.) |
⊢ [𝐵 / 𝐴]struct𝑆 = ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {〈(𝐴‘ndx), 𝐵〉}) | ||
Theorem | setsstrset 34551 | Relation between df-sets 16482 and df-strset 34550. Temporary theorem kept during the transition from the former to the latter. (Contributed by BJ, 13-Feb-2022.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → [𝐵 / 𝐴]struct𝑆 = (𝑆 sSet 〈(𝐴‘ndx), 𝐵〉)) | ||
In this section, we indroduce several supersets of the set ℝ of real numbers and the set ℂ of complex numbers. Once they are given their usual topologies, which are locally compact, both topological spaces have a one-point compactification. They are denoted by ℝ̂ and ℂ̂ respectively, defined in df-bj-cchat 34648 and df-bj-rrhat 34650, and the point at infinity is denoted by ∞, defined in df-bj-infty 34646. Both ℝ and ℂ also have "directional compactifications", denoted respectively by ℝ̅, defined in df-bj-rrbar 34644 (already defined as ℝ*, see df-xr 10668) and ℂ̅, defined in df-bj-ccbar 34631. Since ℂ̅ does not seem to be standard, we describe it in some detail. It is obtained by adding to ℂ a "point at infinity at the end of each ray with origin at 0". Although ℂ̅ is not an important object in itself, the motivation for introducing it is to provide a common superset to both ℝ̅ and ℂ and to define algebraic operations (addition, opposite, multiplication, inverse) as widely as reasonably possible. Mathematically, ℂ̅ is the quotient of ((ℂ × ℝ≥0) ∖ {〈0, 0〉}) by the diagonal multiplicative action of ℝ>0 (think of the closed "northern hemisphere" in ℝ^3 identified with (ℂ × ℝ), that each open ray from 0 included in the closed northern half-space intersects exactly once). Since in set.mm, we want to have a genuine inclusion ℂ ⊆ ℂ̅, we instead define ℂ̅ as the (disjoint) union of ℂ with a circle at infinity denoted by ℂ∞. To have a genuine inclusion ℝ̅ ⊆ ℂ̅, we define +∞ and -∞ as certain points in ℂ∞. Thanks to this framework, one has the genuine inclusions ℝ ⊆ ℝ̅ and ℝ ⊆ ℝ̂ and similarly ℂ ⊆ ℂ̅ and ℂ ⊆ ℂ̂. Furthermore, one has ℝ ⊆ ℂ as well as ℝ̅ ⊆ ℂ̅ and ℝ̂ ⊆ ℂ̂. Furthermore, we define the main algebraic operations on (ℂ̅ ∪ ℂ̂), which is not very mathematical, but "overloads" the operations, so that one can use the same notation in all cases. | ||
Theorem | bj-nfald 34552 | Variant of nfald 2336. (Contributed by BJ, 25-Dec-2023.) |
⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) | ||
Theorem | bj-nfexd 34553 | Variant of nfexd 2337. (Contributed by BJ, 25-Dec-2023.) |
⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓) | ||
Theorem | copsex2d 34554* | Implicit substitution deduction for ordered pairs. (Contributed by BJ, 25-Dec-2023.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑦𝜒) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒)) | ||
Theorem | copsex2b 34555* | Biconditional form of copsex2d 34554. TODO: prove a relative version, that is, with ∃𝑥 ∈ 𝑉∃𝑦 ∈ 𝑊...(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊). (Contributed by BJ, 27-Dec-2023.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑦𝜒) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))) | ||
Theorem | opelopabd 34556* | Membership of an ordere pair in a class abstraction of ordered pairs. (Contributed by BJ, 17-Dec-2023.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑦𝜒) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ 𝜒)) | ||
Theorem | opelopabb 34557* | Membership of an ordered pair in a class abstraction of ordered pairs, biconditional form. (Contributed by BJ, 17-Dec-2023.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑦𝜒) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))) | ||
Theorem | opelopabbv 34558* | Membership of an ordered pair in a class abstraction of ordered pairs, biconditional form. (Contributed by BJ, 17-Dec-2023.) |
⊢ (𝜑 → 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜓}) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ∈ 𝑅 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))) | ||
Theorem | bj-opelrelex 34559 | The coordinates of an ordered pair that belongs to a relation are sets. TODO: Slightly shorter than brrelex12 5568, which could be proved from it. (Contributed by BJ, 27-Dec-2023.) |
⊢ ((Rel 𝑅 ∧ 〈𝐴, 𝐵〉 ∈ 𝑅) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | bj-opelresdm 34560 | If an ordered pair is in a restricted binary relation, then its first component is an element of the restricting class. See also opelres 5824. (Contributed by BJ, 25-Dec-2023.) |
⊢ (〈𝐴, 𝐵〉 ∈ (𝑅 ↾ 𝑋) → 𝐴 ∈ 𝑋) | ||
Theorem | bj-brresdm 34561 |
If two classes are related by a restricted binary relation, then the first
class is an element of the restricting class. See also brres 5825 and
brrelex1 5569.
Remark: there are many pairs like bj-opelresdm 34560 / bj-brresdm 34561, where one uses membership of ordered pairs and the other, related classes (for instance, bj-opelresdm 34560 / brrelex12 5568 or the opelopabg 5390 / brabg 5391 family). They are straightforwardly equivalent by df-br 5031. The latter is indeed a very direct definition, introducing a "shorthand", and barely necessary, were it not for the frequency of the expression 𝐴𝑅𝐵. Therefore, in the spirit of "definitions are here to be used", most theorems, apart from the most elementary ones, should only have the "br" version, not the "opel" one. (Contributed by BJ, 25-Dec-2023.) |
⊢ (𝐴(𝑅 ↾ 𝑋)𝐵 → 𝐴 ∈ 𝑋) | ||
Theorem | brabd0 34562* | Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by BJ, 17-Dec-2023.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑦𝜒) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜓}) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝜒)) | ||
Theorem | brabd 34563* | Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by BJ, 17-Dec-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜓}) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝜒)) | ||
Theorem | bj-brab2a1 34564* | "Unbounded" version of brab2a 5608. (Contributed by BJ, 25-Dec-2023.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜓)) | ||
Complements on the identity relation. | ||
Theorem | bj-opabssvv 34565* | A variant of relopabiv 5657 (which could be proved from it, similarly to relxp 5537 from xpss 5535). (Contributed by BJ, 28-Dec-2023.) |
⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ (V × V) | ||
Theorem | bj-funidres 34566 |
The restricted identity relation is a function. (Contributed by BJ,
27-Dec-2023.)
TODO: relabel funi 6356 to funid. |
⊢ Fun ( I ↾ 𝑉) | ||
Theorem | bj-opelidb 34567 |
Characterization of the ordered pair elements of the identity relation.
Remark: in deduction-style proofs, one could save a few syntactic steps by using another antecedent than ⊤ which already appears in the proof. Here for instance this could be the definition I = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} but this would make the proof less easy to read. (Contributed by BJ, 27-Dec-2023.) |
⊢ (〈𝐴, 𝐵〉 ∈ I ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝐴 = 𝐵)) | ||
Theorem | bj-opelidb1 34568 | Characterization of the ordered pair elements of the identity relation. Variant of bj-opelidb 34567 where only the sethood of the first component is expressed. (Contributed by BJ, 27-Dec-2023.) |
⊢ (〈𝐴, 𝐵〉 ∈ I ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵)) | ||
Theorem | bj-inexeqex 34569 | Lemma for bj-opelid 34571 (but not specific to the identity relation): if the intersection of two classes is a set and the two classes are equal, then both are sets (all three classes are equal, so they all belong to 𝑉, but it is more convenient to have V in the consequent for theorems using it). (Contributed by BJ, 27-Dec-2023.) |
⊢ (((𝐴 ∩ 𝐵) ∈ 𝑉 ∧ 𝐴 = 𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | bj-elsn0 34570 | If the intersection of two classes is a set, then these classes are equal if and only if one is an element of the singleton formed on the other. Stronger form of elsng 4539 and elsn2g 4563 (which could be proved from it). (Contributed by BJ, 20-Jan-2024.) |
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-opelid 34571 | Characterization of the ordered pair elements of the identity relation when the intersection of their components are sets. Note that the antecedent is more general than either component being a set. (Contributed by BJ, 29-Mar-2020.) |
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (〈𝐴, 𝐵〉 ∈ I ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-ideqg 34572 |
Characterization of the classes related by the identity relation when
their intersection is a set. Note that the antecedent is more general
than either class being a set. (Contributed by NM, 30-Apr-2004.) Weaken
the antecedent to sethood of the intersection. (Revised by BJ,
24-Dec-2023.)
TODO: replace ideqg 5686, or at least prove ideqg 5686 from it. |
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-ideqgALT 34573 | Alternate proof of bj-ideqg 34572 from brabga 5386 instead of bj-opelid 34571 itself proved from bj-opelidb 34567. (Contributed by BJ, 27-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-ideqb 34574 | Characterization of classes related by the identity relation. (Contributed by BJ, 24-Dec-2023.) |
⊢ (𝐴 I 𝐵 ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵)) | ||
Theorem | bj-idres 34575 |
Alternate expression for the restricted identity relation. The
advantage of that expression is to expose it as a "bounded"
class, being
included in the Cartesian square of the restricting class. (Contributed
by BJ, 27-Dec-2023.)
This is an alternate of idinxpresid 5882 (see idinxpres 5881). See also elrid 5880 and elidinxp 5878. (Proof modification is discouraged.) |
⊢ ( I ↾ 𝐴) = ( I ∩ (𝐴 × 𝐴)) | ||
Theorem | bj-opelidres 34576 | Characterization of the ordered pairs in the restricted identity relation when the intersection of their component belongs to the restricting class. TODO: prove bj-idreseq 34577 from it. (Contributed by BJ, 29-Mar-2020.) |
⊢ (𝐴 ∈ 𝑉 → (〈𝐴, 𝐵〉 ∈ ( I ↾ 𝑉) ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-idreseq 34577 | Sufficient condition for the restricted identity relation to agree with equality. Note that the instance of bj-ideqg 34572 with V substituted for 𝑉 is a direct consequence of bj-idreseq 34577. This is a strengthening of resieq 5829 which should be proved from it (note that currently, resieq 5829 relies on ideq 5687). Note that the intersection in the antecedent is not very meaningful, but is a device to prove versions with either class assumed to be a set. It could be enough to prove the version with a disjunctive antecedent: ⊢ ((𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶) → .... (Contributed by BJ, 25-Dec-2023.) |
⊢ ((𝐴 ∩ 𝐵) ∈ 𝐶 → (𝐴( I ↾ 𝐶)𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-idreseqb 34578 | Characterization for two classes to be related under the restricted identity relation. (Contributed by BJ, 24-Dec-2023.) |
⊢ (𝐴( I ↾ 𝐶)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵)) | ||
Theorem | bj-ideqg1 34579 |
For sets, the identity relation is the same thing as equality.
(Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon,
27-Aug-2011.) Generalize to a disjunctive antecedent. (Revised by BJ,
24-Dec-2023.)
TODO: delete once bj-ideqg 34572 is in the main section. |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-ideqg1ALT 34580 |
Alternate proof of bj-ideqg1 using brabga 5386 instead of the "unbounded"
version bj-brab2a1 34564 or brab2a 5608. (Contributed by BJ, 25-Dec-2023.)
(Proof modification is discouraged.) (New usage is discouraged.)
TODO: delete once bj-ideqg 34572 is in the main section. |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-opelidb1ALT 34581 | Characterization of the couples in I. (Contributed by BJ, 29-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (〈𝐴, 𝐵〉 ∈ I ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵)) | ||
Theorem | bj-elid3 34582 | Characterization of the couples in I whose first component is a setvar. (Contributed by BJ, 29-Mar-2020.) |
⊢ (〈𝑥, 𝐴〉 ∈ I ↔ 𝑥 = 𝐴) | ||
Theorem | bj-elid4 34583 | Characterization of the elements of I. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ (𝑉 × 𝑊) → (𝐴 ∈ I ↔ (1st ‘𝐴) = (2nd ‘𝐴))) | ||
Theorem | bj-elid5 34584 | Characterization of the elements of I. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ I ↔ (𝐴 ∈ (V × V) ∧ (1st ‘𝐴) = (2nd ‘𝐴))) | ||
Theorem | bj-elid6 34585 | Characterization of the elements of the diagonal of a Cartesian square. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐵 ∈ ( I ↾ 𝐴) ↔ (𝐵 ∈ (𝐴 × 𝐴) ∧ (1st ‘𝐵) = (2nd ‘𝐵))) | ||
Theorem | bj-elid7 34586 | Characterization of the elements of the diagonal of a Cartesian square. (Contributed by BJ, 22-Jun-2019.) |
⊢ (〈𝐵, 𝐶〉 ∈ ( I ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶)) | ||
This subsection defines a functionalized version of the identity relation, that can also be seen as the diagonal in a Cartesian square). As explained in df-bj-diag 34588, it will probably be deleted. | ||
Syntax | cdiag2 34587 | Syntax for the diagonal of the Cartesian square of a set. |
class Id | ||
Definition | df-bj-diag 34588 |
Define the functionalized identity, which can also be seen as the diagonal
function. Its value is given in bj-diagval 34589 when it is viewed as the
functionalized identity, and in bj-diagval2 34590 when it is viewed as the
diagonal function.
Indeed, Definition df-br 5031 identifies a binary relation with the class of couples that are related by that binary relation (see eqrel2 35717 for the extensionality property of binary relations). As a consequence, the identity relation, or identity function (see funi 6356), on any class, can alternatively be seen as the diagonal of the cartesian square of that class. The identity relation on the universal class, I, is an "identity relation generator", since its restriction to any class is the identity relation on that class. It may be useful to consider a functionalized version of that fact, and that is the purpose of df-bj-diag 34588. Note: most proofs will only use its values (Id‘𝐴), in which case it may be enough to use ( I ↾ 𝐴) everywhere and dispense with this definition. (Contributed by BJ, 22-Jun-2019.) |
⊢ Id = (𝑥 ∈ V ↦ ( I ↾ 𝑥)) | ||
Theorem | bj-diagval 34589 | Value of the funtionalized identity, or equivalently of the diagonal function. This expression views it as the functionalized identity, whereas bj-diagval2 34590 views it as the diagonal function. See df-bj-diag 34588 for the terminology. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ 𝑉 → (Id‘𝐴) = ( I ↾ 𝐴)) | ||
Theorem | bj-diagval2 34590 | Value of the funtionalized identity, or equivalently of the diagonal function. This expression views it as the diagonal function, whereas bj-diagval 34589 views it as the functionalized identity. See df-bj-diag 34588 for the terminology. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ 𝑉 → (Id‘𝐴) = ( I ∩ (𝐴 × 𝐴))) | ||
Theorem | bj-eldiag 34591 | Characterization of the elements of the diagonal of a Cartesian square. Subsumed by bj-elid6 34585. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ (Id‘𝐴) ↔ (𝐵 ∈ (𝐴 × 𝐴) ∧ (1st ‘𝐵) = (2nd ‘𝐵)))) | ||
Theorem | bj-eldiag2 34592 | Characterization of the elements of the diagonal of a Cartesian square. Subsumed by bj-elid7 34586. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ 𝑉 → (〈𝐵, 𝐶〉 ∈ (Id‘𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶))) | ||
Definitions of the functionalized direct image and inverse image. The functionalized direct (resp. inverse) image is the morphism component of the covariant (resp. contravariant) powerset endofunctor of the category of sets and relations (and, up to restriction, of its subcategory of sets and functions). Its object component is the powerset operation 𝒫 defined in df-pw 4499. | ||
Syntax | cimdir 34593 | Syntax for the functionalized direct image. |
class 𝒫* | ||
Definition | df-imdir 34594* | Definition of the functionalized direct image, which maps a binary relation between two given sets to its associated direct image relation. (Contributed by BJ, 16-Dec-2023.) |
⊢ 𝒫* = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ (𝑟 “ 𝑥) = 𝑦)})) | ||
Theorem | bj-imdirvallem 34595* | Lemma for bj-imdirval 34596 and bj-iminvval 34608. (Contributed by BJ, 23-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ 𝜓)})) ⇒ ⊢ (𝜑 → (𝐴𝐶𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝜓)})) | ||
Theorem | bj-imdirval 34596* | Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴𝒫*𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ (𝑟 “ 𝑥) = 𝑦)})) | ||
Theorem | bj-imdirval2lem 34597* | Lemma for bj-imdirval2 34598 and bj-iminvval2 34609. (Contributed by BJ, 23-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝜓)} ∈ V) | ||
Theorem | bj-imdirval2 34598* | Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵)) ⇒ ⊢ (𝜑 → ((𝐴𝒫*𝐵)‘𝑅) = {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ (𝑅 “ 𝑥) = 𝑦)}) | ||
Theorem | bj-imdirval3 34599 | Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵)) ⇒ ⊢ (𝜑 → (𝑋((𝐴𝒫*𝐵)‘𝑅)𝑌 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐵) ∧ (𝑅 “ 𝑋) = 𝑌))) | ||
Theorem | bj-imdiridlem 34600* | Lemma for bj-imdirid 34601 and bj-iminvid 34610. (Contributed by BJ, 26-May-2024.) |
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝜑 ↔ 𝑥 = 𝑦)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝜑)} = ( I ↾ 𝒫 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |