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 )