Metamath Proof Explorer

Theorem 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 e. V -> ( 2nd ` ( inl ` X ) ) = X )

Proof

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