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

Metamath Proof Explorer

Theorem djurf1o

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

Ref Expression
Assertion djurf1o 
|- inr : _V -1-1-onto-> ( { 1o } X. _V )

Proof

Step Hyp Ref Expression
1 df-inr 
 |-  inr = ( x e. _V |-> <. 1o , x >. )
2 1onn 
 |-  1o e. _om
3 snidg 
 |-  ( 1o e. _om -> 1o e. { 1o } )
4 2 3 ax-mp 
 |-  1o e. { 1o }
5 opelxpi 
 |-  ( ( 1o e. { 1o } /\ x e. _V ) -> <. 1o , x >. e. ( { 1o } X. _V ) )
6 4 5 mpan 
 |-  ( x e. _V -> <. 1o , x >. e. ( { 1o } X. _V ) )
7 6 adantl 
 |-  ( ( T. /\ x e. _V ) -> <. 1o , x >. e. ( { 1o } X. _V ) )
8 fvexd 
 |-  ( ( T. /\ y e. ( { 1o } X. _V ) ) -> ( 2nd ` y ) e. _V )
9 1st2nd2 
 |-  ( y e. ( { 1o } X. _V ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
10 xp1st 
 |-  ( y e. ( { 1o } X. _V ) -> ( 1st ` y ) e. { 1o } )
11 elsni 
 |-  ( ( 1st ` y ) e. { 1o } -> ( 1st ` y ) = 1o )
12 10 11 syl 
 |-  ( y e. ( { 1o } X. _V ) -> ( 1st ` y ) = 1o )
13 12 opeq1d 
 |-  ( y e. ( { 1o } X. _V ) -> <. ( 1st ` y ) , ( 2nd ` y ) >. = <. 1o , ( 2nd ` y ) >. )
14 9 13 eqtrd 
 |-  ( y e. ( { 1o } X. _V ) -> y = <. 1o , ( 2nd ` y ) >. )
15 14 eqeq2d 
 |-  ( y e. ( { 1o } X. _V ) -> ( <. 1o , x >. = y <-> <. 1o , x >. = <. 1o , ( 2nd ` y ) >. ) )
16 eqcom 
 |-  ( <. 1o , x >. = y <-> y = <. 1o , x >. )
17 eqid 
 |-  1o = 1o
18 1oex 
 |-  1o e. _V
19 vex 
 |-  x e. _V
20 18 19 opth 
 |-  ( <. 1o , x >. = <. 1o , ( 2nd ` y ) >. <-> ( 1o = 1o /\ x = ( 2nd ` y ) ) )
21 17 20 mpbiran 
 |-  ( <. 1o , x >. = <. 1o , ( 2nd ` y ) >. <-> x = ( 2nd ` y ) )
22 15 16 21 3bitr3g 
 |-  ( y e. ( { 1o } X. _V ) -> ( y = <. 1o , x >. <-> x = ( 2nd ` y ) ) )
23 22 bicomd 
 |-  ( y e. ( { 1o } X. _V ) -> ( x = ( 2nd ` y ) <-> y = <. 1o , x >. ) )
24 23 ad2antll 
 |-  ( ( T. /\ ( x e. _V /\ y e. ( { 1o } X. _V ) ) ) -> ( x = ( 2nd ` y ) <-> y = <. 1o , x >. ) )
25 1 7 8 24 f1o2d 
 |-  ( T. -> inr : _V -1-1-onto-> ( { 1o } X. _V ) )
26 25 mptru 
 |-  inr : _V -1-1-onto-> ( { 1o } X. _V )