Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-diag Structured version   Visualization version   GIF version

Definition df-bj-diag 34604
 Description: Define the functionalized identity, which can also be seen as the diagonal function. Its value is given in bj-diagval 34605 when it is viewed as the functionalized identity, and in bj-diagval2 34606 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 35733 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 34604. 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.)
Assertion
Ref Expression
df-bj-diag Id = (𝑥 ∈ V ↦ ( I ↾ 𝑥))

Detailed syntax breakdown of Definition df-bj-diag
StepHypRef Expression
1 cdiag2 34603 . 2 class Id
2 vx . . 3 setvar 𝑥
3 cvv 3441 . . 3 class V
4 cid 5424 . . . 4 class I
52cv 1537 . . . 4 class 𝑥
64, 5cres 5521 . . 3 class ( I ↾ 𝑥)
72, 3, 6cmpt 5110 . 2 class (𝑥 ∈ V ↦ ( I ↾ 𝑥))
81, 7wceq 1538 1 wff Id = (𝑥 ∈ V ↦ ( I ↾ 𝑥))
 Colors of variables: wff setvar class This definition is referenced by:  bj-diagval  34605
 Copyright terms: Public domain W3C validator