Theorem inrresf

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

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

Proof

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