This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )
6 5 adantl 
 |-  ( ( 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 >. ) )
22 21 ad2antll 
 |-  ( ( T. /\ ( x e. _V /\ y e. ( { (/) } X. _V ) ) ) -> ( x = ( 2nd ` y ) <-> y = <. (/) , x >. ) )
23 1 6 7 22 f1o2d 
 |-  ( T. -> inl : _V -1-1-onto-> ( { (/) } X. _V ) )
24 23 mptru 
 |-  inl : _V -1-1-onto-> ( { (/) } X. _V )