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	$$⊢\left({inr\upharpoonright }_B\right):B⟶\left(A\mathrm{\bigsqcup ︀}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		djurf1o	$$⊢inr:\mathrm{V}\underset{1-1\; onto}{⟶}\left\{1_{𝑜}\right\}\times \mathrm{V}$$
2		f1ofun	$$⊢inr:\mathrm{V}\underset{1-1\; onto}{⟶}\left\{1_{𝑜}\right\}\times \mathrm{V}\to \mathrm{Fun}inr$$
3		ffvresb	$$⊢\mathrm{Fun}inr\to \left(\left({inr\upharpoonright }_B\right):B⟶\left(A\mathrm{\bigsqcup ︀}B\right)\leftrightarrow \forall x\in B\left(x\in \mathrm{dom}inr\wedge inr\left(x\right)\in \left(A\mathrm{\bigsqcup ︀}B\right)\right)\right)$$
4	1 2 3	mp2b	$$⊢\left({inr\upharpoonright }_B\right):B⟶\left(A\mathrm{\bigsqcup ︀}B\right)\leftrightarrow \forall x\in B\left(x\in \mathrm{dom}inr\wedge inr\left(x\right)\in \left(A\mathrm{\bigsqcup ︀}B\right)\right)$$
5		elex	$$⊢x\in B\to x\in \mathrm{V}$$
6		opex	$$⊢⟨1_{𝑜},x⟩\in \mathrm{V}$$
7		df-inr	$$⊢inr=\left(x\in \mathrm{V}⟼⟨1_{𝑜},x⟩\right)$$
8	6 7	dmmpti	$$⊢\mathrm{dom}inr=\mathrm{V}$$
9	5 8	eleqtrrdi	$$⊢x\in B\to x\in \mathrm{dom}inr$$
10		djurcl	$$⊢x\in B\to inr\left(x\right)\in \left(A\mathrm{\bigsqcup ︀}B\right)$$
11	9 10	jca	$$⊢x\in B\to \left(x\in \mathrm{dom}inr\wedge inr\left(x\right)\in \left(A\mathrm{\bigsqcup ︀}B\right)\right)$$
12	4 11	mprgbir	$$⊢\left({inr\upharpoonright }_B\right):B⟶\left(A\mathrm{\bigsqcup ︀}B\right)$$