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	$$⊢\left({inr\upharpoonright }_B\right):B\underset{1-1}{⟶}\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		f1of1	$$⊢inr:\mathrm{V}\underset{1-1\; onto}{⟶}\left\{1_{𝑜}\right\}\times \mathrm{V}\to inr:\mathrm{V}\underset{1-1}{⟶}\left\{1_{𝑜}\right\}\times \mathrm{V}$$
3	1 2	ax-mp	$$⊢inr:\mathrm{V}\underset{1-1}{⟶}\left\{1_{𝑜}\right\}\times \mathrm{V}$$
4		ssv	$$⊢B\subseteq \mathrm{V}$$
5		inrresf	$$⊢\left({inr\upharpoonright }_B\right):B⟶\left(A\mathrm{\bigsqcup ︀}B\right)$$
6		f1resf1	$$⊢\left(inr:\mathrm{V}\underset{1-1}{⟶}\left\{1_{𝑜}\right\}\times \mathrm{V}\wedge B\subseteq \mathrm{V}\wedge \left({inr\upharpoonright }_B\right):B⟶\left(A\mathrm{\bigsqcup ︀}B\right)\right)\to \left({inr\upharpoonright }_B\right):B\underset{1-1}{⟶}\left(A\mathrm{\bigsqcup ︀}B\right)$$
7	3 4 5 6	mp3an	$$⊢\left({inr\upharpoonright }_B\right):B\underset{1-1}{⟶}\left(A\mathrm{\bigsqcup ︀}B\right)$$