Theorem inrresf1

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

	Ref	Expression
Assertion	inrresf1	|- ( inr |` B ) : B -1-1-> ( A |_| B )

Proof

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