Theorem inlresf

Description: The left injection restricted to the left class of a disjoint union is a function from the left class into the disjoint union. (Contributed by AV, 27-Jun-2022)

	Ref	Expression
Assertion	inlresf	|- ( inl |` A ) : A --> ( A |_| B )

Proof

Step	Hyp	Ref	Expression
1		djulf1o	|- inl : _V -1-1-onto-> ( { (/) } X. _V )
2		f1ofun	|- ( inl : _V -1-1-onto-> ( { (/) } X. _V ) -> Fun inl )
3		ffvresb	|- ( Fun inl -> ( ( inl |` A ) : A --> ( A |_| B ) <-> A. x e. A ( x e. dom inl /\ ( inl ` x ) e. ( A |_| B ) ) ) )
4	1 2 3	mp2b	|- ( ( inl |` A ) : A --> ( A |_| B ) <-> A. x e. A ( x e. dom inl /\ ( inl ` x ) e. ( A |_| B ) ) )
5		elex	|- ( x e. A -> x e. _V )
6		opex	|- <. (/) , x >. e. _V
7		df-inl	|- inl = ( x e. _V |-> <. (/) , x >. )
8	6 7	dmmpti	|- dom inl = _V
9	5 8	eleqtrrdi	|- ( x e. A -> x e. dom inl )
10		djulcl	|- ( x e. A -> ( inl ` x ) e. ( A |_| B ) )
11	9 10	jca	|- ( x e. A -> ( x e. dom inl /\ ( inl ` x ) e. ( A |_| B ) ) )
12	4 11	mprgbir	|- ( inl |` A ) : A --> ( A |_| B )