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 )