# Metamath Proof Explorer

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