P. 377 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37601-37700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-opelresdm 37601	If an ordered pair is in a restricted binary relation, then its first component is an element of the restricting class. See also opelres 5969. (Contributed by BJ, 25-Dec-2023.)
⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑅 ↾ 𝑋) → 𝐴 ∈ 𝑋)
Theorem	bj-brresdm 37602	If two classes are related by a restricted binary relation, then the first class is an element of the restricting class. See also brres 5970 and brrelex1 5698. Remark: there are many pairs like bj-opelresdm 37601 / bj-brresdm 37602, where one uses membership of ordered pairs and the other, related classes (for instance, bj-opelresdm 37601 / brrelex12 5697 or the opelopabg 5507 / brabg 5508 family). They are straightforwardly equivalent by df-br 5100. 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 37603*	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 37604*	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 37605*	"Unbounded" version of brab2a 5738. (Contributed by BJ, 25-Dec-2023.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝐴𝑅𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜓))
21.19.6.2  Identity relation (complements) Complements on the identity relation.
Theorem	bj-opabssvv 37606*	A variant of relopabiv 5791 (which could be proved from it, similarly to relxp 5663 from xpss 5661). (Contributed by BJ, 28-Dec-2023.)
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ (V × V)
Theorem	bj-funidres 37607	The restricted identity relation is a function. (Contributed by BJ, 27-Dec-2023.) TODO: relabel funi 6549 to funid.
⊢ Fun ( I ↾ 𝑉)
Theorem	bj-opelidb 37608	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 37609	Characterization of the ordered pair elements of the identity relation. Variant of bj-opelidb 37608 where only the sethood of the first component is expressed. (Contributed by BJ, 27-Dec-2023.)
⊢ (⟨𝐴, 𝐵⟩ ∈ I ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵))
Theorem	bj-inexeqex 37610	Lemma for bj-opelid 37612 (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 37611	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 4595 and elsn2g 4622 (which could be proved from it). (Contributed by BJ, 20-Jan-2024.)
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
Theorem	bj-opelid 37612	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 37613	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 5821, or at least prove ideqg 5821 from it.
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
Theorem	bj-ideqgALT 37614	Alternate proof of bj-ideqg 37613 from brabga 5503 instead of bj-opelid 37612 itself proved from bj-opelidb 37608. (Contributed by BJ, 27-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
Theorem	bj-ideqb 37615	Characterization of classes related by the identity relation. (Contributed by BJ, 24-Dec-2023.)
⊢ (𝐴 I 𝐵 ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵))
Theorem	bj-idres 37616	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 6034 (see idinxpres 6033). See also elrid 6032 and elidinxp 6030. (Proof modification is discouraged.)
⊢ ( I ↾ 𝐴) = ( I ∩ (𝐴 × 𝐴))
Theorem	bj-opelidres 37617	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 37618 from it. (Contributed by BJ, 29-Mar-2020.)
⊢ (𝐴 ∈ 𝑉 → (⟨𝐴, 𝐵⟩ ∈ ( I ↾ 𝑉) ↔ 𝐴 = 𝐵))
Theorem	bj-idreseq 37618	Sufficient condition for the restricted identity relation to agree with equality. Note that the instance of bj-ideqg 37613 with V substituted for 𝑉 is a direct consequence of bj-idreseq 37618. This is a strengthening of resieq 5974 which should be proved from it (note that currently, resieq 5974 relies on ideq 5822). 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 37619	Characterization for two classes to be related under the restricted identity relation. (Contributed by BJ, 24-Dec-2023.)
⊢ (𝐴( I ↾ 𝐶)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐴 = 𝐵))
Theorem	bj-ideqg1 37620	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 37613 is in the main section.
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
Theorem	bj-ideqg1ALT 37621	Alternate proof of bj-ideqg1 using brabga 5503 instead of the "unbounded" version bj-brab2a1 37605 or brab2a 5738. (Contributed by BJ, 25-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.) TODO: delete once bj-ideqg 37613 is in the main section.
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵))
Theorem	bj-opelidb1ALT 37622	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 37623	Characterization of the couples in I whose first component is a setvar. (Contributed by BJ, 29-Mar-2020.)
⊢ (⟨𝑥, 𝐴⟩ ∈ I ↔ 𝑥 = 𝐴)
Theorem	bj-elid4 37624	Characterization of the elements of I. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐴 ∈ (𝑉 × 𝑊) → (𝐴 ∈ I ↔ (1st ‘𝐴) = (2nd ‘𝐴)))
Theorem	bj-elid5 37625	Characterization of the elements of I. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐴 ∈ I ↔ (𝐴 ∈ (V × V) ∧ (1st ‘𝐴) = (2nd ‘𝐴)))
Theorem	bj-elid6 37626	Characterization of the elements of the diagonal of a Cartesian square. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐵 ∈ ( I ↾ 𝐴) ↔ (𝐵 ∈ (𝐴 × 𝐴) ∧ (1st ‘𝐵) = (2nd ‘𝐵)))
Theorem	bj-elid7 37627	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 37629, it will probably be deleted.
Syntax	cdiag2 37628	Syntax for the diagonal of the Cartesian square of a set.
class Id
Definition	df-bj-diag 37629	Define the functionalized identity, which can also be seen as the diagonal function. Its value is given in bj-diagval 37630 when it is viewed as the functionalized identity, and in bj-diagval2 37631 when it is viewed as the diagonal function. Indeed, Definition df-br 5100 identifies a binary relation with the class of couples that are related by that binary relation (see eqrel2 38768 for the extensionality property of binary relations). As a consequence, the identity relation, or identity function (see funi 6549), 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 37629. 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 37630	Value of the functionalized identity, or equivalently of the diagonal function. This expression views it as the functionalized identity, whereas bj-diagval2 37631 views it as the diagonal function. See df-bj-diag 37629 for the terminology. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐴 ∈ 𝑉 → (Id‘𝐴) = ( I ↾ 𝐴))
Theorem	bj-diagval2 37631	Value of the functionalized identity, or equivalently of the diagonal function. This expression views it as the diagonal function, whereas bj-diagval 37630 views it as the functionalized identity. See df-bj-diag 37629 for the terminology. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐴 ∈ 𝑉 → (Id‘𝐴) = ( I ∩ (𝐴 × 𝐴)))
Theorem	bj-eldiag 37632	Characterization of the elements of the diagonal of a Cartesian square. Subsumed by bj-elid6 37626. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ (Id‘𝐴) ↔ (𝐵 ∈ (𝐴 × 𝐴) ∧ (1st ‘𝐵) = (2nd ‘𝐵))))
Theorem	bj-eldiag2 37633	Characterization of the elements of the diagonal of a Cartesian square. Subsumed by bj-elid7 37627. (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 4556.
Syntax	cimdir 37634	Syntax for the functionalized direct image.
class 𝒫*
Definition	df-imdir 37635*	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 37636*	Lemma for bj-imdirval 37637 and bj-iminvval 37649. (Contributed by BJ, 23-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ 𝜓)}))    ⇒   ⊢ (𝜑 → (𝐴𝐶𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝜓)}))
Theorem	bj-imdirval 37637*	Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴𝒫*𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ (𝑟 “ 𝑥) = 𝑦)}))
Theorem	bj-imdirval2lem 37638*	Lemma for bj-imdirval2 37639 and bj-iminvval2 37650. (Contributed by BJ, 23-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝜓)} ∈ V)
Theorem	bj-imdirval2 37639*	Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵))    ⇒   ⊢ (𝜑 → ((𝐴𝒫*𝐵)‘𝑅) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ (𝑅 “ 𝑥) = 𝑦)})
Theorem	bj-imdirval3 37640	Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵))    ⇒   ⊢ (𝜑 → (𝑋((𝐴𝒫*𝐵)‘𝑅)𝑌 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐵) ∧ (𝑅 “ 𝑋) = 𝑌)))
Theorem	bj-imdiridlem 37641*	Lemma for bj-imdirid 37642 and bj-iminvid 37651. (Contributed by BJ, 26-May-2024.)
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝜑 ↔ 𝑥 = 𝑦))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝜑)} = ( I ↾ 𝒫 𝐴)
Theorem	bj-imdirid 37642	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 37643*	Membership in an ordered-pair class abstraction. One can remove the DV condition on 𝑥, 𝑦 by using opabid 5494 in place of opabidw 5493. (Contributed by BJ, 22-May-2024.)
⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦 ↔ 𝜑)
Theorem	bj-opabco 37644*	Composition of ordered-pair class abstractions. (Contributed by BJ, 22-May-2024.)
⊢ ({⟨𝑦, 𝑧⟩ ∣ 𝜓} ∘ {⟨𝑥, 𝑦⟩ ∣ 𝜑}) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝜑 ∧ 𝜓)}
Theorem	bj-xpcossxp 37645	The composition of two Cartesian products is included in the expected Cartesian product. There is equality if (𝐵 ∩ 𝐶) ≠ ∅, see xpcogend 14984. (Contributed by BJ, 22-May-2024.)
⊢ ((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐷)
Theorem	bj-imdirco 37646	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 37647	Syntax for the functionalized inverse image.
class 𝒫*
Definition	df-iminv 37648*	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 37649*	Value of the functionalized inverse image. (Contributed by BJ, 23-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴𝒫*𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝑥 = (◡𝑟 “ 𝑦))}))
Theorem	bj-iminvval2 37650*	Value of the functionalized inverse image. (Contributed by BJ, 23-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵))    ⇒   ⊢ (𝜑 → ((𝐴𝒫*𝐵)‘𝑅) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝑥 = (◡𝑅 “ 𝑦))})
Theorem	bj-iminvid 37651	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 37668) using the real numbers ℝ (df-r 11080) 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 11011) 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 37680) 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 37652	Syntax for the fractional part of a temporary real.
class {R
Definition	df-bj-fractemp 37653*	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 37654	Syntax for the function +∞eiτ parameterizing ℂ∞.
class +∞eiτ
Definition	df-bj-inftyexpitau 37655	Definition of the auxiliary function +∞eiτ parameterizing the circle at infinity ℂ∞ in ℂ̅. We use coupling with {R} to simplify the proof of bj-inftyexpitaudisj 37661. (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 37656	Syntax for the circle at infinity ℂ∞N.
class ℂ∞N
Definition	df-bj-ccinftyN 37657	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 37658	The function +∞eiτ written as a surjection with domain and range. (Contributed by BJ, 4-Feb-2023.)
⊢ +∞eiτ:ℝ–onto→ℂ∞N
Syntax	chalf 37659	Syntax for the temporary one-half.
class 1/2
Definition	df-bj-onehalf 37660	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 7366) $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 37661	An element of the circle at infinity is not a complex number. (Contributed by BJ, 4-Feb-2023.)
⊢ ¬ (+∞eiτ‘𝐴) ∈ ℂ
Syntax	cinftyexpi 37662	Syntax for the function +∞ei parameterizing ℂ∞.
class +∞ei
Definition	df-bj-inftyexpi 37663	Definition of the auxiliary function +∞ei parameterizing the circle at infinity ℂ∞ in ℂ̅. We use coupling with ℂ to simplify the proof of bj-ccinftydisj 37669. 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 37655 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 37664	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 37665	Injectivity of the parameterization +∞ei. Remark: a more conceptual proof would use bj-inftyexpiinv 37664 and the fact that a function with a retraction is injective. (Contributed by BJ, 22-Jun-2019.)
⊢ ((𝐴 ∈ (-π(,]π) ∧ 𝐵 ∈ (-π(,]π)) → (𝐴 = 𝐵 ↔ (+∞ei‘𝐴) = (+∞ei‘𝐵)))
Theorem	bj-inftyexpidisj 37666	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 37667	Syntax for the circle at infinity ℂ∞.
class ℂ∞
Definition	df-bj-ccinfty 37668	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 37669	The circle at infinity is disjoint from the set of complex numbers. (Contributed by BJ, 22-Jun-2019.)
⊢ (ℂ ∩ ℂ∞) = ∅
Theorem	bj-elccinfty 37670	A lemma for infinite extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
⊢ (𝐴 ∈ (-π(,]π) → (+∞ei‘𝐴) ∈ ℂ∞)
Syntax	cccbar 37671	Syntax for the set of extended complex numbers ℂ̅.
class ℂ̅
Definition	df-bj-ccbar 37672	Definition of the set of extended complex numbers ℂ̅. (Contributed by BJ, 22-Jun-2019.)
⊢ ℂ̅ = (ℂ ∪ ℂ∞)
Theorem	bj-ccssccbar 37673	Complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
⊢ ℂ ⊆ ℂ̅
Theorem	bj-ccinftyssccbar 37674	Infinite extended complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
⊢ ℂ∞ ⊆ ℂ̅
Syntax	cpinfty 37675	Syntax for "plus infinity".
class +∞
Definition	df-bj-pinfty 37676	Definition of "plus infinity". (Contributed by BJ, 27-Jun-2019.)
⊢ +∞ = (+∞ei‘0)
Theorem	bj-pinftyccb 37677	The class +∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ +∞ ∈ ℂ̅
Theorem	bj-pinftynrr 37678	The extended complex number +∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ ¬ +∞ ∈ ℂ
Syntax	cminfty 37679	Syntax for "minus infinity".
class -∞
Definition	df-bj-minfty 37680	Definition of "minus infinity". (Contributed by BJ, 27-Jun-2019.)
⊢ -∞ = (+∞ei‘π)
Theorem	bj-minftyccb 37681	The class -∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ -∞ ∈ ℂ̅
Theorem	bj-minftynrr 37682	The extended complex number -∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ ¬ -∞ ∈ ℂ
Theorem	bj-pinftynminfty 37683	The extended complex numbers +∞ and -∞ are different. (Contributed by BJ, 27-Jun-2019.)
⊢ +∞ ≠ -∞
Syntax	crrbar 37684	Syntax for the set of extended real numbers.
class ℝ̅
Definition	df-bj-rrbar 37685	Definition of the set of extended real numbers. This aims to replace df-xr 11217. (Contributed by BJ, 29-Jun-2019.)
⊢ ℝ̅ = (ℝ ∪ {-∞, +∞})
Syntax	cinfty 37686	Syntax for ∞.
class ∞
Definition	df-bj-infty 37687	Definition of ∞, the point at infinity of the real or complex projective line. (Contributed by BJ, 27-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)
⊢ ∞ = 𝒫 ∪ ℂ
Syntax	ccchat 37688	Syntax for ℂ̂.
class ℂ̂
Definition	df-bj-cchat 37689	Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.)
⊢ ℂ̂ = (ℂ ∪ {∞})
Syntax	crrhat 37690	Syntax for ℝ̂.
class ℝ̂
Definition	df-bj-rrhat 37691	Define the real projective line. (Contributed by BJ, 27-Jun-2019.)
⊢ ℝ̂ = (ℝ ∪ {∞})
Theorem	bj-rrhatsscchat 37692	The real projective line is included in the complex projective line. (Contributed by BJ, 27-Jun-2019.)
⊢ ℝ̂ ⊆ ℂ̂
21.19.6.6  Addition and opposite We define the operations of addition and opposite on the extended complex numbers and on the complex projective line (Riemann sphere) simultaneously, thus "overloading" the operations.
Syntax	caddcc 37693	Syntax for the addition on extended complex numbers.
class +ℂ̅
Definition	df-bj-addc 37694	Define the additions on the extended complex numbers (on the subset of (ℂ̅ × ℂ̅) where it makes sense) and on the complex projective line (Riemann sphere). We use the plural in "additions" since these are two different operations, even though +ℂ̅ is overloaded. (Contributed by BJ, 22-Jun-2019.)
⊢ +ℂ̅ = (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ ( I ↾ ℂ∞))) ↦ if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if((1st ‘𝑥) ∈ ℂ, if((2nd ‘𝑥) ∈ ℂ, ⟨((1st ‘(1st ‘𝑥)) +R (1st ‘(2nd ‘𝑥))), ((2nd ‘(1st ‘𝑥)) +R (2nd ‘(2nd ‘𝑥)))⟩, (2nd ‘𝑥)), (1st ‘𝑥))))
Syntax	coppcc 37695	Syntax for negation on the set of extended complex numbers and the complex projective line (Riemann sphere).
class -ℂ̅
Definition	df-bj-oppc 37696*	Define the negation (operation giving the opposite) on the set of extended complex numbers and the complex projective line (Riemann sphere). (Contributed by BJ, 22-Jun-2019.)
⊢ -ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ ⟨1/2, 0R⟩)))))
21.19.6.7  Order relation on the extended reals In this section, we redefine df-ltxr 11218 without the intermediate step of df-lt 11083.
Syntax	cltxr 37697	Syntax for the standard (strict) order on the extended reals.
class <ℝ̅
Definition	df-bj-lt 37698*	Define the standard (strict) order on the extended reals. (Contributed by BJ, 4-Feb-2023.)
⊢ <ℝ̅ = ({𝑥 ∈ (ℝ̅ × ℝ̅) ∣ ∃𝑦∃𝑧(((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)} ∪ ((({-∞} × ℝ) ∪ (ℝ × {+∞})) ∪ ({-∞} × {+∞})))
21.19.6.8  Argument, multiplication and inverse Since one needs arguments in order to define multiplication in ℂ̅, and one needs complex multiplication in order to define arguments, it would be contrived to construct a whole theory for a temporary multiplication (and temporary powers, then temporary logarithm, and finally temporary argument) before redefining the extended complex multiplication. Therefore, we adopt a two-step process, see df-bj-mulc 37702.
Syntax	carg 37699	Syntax for the argument of a nonzero extended complex number.
class Arg
Definition	df-bj-arg 37700	Define the argument of a nonzero extended complex number. By convention, it has values in (-π, π]. Another convention chooses values in [0, 2π) but the present convention simplifies formulas giving the argument as an arctangent. (Contributed by BJ, 22-Jun-2019.) The "else" case of the second conditional operator, corresponding to infinite extended complex numbers other than -∞, gives a definition depending on the specific definition chosen for these numbers (df-bj-inftyexpitau 37655), and therefore should not be relied upon. (New usage is discouraged.)
⊢ Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π))))