Definition df-inr

Description: Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022)

	Ref	Expression
Assertion	df-inr	⊢ inr = ( 𝑥 ∈ V ↦ ⟨ 1o , 𝑥 ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinr	⊢ inr
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		c1o	⊢ 1o
4	1	cv	⊢ 𝑥
5	3 4	cop	⊢ ⟨ 1o , 𝑥 ⟩
6	1 2 5	cmpt	⊢ ( 𝑥 ∈ V ↦ ⟨ 1o , 𝑥 ⟩ )
7	0 6	wceq	⊢ inr = ( 𝑥 ∈ V ↦ ⟨ 1o , 𝑥 ⟩ )