Users' Mathboxes 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 37116
Description: Define the functionalized identity, which can also be seen as the diagonal function. Its value is given in bj-diagval 37117 when it is viewed as the functionalized identity, and in bj-diagval2 37118 when it is viewed as the diagonal function.

Indeed, Definition df-br 5151 identifies a binary relation with the class of couples that are related by that binary relation (see eqrel2 38242 for the extensionality property of binary relations). As a consequence, the identity relation, or identity function (see funi 6596), 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 37116.

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 37115 . 2 class Id
2 vx . . 3 setvar 𝑥
3 cvv 3477 . . 3 class V
4 cid 5576 . . . 4 class I
52cv 1534 . . . 4 class 𝑥
64, 5cres 5686 . . 3 class ( I ↾ 𝑥)
72, 3, 6cmpt 5233 . 2 class (𝑥 ∈ V ↦ ( I ↾ 𝑥))
81, 7wceq 1535 1 wff Id = (𝑥 ∈ V ↦ ( I ↾ 𝑥))
Colors of variables: wff setvar class
This definition is referenced by:  bj-diagval  37117
  Copyright terms: Public domain W3C validator