P. 372 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37101-37200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-ismoored0 37101	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝐴 ∈ Moore → ∪ 𝐴 ∈ 𝐴)
Theorem	bj-ismoored 37102	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ Moore)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (∪ 𝐴 ∩ ∩ 𝐵) ∈ 𝐴)
Theorem	bj-ismoored2 37103	Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ Moore)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → ∩ 𝐵 ∈ 𝐴)
Theorem	bj-ismooredr 37104*	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 37105*	Sufficient condition to be a Moore collection (variant of bj-ismooredr 37104 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 37106	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 37107	The empty set is not a Moore collection. (Contributed by BJ, 9-Dec-2021.)
⊢ ¬ ∅ ∈ Moore
Theorem	bj-snmoore 37108	A singleton is a Moore collection. See bj-snmooreb 37109 for a biconditional version. (Contributed by BJ, 10-Apr-2024.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Moore)
Theorem	bj-snmooreb 37109	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 37110	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 37108). 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)
21.19.5.23  Maps-to notation for functions with three arguments
Theorem	bj-0nelmpt 37111	The empty set is not an element of a function (given in maps-to notation). (Contributed by BJ, 30-Dec-2020.)
⊢ ¬ ∅ ∈ (𝑥 ∈ 𝐴 ↦ 𝐵)
Theorem	bj-mptval 37112	Value of a function given in maps-to notation. (Contributed by BJ, 30-Dec-2020.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑋 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑋) = 𝑌 ↔ 𝑋(𝑥 ∈ 𝐴 ↦ 𝐵)𝑌)))
Theorem	bj-dfmpoa 37113*	An equivalent definition of df-mpo 7395. (Contributed by BJ, 30-Dec-2020.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨𝑠, 𝑡⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑠 = ⟨𝑥, 𝑦⟩ ∧ 𝑡 = 𝐶)}
Theorem	bj-mpomptALT 37114*	Alternate proof of mpompt 7506. (Contributed by BJ, 30-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)    ⇒   ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
Syntax	cmpt3 37115	Syntax for maps-to notation for functions with three arguments.
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷)
Definition	df-bj-mpt3 37116*	Define maps-to notation for functions with three arguments. See df-mpt 5192 and df-mpo 7395 for functions with one and two arguments respectively. This definition is analogous to bj-dfmpoa 37113. (Contributed by BJ, 11-Apr-2020.)
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) = {⟨𝑠, 𝑡⟩ ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑠 = ⟨𝑥, 𝑦, 𝑧⟩ ∧ 𝑡 = 𝐷)}
21.19.5.24  Currying Currying and uncurrying. See also df-cur 8249 and df-unc 8250. Contrary to these, the definitions in this section are parameterized.
Syntax	csethom 37117	Syntax for the set of set morphisms.
class Set⟶
Definition	df-bj-sethom 37118*	Define the set of functions (morphisms of sets) between two sets. Same as df-map 8804 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 37119	Syntax for the set of topological morphisms.
class Top⟶
Definition	df-bj-tophom 37120*	Define the set of continuous functions (morphisms of topological spaces) between two topological spaces. Similar to df-cn 23121 (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 37121	Syntax for the set of magma morphisms.
class Mgm⟶
Definition	df-bj-mgmhom 37122*	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 37123	Syntax for the set of topological magma morphisms.
class TopMgm⟶
Definition	df-bj-topmgmhom 37124*	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- 37125	Syntax for the parameterized currying function.
class curry_
Definition	df-bj-cur 37126*	Define currying. See also df-cur 8249. (Contributed by BJ, 11-Apr-2020.)
⊢ curry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ ((𝑥 × 𝑦) Set⟶ 𝑧) ↦ (𝑎 ∈ 𝑥 ↦ (𝑏 ∈ 𝑦 ↦ (𝑓‘⟨𝑎, 𝑏⟩)))))
Syntax	cunc- 37127	Notation for the parameterized uncurrying function.
class uncurry_
Definition	df-bj-unc 37128*	Define uncurrying. See also df-unc 8250. (Contributed by BJ, 11-Apr-2020.)
⊢ uncurry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ (𝑥 Set⟶ (𝑦 Set⟶ 𝑧)) ↦ (𝑎 ∈ 𝑥, 𝑏 ∈ 𝑦 ↦ ((𝑓‘𝑎)‘𝑏))))
21.19.5.25  Setting components of extensible structures 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 37129	Syntax for component-setting in extensible structures.
class [𝐵 / 𝐴]struct𝑆
Definition	df-strset 37130	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 17141, but since extensible structures are functions on ℕ, it will be more natural to replace it with ℕ when df-strset 37130 becomes the main definition. (Contributed by BJ, 13-Feb-2022.)
⊢ [𝐵 / 𝐴]struct𝑆 = ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {⟨(𝐴‘ndx), 𝐵⟩})
Theorem	setsstrset 37131	Relation between df-sets 17141 and df-strset 37130. Temporary theorem kept during the transition from the former to the latter. (Contributed by BJ, 13-Feb-2022.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → [𝐵 / 𝐴]struct𝑆 = (𝑆 sSet ⟨(𝐴‘ndx), 𝐵⟩))
21.19.6  Extended real and complex numbers, real and complex projective lines 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 37228 and df-bj-rrhat 37230, and the point at infinity is denoted by ∞, defined in df-bj-infty 37226. Both ℝ and ℂ also have "directional compactifications", denoted respectively by ℝ̅, defined in df-bj-rrbar 37224 (already defined as ℝ*, see df-xr 11219) and ℂ̅, defined in df-bj-ccbar 37211. 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.
21.19.6.1  Complements on class abstractions of ordered pairs and binary relations
Theorem	bj-nfald 37132	Variant of nfald 2327. (Contributed by BJ, 25-Dec-2023.)
⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓)
Theorem	bj-nfexd 37133	Variant of nfexd 2328. (Contributed by BJ, 25-Dec-2023.)
⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓)
Theorem	copsex2d 37134*	Implicit substitution deduction for ordered pairs. (Contributed by BJ, 25-Dec-2023.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → Ⅎ𝑦𝜒)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ 𝜒))
Theorem	copsex2b 37135*	Biconditional form of copsex2d 37134. TODO: prove a relative version, that is, with ∃𝑥 ∈ 𝑉∃𝑦 ∈ 𝑊...(𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊). (Contributed by BJ, 27-Dec-2023.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → Ⅎ𝑦𝜒)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒)))
Theorem	opelopabd 37136*	Membership of an ordere pair in a class abstraction of ordered pairs. (Contributed by BJ, 17-Dec-2023.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → Ⅎ𝑦𝜒)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ 𝜒))
Theorem	opelopabb 37137*	Membership of an ordered pair in a class abstraction of ordered pairs, biconditional form. (Contributed by BJ, 17-Dec-2023.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → Ⅎ𝑦𝜒)    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒)))
Theorem	opelopabbv 37138*	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 37139	The coordinates of an ordered pair that belongs to a relation are sets. TODO: Slightly shorter than brrelex12 5693, which could be proved from it. (Contributed by BJ, 27-Dec-2023.)
⊢ ((Rel 𝑅 ∧ ⟨𝐴, 𝐵⟩ ∈ 𝑅) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	bj-opelresdm 37140	If an ordered pair is in a restricted binary relation, then its first component is an element of the restricting class. See also opelres 5959. (Contributed by BJ, 25-Dec-2023.)
⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑅 ↾ 𝑋) → 𝐴 ∈ 𝑋)
Theorem	bj-brresdm 37141	If two classes are related by a restricted binary relation, then the first class is an element of the restricting class. See also brres 5960 and brrelex1 5694. Remark: there are many pairs like bj-opelresdm 37140 / bj-brresdm 37141, where one uses membership of ordered pairs and the other, related classes (for instance, bj-opelresdm 37140 / brrelex12 5693 or the opelopabg 5501 / brabg 5502 family). They are straightforwardly equivalent by df-br 5111. 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 37142*	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 37143*	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 37144*	"Unbounded" version of brab2a 5735. (Contributed by BJ, 25-Dec-2023.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝐴𝑅𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜓))
21.19.6.2  Identity relation (complements) Complements on the identity relation.
Theorem	bj-opabssvv 37145*	A variant of relopabiv 5786 (which could be proved from it, similarly to relxp 5659 from xpss 5657). (Contributed by BJ, 28-Dec-2023.)
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ (V × V)
Theorem	bj-funidres 37146	The restricted identity relation is a function. (Contributed by BJ, 27-Dec-2023.) TODO: relabel funi 6551 to funid.
⊢ Fun ( I ↾ 𝑉)
Theorem	bj-opelidb 37147	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 37148	Characterization of the ordered pair elements of the identity relation. Variant of bj-opelidb 37147 where only the sethood of the first component is expressed. (Contributed by BJ, 27-Dec-2023.)
⊢ (⟨𝐴, 𝐵⟩ ∈ I ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵))
Theorem	bj-inexeqex 37149	Lemma for bj-opelid 37151 (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 37150	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 4606 and elsn2g 4631 (which could be proved from it). (Contributed by BJ, 20-Jan-2024.)
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
Theorem	bj-opelid 37151	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 37152	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 5818, or at least prove ideqg 5818 from it.
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
Theorem	bj-ideqgALT 37153	Alternate proof of bj-ideqg 37152 from brabga 5497 instead of bj-opelid 37151 itself proved from bj-opelidb 37147. (Contributed by BJ, 27-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
Theorem	bj-ideqb 37154	Characterization of classes related by the identity relation. (Contributed by BJ, 24-Dec-2023.)
⊢ (𝐴 I 𝐵 ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵))
Theorem	bj-idres 37155	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 6022 (see idinxpres 6021). See also elrid 6020 and elidinxp 6018. (Proof modification is discouraged.)
⊢ ( I ↾ 𝐴) = ( I ∩ (𝐴 × 𝐴))
Theorem	bj-opelidres 37156	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 37157 from it. (Contributed by BJ, 29-Mar-2020.)
⊢ (𝐴 ∈ 𝑉 → (⟨𝐴, 𝐵⟩ ∈ ( I ↾ 𝑉) ↔ 𝐴 = 𝐵))
Theorem	bj-idreseq 37157	Sufficient condition for the restricted identity relation to agree with equality. Note that the instance of bj-ideqg 37152 with V substituted for 𝑉 is a direct consequence of bj-idreseq 37157. This is a strengthening of resieq 5964 which should be proved from it (note that currently, resieq 5964 relies on ideq 5819). 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 37158	Characterization for two classes to be related under the restricted identity relation. (Contributed by BJ, 24-Dec-2023.)
⊢ (𝐴( I ↾ 𝐶)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵))
Theorem	bj-ideqg1 37159	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 37152 is in the main section.
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
Theorem	bj-ideqg1ALT 37160	Alternate proof of bj-ideqg1 using brabga 5497 instead of the "unbounded" version bj-brab2a1 37144 or brab2a 5735. (Contributed by BJ, 25-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.) TODO: delete once bj-ideqg 37152 is in the main section.
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
Theorem	bj-opelidb1ALT 37161	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 37162	Characterization of the couples in I whose first component is a setvar. (Contributed by BJ, 29-Mar-2020.)
⊢ (⟨𝑥, 𝐴⟩ ∈ I ↔ 𝑥 = 𝐴)
Theorem	bj-elid4 37163	Characterization of the elements of I. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐴 ∈ (𝑉 × 𝑊) → (𝐴 ∈ I ↔ (1st ‘𝐴) = (2nd ‘𝐴)))
Theorem	bj-elid5 37164	Characterization of the elements of I. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐴 ∈ I ↔ (𝐴 ∈ (V × V) ∧ (1st ‘𝐴) = (2nd ‘𝐴)))
Theorem	bj-elid6 37165	Characterization of the elements of the diagonal of a Cartesian square. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐵 ∈ ( I ↾ 𝐴) ↔ (𝐵 ∈ (𝐴 × 𝐴) ∧ (1st ‘𝐵) = (2nd ‘𝐵)))
Theorem	bj-elid7 37166	Characterization of the elements of the diagonal of a Cartesian square. (Contributed by BJ, 22-Jun-2019.)
⊢ (⟨𝐵, 𝐶⟩ ∈ ( I ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶))
21.19.6.3  Functionalized identity (diagonal in a Cartesian square) 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 37168, it will probably be deleted.
Syntax	cdiag2 37167	Syntax for the diagonal of the Cartesian square of a set.
class Id
Definition	df-bj-diag 37168	Define the functionalized identity, which can also be seen as the diagonal function. Its value is given in bj-diagval 37169 when it is viewed as the functionalized identity, and in bj-diagval2 37170 when it is viewed as the diagonal function. Indeed, Definition df-br 5111 identifies a binary relation with the class of couples that are related by that binary relation (see eqrel2 38294 for the extensionality property of binary relations). As a consequence, the identity relation, or identity function (see funi 6551), 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 37168. 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 37169	Value of the functionalized identity, or equivalently of the diagonal function. This expression views it as the functionalized identity, whereas bj-diagval2 37170 views it as the diagonal function. See df-bj-diag 37168 for the terminology. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐴 ∈ 𝑉 → (Id‘𝐴) = ( I ↾ 𝐴))
Theorem	bj-diagval2 37170	Value of the functionalized identity, or equivalently of the diagonal function. This expression views it as the diagonal function, whereas bj-diagval 37169 views it as the functionalized identity. See df-bj-diag 37168 for the terminology. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐴 ∈ 𝑉 → (Id‘𝐴) = ( I ∩ (𝐴 × 𝐴)))
Theorem	bj-eldiag 37171	Characterization of the elements of the diagonal of a Cartesian square. Subsumed by bj-elid6 37165. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ (Id‘𝐴) ↔ (𝐵 ∈ (𝐴 × 𝐴) ∧ (1st ‘𝐵) = (2nd ‘𝐵))))
Theorem	bj-eldiag2 37172	Characterization of the elements of the diagonal of a Cartesian square. Subsumed by bj-elid7 37166. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐴 ∈ 𝑉 → (⟨𝐵, 𝐶⟩ ∈ (Id‘𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶)))
21.19.6.4  Direct image and inverse image 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 4568.
Syntax	cimdir 37173	Syntax for the functionalized direct image.
class 𝒫*
Definition	df-imdir 37174*	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 37175*	Lemma for bj-imdirval 37176 and bj-iminvval 37188. (Contributed by BJ, 23-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ 𝜓)}))    ⇒   ⊢ (𝜑 → (𝐴𝐶𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝜓)}))
Theorem	bj-imdirval 37176*	Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴𝒫*𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ (𝑟 “ 𝑥) = 𝑦)}))
Theorem	bj-imdirval2lem 37177*	Lemma for bj-imdirval2 37178 and bj-iminvval2 37189. (Contributed by BJ, 23-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝜓)} ∈ V)
Theorem	bj-imdirval2 37178*	Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵))    ⇒   ⊢ (𝜑 → ((𝐴𝒫*𝐵)‘𝑅) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ (𝑅 “ 𝑥) = 𝑦)})
Theorem	bj-imdirval3 37179	Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵))    ⇒   ⊢ (𝜑 → (𝑋((𝐴𝒫*𝐵)‘𝑅)𝑌 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐵) ∧ (𝑅 “ 𝑋) = 𝑌)))
Theorem	bj-imdiridlem 37180*	Lemma for bj-imdirid 37181 and bj-iminvid 37190. (Contributed by BJ, 26-May-2024.)
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝜑 ↔ 𝑥 = 𝑦))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝜑)} = ( I ↾ 𝒫 𝐴)
Theorem	bj-imdirid 37181	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 37182*	Membership in an ordered-pair class abstraction. One can remove the DV condition on 𝑥, 𝑦 by using opabid 5488 in place of opabidw 5487. (Contributed by BJ, 22-May-2024.)
⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦 ↔ 𝜑)
Theorem	bj-opabco 37183*	Composition of ordered-pair class abstractions. (Contributed by BJ, 22-May-2024.)
⊢ ({⟨𝑦, 𝑧⟩ ∣ 𝜓} ∘ {⟨𝑥, 𝑦⟩ ∣ 𝜑}) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝜑 ∧ 𝜓)}
Theorem	bj-xpcossxp 37184	The composition of two Cartesian products is included in the expected Cartesian product. There is equality if (𝐵 ∩ 𝐶) ≠ ∅, see xpcogend 14947. (Contributed by BJ, 22-May-2024.)
⊢ ((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐷)
Theorem	bj-imdirco 37185	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 37186	Syntax for the functionalized inverse image.
class 𝒫*
Definition	df-iminv 37187*	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 37188*	Value of the functionalized inverse image. (Contributed by BJ, 23-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴𝒫*𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝑥 = (◡𝑟 “ 𝑦))}))
Theorem	bj-iminvval2 37189*	Value of the functionalized inverse image. (Contributed by BJ, 23-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵))    ⇒   ⊢ (𝜑 → ((𝐴𝒫*𝐵)‘𝑅) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝑥 = (◡𝑅 “ 𝑦))})
Theorem	bj-iminvid 37190	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 ↾ 𝒫 𝐴))
21.19.6.5  Extended numbers and projective lines as sets We parameterize the set of infinite extended complex numbers ℂ∞ (df-bj-ccinfty 37207) using the real numbers ℝ (df-r 11085) 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 11016) 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 37219) 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 37191	Syntax for the fractional part of a temporary real.
class {R
Definition	df-bj-fractemp 37192*	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 37193	Syntax for the function +∞eiτ parameterizing ℂ∞.
class +∞eiτ
Definition	df-bj-inftyexpitau 37194	Definition of the auxiliary function +∞eiτ parameterizing the circle at infinity ℂ∞ in ℂ̅. We use coupling with {R} to simplify the proof of bj-inftyexpitaudisj 37200. (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 37195	Syntax for the circle at infinity ℂ∞N.
class ℂ∞N
Definition	df-bj-ccinftyN 37196	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 37197	The function +∞eiτ written as a surjection with domain and range. (Contributed by BJ, 4-Feb-2023.)
⊢ +∞eiτ:ℝ–onto→ℂ∞N
Syntax	chalf 37198	Syntax for the temporary one-half.
class 1/2
Definition	df-bj-onehalf 37199	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 7364) $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 37200	An element of the circle at infinity is not a complex number. (Contributed by BJ, 4-Feb-2023.)
⊢ ¬ (+∞eiτ‘𝐴) ∈ ℂ