Definition df-inl

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

	Ref	Expression
Assertion	df-inl	⊢ inl = ( 𝑥 ∈ V ↦ ⟨ ∅ , 𝑥 ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinl	⊢ inl
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		c0	⊢ ∅
4	1	cv	⊢ 𝑥
5	3 4	cop	⊢ ⟨ ∅ , 𝑥 ⟩
6	1 2 5	cmpt	⊢ ( 𝑥 ∈ V ↦ ⟨ ∅ , 𝑥 ⟩ )
7	0 6	wceq	⊢ inl = ( 𝑥 ∈ V ↦ ⟨ ∅ , 𝑥 ⟩ )