![]() |
Metamath
Proof Explorer Theorem List (p. 372 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 | bj-mpomptALT 37101* | Alternate proof of mpompt 7546. (Contributed by BJ, 30-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) | ||
Syntax | cmpt3 37102 | Syntax for maps-to notation for functions with three arguments. |
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) | ||
Definition | df-bj-mpt3 37103* | Define maps-to notation for functions with three arguments. See df-mpt 5231 and df-mpo 7435 for functions with one and two arguments respectively. This definition is analogous to bj-dfmpoa 37100. (Contributed by BJ, 11-Apr-2020.) |
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) = {〈𝑠, 𝑡〉 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑠 = 〈𝑥, 𝑦, 𝑧〉 ∧ 𝑡 = 𝐷)} | ||
Currying and uncurrying. See also df-cur 8290 and df-unc 8291. Contrary to these, the definitions in this section are parameterized. | ||
Syntax | csethom 37104 | Syntax for the set of set morphisms. |
class Set⟶ | ||
Definition | df-bj-sethom 37105* |
Define the set of functions (morphisms of sets) between two sets. Same
as df-map 8866 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 37106 | Syntax for the set of topological morphisms. |
class Top⟶ | ||
Definition | df-bj-tophom 37107* | Define the set of continuous functions (morphisms of topological spaces) between two topological spaces. Similar to df-cn 23250 (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 37108 | Syntax for the set of magma morphisms. |
class Mgm⟶ | ||
Definition | df-bj-mgmhom 37109* | 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 37110 | Syntax for the set of topological magma morphisms. |
class TopMgm⟶ | ||
Definition | df-bj-topmgmhom 37111* | 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- 37112 | Syntax for the parameterized currying function. |
class curry_ | ||
Definition | df-bj-cur 37113* | Define currying. See also df-cur 8290. (Contributed by BJ, 11-Apr-2020.) |
⊢ curry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ ((𝑥 × 𝑦) Set⟶ 𝑧) ↦ (𝑎 ∈ 𝑥 ↦ (𝑏 ∈ 𝑦 ↦ (𝑓‘〈𝑎, 𝑏〉))))) | ||
Syntax | cunc- 37114 | Notation for the parameterized uncurrying function. |
class uncurry_ | ||
Definition | df-bj-unc 37115* | Define uncurrying. See also df-unc 8291. (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 37116 | Syntax for component-setting in extensible structures. |
class [𝐵 / 𝐴]struct𝑆 | ||
Definition | df-strset 37117 | 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. The V in this definition was chosen to be closer to df-sets 17197, but since extensible structures are functions on ℕ, it will be more natural to replace it with ℕ when df-strset 37117 becomes the main definition. (Contributed by BJ, 13-Feb-2022.) |
⊢ [𝐵 / 𝐴]struct𝑆 = ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {〈(𝐴‘ndx), 𝐵〉}) | ||
Theorem | setsstrset 37118 | Relation between df-sets 17197 and df-strset 37117. 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 37215 and df-bj-rrhat 37217, and the point at infinity is denoted by ∞, defined in df-bj-infty 37213. Both ℝ and ℂ also have "directional compactifications", denoted respectively by ℝ̅, defined in df-bj-rrbar 37211 (already defined as ℝ*, see df-xr 11296) and ℂ̅, defined in df-bj-ccbar 37198. 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 37119 | Variant of nfald 2326. (Contributed by BJ, 25-Dec-2023.) |
⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓) | ||
Theorem | bj-nfexd 37120 | Variant of nfexd 2327. (Contributed by BJ, 25-Dec-2023.) |
⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓) | ||
Theorem | copsex2d 37121* | Implicit substitution deduction for ordered pairs. (Contributed by BJ, 25-Dec-2023.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑦𝜒) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒)) | ||
Theorem | copsex2b 37122* | Biconditional form of copsex2d 37121. TODO: prove a relative version, that is, with ∃𝑥 ∈ 𝑉∃𝑦 ∈ 𝑊...(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊). (Contributed by BJ, 27-Dec-2023.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑦𝜒) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))) | ||
Theorem | opelopabd 37123* | Membership of an ordere pair in a class abstraction of ordered pairs. (Contributed by BJ, 17-Dec-2023.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑦𝜒) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ 𝜒)) | ||
Theorem | opelopabb 37124* | Membership of an ordered pair in a class abstraction of ordered pairs, biconditional form. (Contributed by BJ, 17-Dec-2023.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑦𝜒) & ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))) | ||
Theorem | opelopabbv 37125* | 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 37126 | The coordinates of an ordered pair that belongs to a relation are sets. TODO: Slightly shorter than brrelex12 5740, which could be proved from it. (Contributed by BJ, 27-Dec-2023.) |
⊢ ((Rel 𝑅 ∧ 〈𝐴, 𝐵〉 ∈ 𝑅) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | bj-opelresdm 37127 | If an ordered pair is in a restricted binary relation, then its first component is an element of the restricting class. See also opelres 6005. (Contributed by BJ, 25-Dec-2023.) |
⊢ (〈𝐴, 𝐵〉 ∈ (𝑅 ↾ 𝑋) → 𝐴 ∈ 𝑋) | ||
Theorem | bj-brresdm 37128 |
If two classes are related by a restricted binary relation, then the first
class is an element of the restricting class. See also brres 6006 and
brrelex1 5741.
Remark: there are many pairs like bj-opelresdm 37127 / bj-brresdm 37128, where one uses membership of ordered pairs and the other, related classes (for instance, bj-opelresdm 37127 / brrelex12 5740 or the opelopabg 5547 / brabg 5548 family). They are straightforwardly equivalent by df-br 5148. 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 37129* | 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 37130* | 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 37131* | "Unbounded" version of brab2a 5781. (Contributed by BJ, 25-Dec-2023.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜓)) | ||
Complements on the identity relation. | ||
Theorem | bj-opabssvv 37132* | A variant of relopabiv 5832 (which could be proved from it, similarly to relxp 5706 from xpss 5704). (Contributed by BJ, 28-Dec-2023.) |
⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ (V × V) | ||
Theorem | bj-funidres 37133 |
The restricted identity relation is a function. (Contributed by BJ,
27-Dec-2023.)
TODO: relabel funi 6599 to funid. |
⊢ Fun ( I ↾ 𝑉) | ||
Theorem | bj-opelidb 37134 |
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 37135 | Characterization of the ordered pair elements of the identity relation. Variant of bj-opelidb 37134 where only the sethood of the first component is expressed. (Contributed by BJ, 27-Dec-2023.) |
⊢ (〈𝐴, 𝐵〉 ∈ I ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵)) | ||
Theorem | bj-inexeqex 37136 | Lemma for bj-opelid 37138 (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 37137 | 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 4644 and elsn2g 4668 (which could be proved from it). (Contributed by BJ, 20-Jan-2024.) |
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-opelid 37138 | 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 37139 |
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 5864, or at least prove ideqg 5864 from it. |
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-ideqgALT 37140 | Alternate proof of bj-ideqg 37139 from brabga 5543 instead of bj-opelid 37138 itself proved from bj-opelidb 37134. (Contributed by BJ, 27-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-ideqb 37141 | Characterization of classes related by the identity relation. (Contributed by BJ, 24-Dec-2023.) |
⊢ (𝐴 I 𝐵 ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵)) | ||
Theorem | bj-idres 37142 |
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 6067 (see idinxpres 6066). See also elrid 6065 and elidinxp 6063. (Proof modification is discouraged.) |
⊢ ( I ↾ 𝐴) = ( I ∩ (𝐴 × 𝐴)) | ||
Theorem | bj-opelidres 37143 | 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 37144 from it. (Contributed by BJ, 29-Mar-2020.) |
⊢ (𝐴 ∈ 𝑉 → (〈𝐴, 𝐵〉 ∈ ( I ↾ 𝑉) ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-idreseq 37144 | Sufficient condition for the restricted identity relation to agree with equality. Note that the instance of bj-ideqg 37139 with V substituted for 𝑉 is a direct consequence of bj-idreseq 37144. This is a strengthening of resieq 6010 which should be proved from it (note that currently, resieq 6010 relies on ideq 5865). 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 37145 | Characterization for two classes to be related under the restricted identity relation. (Contributed by BJ, 24-Dec-2023.) |
⊢ (𝐴( I ↾ 𝐶)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵)) | ||
Theorem | bj-ideqg1 37146 |
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 37139 is in the main section. |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-ideqg1ALT 37147 |
Alternate proof of bj-ideqg1 using brabga 5543 instead of the "unbounded"
version bj-brab2a1 37131 or brab2a 5781. (Contributed by BJ, 25-Dec-2023.)
(Proof modification is discouraged.) (New usage is discouraged.)
TODO: delete once bj-ideqg 37139 is in the main section. |
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-opelidb1ALT 37148 | 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 37149 | Characterization of the couples in I whose first component is a setvar. (Contributed by BJ, 29-Mar-2020.) |
⊢ (〈𝑥, 𝐴〉 ∈ I ↔ 𝑥 = 𝐴) | ||
Theorem | bj-elid4 37150 | Characterization of the elements of I. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ (𝑉 × 𝑊) → (𝐴 ∈ I ↔ (1st ‘𝐴) = (2nd ‘𝐴))) | ||
Theorem | bj-elid5 37151 | Characterization of the elements of I. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ I ↔ (𝐴 ∈ (V × V) ∧ (1st ‘𝐴) = (2nd ‘𝐴))) | ||
Theorem | bj-elid6 37152 | Characterization of the elements of the diagonal of a Cartesian square. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐵 ∈ ( I ↾ 𝐴) ↔ (𝐵 ∈ (𝐴 × 𝐴) ∧ (1st ‘𝐵) = (2nd ‘𝐵))) | ||
Theorem | bj-elid7 37153 | 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 37155, it will probably be deleted. | ||
Syntax | cdiag2 37154 | Syntax for the diagonal of the Cartesian square of a set. |
class Id | ||
Definition | df-bj-diag 37155 |
Define the functionalized identity, which can also be seen as the diagonal
function. Its value is given in bj-diagval 37156 when it is viewed as the
functionalized identity, and in bj-diagval2 37157 when it is viewed as the
diagonal function.
Indeed, Definition df-br 5148 identifies a binary relation with the class of couples that are related by that binary relation (see eqrel2 38280 for the extensionality property of binary relations). As a consequence, the identity relation, or identity function (see funi 6599), 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 37155. 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 37156 | Value of the functionalized identity, or equivalently of the diagonal function. This expression views it as the functionalized identity, whereas bj-diagval2 37157 views it as the diagonal function. See df-bj-diag 37155 for the terminology. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ 𝑉 → (Id‘𝐴) = ( I ↾ 𝐴)) | ||
Theorem | bj-diagval2 37157 | Value of the functionalized identity, or equivalently of the diagonal function. This expression views it as the diagonal function, whereas bj-diagval 37156 views it as the functionalized identity. See df-bj-diag 37155 for the terminology. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ 𝑉 → (Id‘𝐴) = ( I ∩ (𝐴 × 𝐴))) | ||
Theorem | bj-eldiag 37158 | Characterization of the elements of the diagonal of a Cartesian square. Subsumed by bj-elid6 37152. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ (Id‘𝐴) ↔ (𝐵 ∈ (𝐴 × 𝐴) ∧ (1st ‘𝐵) = (2nd ‘𝐵)))) | ||
Theorem | bj-eldiag2 37159 | Characterization of the elements of the diagonal of a Cartesian square. Subsumed by bj-elid7 37153. (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 4606. | ||
Syntax | cimdir 37160 | Syntax for the functionalized direct image. |
class 𝒫* | ||
Definition | df-imdir 37161* | 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 37162* | Lemma for bj-imdirval 37163 and bj-iminvval 37175. (Contributed by BJ, 23-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ 𝜓)})) ⇒ ⊢ (𝜑 → (𝐴𝐶𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝜓)})) | ||
Theorem | bj-imdirval 37163* | Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴𝒫*𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ (𝑟 “ 𝑥) = 𝑦)})) | ||
Theorem | bj-imdirval2lem 37164* | Lemma for bj-imdirval2 37165 and bj-iminvval2 37176. (Contributed by BJ, 23-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝜓)} ∈ V) | ||
Theorem | bj-imdirval2 37165* | Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵)) ⇒ ⊢ (𝜑 → ((𝐴𝒫*𝐵)‘𝑅) = {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ (𝑅 “ 𝑥) = 𝑦)}) | ||
Theorem | bj-imdirval3 37166 | Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵)) ⇒ ⊢ (𝜑 → (𝑋((𝐴𝒫*𝐵)‘𝑅)𝑌 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐵) ∧ (𝑅 “ 𝑋) = 𝑌))) | ||
Theorem | bj-imdiridlem 37167* | Lemma for bj-imdirid 37168 and bj-iminvid 37177. (Contributed by BJ, 26-May-2024.) |
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝜑 ↔ 𝑥 = 𝑦)) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝜑)} = ( I ↾ 𝒫 𝐴) | ||
Theorem | bj-imdirid 37168 | Functorial property of the direct image: the direct image by the identity on a set is the identity on the powerset. (Contributed by BJ, 24-Dec-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐴𝒫*𝐴)‘( I ↾ 𝐴)) = ( I ↾ 𝒫 𝐴)) | ||
Theorem | bj-opelopabid 37169* | Membership in an ordered-pair class abstraction. One can remove the DV condition on 𝑥, 𝑦 by using opabid 5534 in place of opabidw 5533. (Contributed by BJ, 22-May-2024.) |
⊢ (𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ↔ 𝜑) | ||
Theorem | bj-opabco 37170* | Composition of ordered-pair class abstractions. (Contributed by BJ, 22-May-2024.) |
⊢ ({〈𝑦, 𝑧〉 ∣ 𝜓} ∘ {〈𝑥, 𝑦〉 ∣ 𝜑}) = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝜑 ∧ 𝜓)} | ||
Theorem | bj-xpcossxp 37171 | The composition of two Cartesian products is included in the expected Cartesian product. There is equality if (𝐵 ∩ 𝐶) ≠ ∅, see xpcogend 15009. (Contributed by BJ, 22-May-2024.) |
⊢ ((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐷) | ||
Theorem | bj-imdirco 37172 | Functorial property of the direct image: the direct image by a composition is the composition of the direct images. (Contributed by BJ, 23-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵)) & ⊢ (𝜑 → 𝑆 ⊆ (𝐵 × 𝐶)) ⇒ ⊢ (𝜑 → ((𝐴𝒫*𝐶)‘(𝑆 ∘ 𝑅)) = (((𝐵𝒫*𝐶)‘𝑆) ∘ ((𝐴𝒫*𝐵)‘𝑅))) | ||
Syntax | ciminv 37173 | Syntax for the functionalized inverse image. |
class 𝒫* | ||
Definition | df-iminv 37174* | Definition of the functionalized inverse image, which maps a binary relation between two given sets to its associated inverse image relation. (Contributed by BJ, 23-Dec-2023.) |
⊢ 𝒫* = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ 𝑥 = (◡𝑟 “ 𝑦))})) | ||
Theorem | bj-iminvval 37175* | Value of the functionalized inverse image. (Contributed by BJ, 23-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴𝒫*𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝑥 = (◡𝑟 “ 𝑦))})) | ||
Theorem | bj-iminvval2 37176* | Value of the functionalized inverse image. (Contributed by BJ, 23-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵)) ⇒ ⊢ (𝜑 → ((𝐴𝒫*𝐵)‘𝑅) = {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝑥 = (◡𝑅 “ 𝑦))}) | ||
Theorem | bj-iminvid 37177 | Functorial property of the inverse image: the inverse image by the identity on a set is the identity on the powerset. (Contributed by BJ, 26-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐴𝒫*𝐴)‘( I ↾ 𝐴)) = ( I ↾ 𝒫 𝐴)) | ||
We parameterize the set of infinite extended complex numbers ℂ∞ (df-bj-ccinfty 37194) using the real numbers ℝ (df-r 11162) via the function +∞eiτ. Since at that point, we have only defined the set of real numbers but no operations on it, we define a temporary "fractional part" function, which is more convenient to define on the temporary reals R (df-nr 11093) since we can use operations on the latter. We also define the temporary real "one-half" in order to define minus infinity (df-bj-minfty 37206) and then we can define the sets of extended real numbers and of extended complex numbers, and the projective real and complex lines, as well as addition and negation on these, and also the order relation on the extended reals (which bypasses the intermediate definition of a temporary order on the real numbers and then a superseding one on the extended real numbers). | ||
Syntax | cfractemp 37178 | Syntax for the fractional part of a temporary real. |
class {R | ||
Definition | df-bj-fractemp 37179* |
Temporary definition: fractional part of a temporary real.
To understand this definition, recall the canonical injection ω⟶R, 𝑛 ↦ [{𝑥 ∈ Q ∣ 𝑥 <Q 〈suc 𝑛, 1o〉}, 1P] ~R where we successively take the successor of 𝑛 to land in positive integers, then take the couple with 1o as second component to land in positive rationals, then take the Dedekind cut that positive rational forms, and finally take the equivalence class of the couple with 1P as second component. Adding one at the beginning and subtracting it at the end is necessary since the constructions used in set.mm use the positive integers, positive rationals, and positive reals as intermediate number systems. (Contributed by BJ, 22-Jan-2023.) The precise definition is irrelevant and should generally not be used. One could even inline it. The definitive fractional part of an extended or projective complex number will be defined later. (New usage is discouraged.) |
⊢ {R = (𝑥 ∈ R ↦ (℩𝑦 ∈ R ((𝑦 = 0R ∨ (0R <R 𝑦 ∧ 𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([〈{𝑧 ∈ Q ∣ 𝑧 <Q 〈suc 𝑛, 1o〉}, 1P〉] ~R +R 𝑦) = 𝑥))) | ||
Syntax | cinftyexpitau 37180 | Syntax for the function +∞eiτ parameterizing ℂ∞. |
class +∞eiτ | ||
Definition | df-bj-inftyexpitau 37181 | Definition of the auxiliary function +∞eiτ parameterizing the circle at infinity ℂ∞ in ℂ̅. We use coupling with {R} to simplify the proof of bj-inftyexpitaudisj 37187. (Contributed by BJ, 22-Jan-2023.) The precise definition is irrelevant and should generally not be used. TODO: prove only the necessary lemmas to prove ⊢ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((+∞eiτ‘𝐴) = (+∞eiτ‘𝐵) ↔ (𝐴 − 𝐵) ∈ ℤ)). (New usage is discouraged.) |
⊢ +∞eiτ = (𝑥 ∈ ℝ ↦ 〈({R‘(1st ‘𝑥)), {R}〉) | ||
Syntax | cccinftyN 37182 | Syntax for the circle at infinity ℂ∞N. |
class ℂ∞N | ||
Definition | df-bj-ccinftyN 37183 | Definition of the circle at infinity ℂ∞N. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.) |
⊢ ℂ∞N = ran +∞eiτ | ||
Theorem | bj-inftyexpitaufo 37184 | The function +∞eiτ written as a surjection with domain and range. (Contributed by BJ, 4-Feb-2023.) |
⊢ +∞eiτ:ℝ–onto→ℂ∞N | ||
Syntax | chalf 37185 | Syntax for the temporary one-half. |
class 1/2 | ||
Definition | df-bj-onehalf 37186 |
Define the temporary real "one-half". Once the machinery is
developed,
the real number "one-half" is commonly denoted by (1 / 2).
(Contributed by BJ, 4-Feb-2023.) (New usage is discouraged.)
TODO: $p |- 1/2 e. R. $= ? $. (riotacl 7404) $p |- -. 0R = 1/2 $= ? $. (since -. ( 0R +R 0R ) = 1R ) $p |- 0R <R 1/2 $= ? $. $p |- 1/2 <R 1R $= ? $. $p |- ( {R ` 0R ) = 0R $= ? $. $p |- ( {R ` 1/2 ) = 1/2 $= ? $. df-minfty $a |- minfty = ( inftyexpitau ` <. 1/2 , 0R >. ) $. |
⊢ 1/2 = (℩𝑥 ∈ R (𝑥 +R 𝑥) = 1R) | ||
Theorem | bj-inftyexpitaudisj 37187 | An element of the circle at infinity is not a complex number. (Contributed by BJ, 4-Feb-2023.) |
⊢ ¬ (+∞eiτ‘𝐴) ∈ ℂ | ||
Syntax | cinftyexpi 37188 | Syntax for the function +∞ei parameterizing ℂ∞. |
class +∞ei | ||
Definition | df-bj-inftyexpi 37189 | Definition of the auxiliary function +∞ei parameterizing the circle at infinity ℂ∞ in ℂ̅. We use coupling with ℂ to simplify the proof of bj-ccinftydisj 37195. It could seem more natural to define +∞ei on all of ℝ, but we want to use only basic functions in the definition of ℂ̅. TODO: transition to df-bj-inftyexpitau 37181 instead. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.) |
⊢ +∞ei = (𝑥 ∈ (-π(,]π) ↦ 〈𝑥, ℂ〉) | ||
Theorem | bj-inftyexpiinv 37190 | Utility theorem for the inverse of +∞ei. (Contributed by BJ, 22-Jun-2019.) This utility theorem is irrelevant and should generally not be used. (New usage is discouraged.) |
⊢ (𝐴 ∈ (-π(,]π) → (1st ‘(+∞ei‘𝐴)) = 𝐴) | ||
Theorem | bj-inftyexpiinj 37191 | Injectivity of the parameterization +∞ei. Remark: a more conceptual proof would use bj-inftyexpiinv 37190 and the fact that a function with a retraction is injective. (Contributed by BJ, 22-Jun-2019.) |
⊢ ((𝐴 ∈ (-π(,]π) ∧ 𝐵 ∈ (-π(,]π)) → (𝐴 = 𝐵 ↔ (+∞ei‘𝐴) = (+∞ei‘𝐵))) | ||
Theorem | bj-inftyexpidisj 37192 | An element of the circle at infinity is not a complex number. (Contributed by BJ, 22-Jun-2019.) This utility theorem is irrelevant and should generally not be used. (New usage is discouraged.) |
⊢ ¬ (+∞ei‘𝐴) ∈ ℂ | ||
Syntax | cccinfty 37193 | Syntax for the circle at infinity ℂ∞. |
class ℂ∞ | ||
Definition | df-bj-ccinfty 37194 | Definition of the circle at infinity ℂ∞. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.) |
⊢ ℂ∞ = ran +∞ei | ||
Theorem | bj-ccinftydisj 37195 | The circle at infinity is disjoint from the set of complex numbers. (Contributed by BJ, 22-Jun-2019.) |
⊢ (ℂ ∩ ℂ∞) = ∅ | ||
Theorem | bj-elccinfty 37196 | A lemma for infinite extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
⊢ (𝐴 ∈ (-π(,]π) → (+∞ei‘𝐴) ∈ ℂ∞) | ||
Syntax | cccbar 37197 | Syntax for the set of extended complex numbers ℂ̅. |
class ℂ̅ | ||
Definition | df-bj-ccbar 37198 | Definition of the set of extended complex numbers ℂ̅. (Contributed by BJ, 22-Jun-2019.) |
⊢ ℂ̅ = (ℂ ∪ ℂ∞) | ||
Theorem | bj-ccssccbar 37199 | Complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℂ ⊆ ℂ̅ | ||
Theorem | bj-ccinftyssccbar 37200 | Infinite extended complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℂ∞ ⊆ ℂ̅ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |