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 ) ) = (/) )