Description: Right injection of a disjoint union. (Contributed by Mario Carneiro, 21Jun2022)
Ref  Expression  

Assertion  dfinr   inr = ( x e. _V > <. 1o , x >. ) 
Step  Hyp  Ref  Expression 

0  cinr   inr 

1  vx   x 

2  cvv   _V 

3  c1o   1o 

4  1  cv   x 
5  3 4  cop   <. 1o , x >. 
6  1 2 5  cmpt   ( x e. _V > <. 1o , x >. ) 
7  0 6  wceq   inr = ( x e. _V > <. 1o , x >. ) 