Theorem inlresf1

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

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

Proof

Step	Hyp	Ref	Expression
1		djulf1o	|- inl : _V -1-1-onto-> ( { (/) } X. _V )
2		f1of1	|- ( inl : _V -1-1-onto-> ( { (/) } X. _V ) -> inl : _V -1-1-> ( { (/) } X. _V ) )
3	1 2	ax-mp	|- inl : _V -1-1-> ( { (/) } X. _V )
4		ssv	|- A C_ _V
5		inlresf	|- ( inl |` A ) : A --> ( A |_| B )
6		f1resf1	|- ( ( inl : _V -1-1-> ( { (/) } X. _V ) /\ A C_ _V /\ ( inl |` A ) : A --> ( A |_| B ) ) -> ( inl |` A ) : A -1-1-> ( A |_| B ) )
7	3 4 5 6	mp3an	|- ( inl |` A ) : A -1-1-> ( A |_| B )