Theorem 1stinr

Description: The first component of the value of a right injection is 1o . (Contributed by AV, 27-Jun-2022)

	Ref	Expression
Assertion	1stinr	|- ( X e. V -> ( 1st ` ( inr ` X ) ) = 1o )

Proof

Step	Hyp	Ref	Expression
1		df-inr	|- inr = ( x e. _V |-> <. 1o , x >. )
2		opeq2	|- ( x = X -> <. 1o , x >. = <. 1o , X >. )
3		elex	|- ( X e. V -> X e. _V )
4		opex	|- <. 1o , X >. e. _V
5	4	a1i	|- ( X e. V -> <. 1o , X >. e. _V )
6	1 2 3 5	fvmptd3	|- ( X e. V -> ( inr ` X ) = <. 1o , X >. )
7	6	fveq2d	|- ( X e. V -> ( 1st ` ( inr ` X ) ) = ( 1st ` <. 1o , X >. ) )
8		1oex	|- 1o e. _V
9		op1stg	|- ( ( 1o e. _V /\ X e. V ) -> ( 1st ` <. 1o , X >. ) = 1o )
10	8 9	mpan	|- ( X e. V -> ( 1st ` <. 1o , X >. ) = 1o )
11	7 10	eqtrd	|- ( X e. V -> ( 1st ` ( inr ` X ) ) = 1o )