Metamath Proof Explorer

Theorem 1stinl

Description: The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022)

Ref Expression
Assertion 1stinl 
|- ( X e. V -> ( 1st ` ( inl ` 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 -> ( 1st ` ( inl ` X ) ) = ( 1st ` <. (/) , X >. ) )
8 0ex 
 |-  (/) e. _V
9 op1stg 
 |-  ( ( (/) e. _V /\ X e. V ) -> ( 1st ` <. (/) , X >. ) = (/) )
10 8 9 mpan 
 |-  ( X e. V -> ( 1st ` <. (/) , X >. ) = (/) )
11 7 10 eqtrd 
 |-  ( X e. V -> ( 1st ` ( inl ` X ) ) = (/) )