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

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

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 35078 . 2 class Id
2 vx . . 3 setvar 𝑥
3 cvv 3408 . . 3 class V
4 cid 5454 . . . 4 class I
52cv 1542 . . . 4 class 𝑥
64, 5cres 5553 . . 3 class ( I ↾ 𝑥)
72, 3, 6cmpt 5135 . 2 class (𝑥 ∈ V ↦ ( I ↾ 𝑥))
81, 7wceq 1543 1 wff Id = (𝑥 ∈ V ↦ ( I ↾ 𝑥))
Colors of variables: wff setvar class
This definition is referenced by:  bj-diagval  35080
  Copyright terms: Public domain W3C validator