# Metamath Proof Explorer

## Theorem djulf1o

Description: The left injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022)

Ref Expression
Assertion djulf1o
`|- inl : _V -1-1-onto-> ( { (/) } X. _V )`

### Proof

Step Hyp Ref Expression
1 df-inl
` |-  inl = ( x e. _V |-> <. (/) , x >. )`
2 0ex
` |-  (/) e. _V`
3 2 snid
` |-  (/) e. { (/) }`
4 opelxpi
` |-  ( ( (/) e. { (/) } /\ x e. _V ) -> <. (/) , x >. e. ( { (/) } X. _V ) )`
5 3 4 mpan
` |-  ( x e. _V -> <. (/) , x >. e. ( { (/) } X. _V ) )`
` |-  ( ( T. /\ x e. _V ) -> <. (/) , x >. e. ( { (/) } X. _V ) )`
7 fvexd
` |-  ( ( T. /\ y e. ( { (/) } X. _V ) ) -> ( 2nd ` y ) e. _V )`
8 1st2nd2
` |-  ( y e. ( { (/) } X. _V ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )`
9 xp1st
` |-  ( y e. ( { (/) } X. _V ) -> ( 1st ` y ) e. { (/) } )`
10 elsni
` |-  ( ( 1st ` y ) e. { (/) } -> ( 1st ` y ) = (/) )`
11 9 10 syl
` |-  ( y e. ( { (/) } X. _V ) -> ( 1st ` y ) = (/) )`
12 11 opeq1d
` |-  ( y e. ( { (/) } X. _V ) -> <. ( 1st ` y ) , ( 2nd ` y ) >. = <. (/) , ( 2nd ` y ) >. )`
13 8 12 eqtrd
` |-  ( y e. ( { (/) } X. _V ) -> y = <. (/) , ( 2nd ` y ) >. )`
14 13 eqeq2d
` |-  ( y e. ( { (/) } X. _V ) -> ( <. (/) , x >. = y <-> <. (/) , x >. = <. (/) , ( 2nd ` y ) >. ) )`
15 eqcom
` |-  ( <. (/) , x >. = y <-> y = <. (/) , x >. )`
16 eqid
` |-  (/) = (/)`
17 vex
` |-  x e. _V`
18 2 17 opth
` |-  ( <. (/) , x >. = <. (/) , ( 2nd ` y ) >. <-> ( (/) = (/) /\ x = ( 2nd ` y ) ) )`
19 16 18 mpbiran
` |-  ( <. (/) , x >. = <. (/) , ( 2nd ` y ) >. <-> x = ( 2nd ` y ) )`
20 14 15 19 3bitr3g
` |-  ( y e. ( { (/) } X. _V ) -> ( y = <. (/) , x >. <-> x = ( 2nd ` y ) ) )`
21 20 bicomd
` |-  ( y e. ( { (/) } X. _V ) -> ( x = ( 2nd ` y ) <-> y = <. (/) , x >. ) )`
` |-  ( ( T. /\ ( x e. _V /\ y e. ( { (/) } X. _V ) ) ) -> ( x = ( 2nd ` y ) <-> y = <. (/) , x >. ) )`
` |-  ( T. -> inl : _V -1-1-onto-> ( { (/) } X. _V ) )`
` |-  inl : _V -1-1-onto-> ( { (/) } X. _V )`