2ndinl

Description: The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022)

		Ref	Expression
	Assertion	2ndinl	$⊢ X \in V \to 2^{nd} (inl (X)) = X$

Step	Hyp	Ref	Expression
1		df-inl	$⊢ inl = (x \in V ⟼ ⟨\emptyset, x⟩)$
2		opeq2	$⊢ x = X \to ⟨\emptyset, x⟩ = ⟨\emptyset, X⟩$
3		elex	$⊢ X \in V \to X \in V$
4		opex	$⊢ ⟨\emptyset, X⟩ \in V$
5	4	a1i	$⊢ X \in V \to ⟨\emptyset, X⟩ \in V$
6	1 2 3 5	fvmptd3	$⊢ X \in V \to inl (X) = ⟨\emptyset, X⟩$
7	6	fveq2d	$⊢ X \in V \to 2^{nd} (inl (X)) = 2^{nd} (⟨\emptyset, X⟩)$
8		0ex	$⊢ \emptyset \in V$
9		op2ndg	$⊢ (\emptyset \in V \land X \in V) \to 2^{nd} (⟨\emptyset, X⟩) = X$
10	8 9	mpan	$⊢ X \in V \to 2^{nd} (⟨\emptyset, X⟩) = X$
11	7 10	eqtrd	$⊢ X \in V \to 2^{nd} (inl (X)) = X$

Metamath Proof Explorer