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 ↾ 𝐵 ) : 𝐵 –1-1→ ( 𝐴 ⊔ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		djurf1o	⊢ inr : V –1-1-onto→ ( { 1o } × V )
2		f1of1	⊢ ( inr : V –1-1-onto→ ( { 1o } × V ) → inr : V –1-1→ ( { 1o } × V ) )
3	1 2	ax-mp	⊢ inr : V –1-1→ ( { 1o } × V )
4		ssv	⊢ 𝐵 ⊆ V
5		inrresf	⊢ ( inr ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 )
6		f1resf1	⊢ ( ( inr : V –1-1→ ( { 1o } × V ) ∧ 𝐵 ⊆ V ∧ ( inr ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 ) ) → ( inr ↾ 𝐵 ) : 𝐵 –1-1→ ( 𝐴 ⊔ 𝐵 ) )
7	3 4 5 6	mp3an	⊢ ( inr ↾ 𝐵 ) : 𝐵 –1-1→ ( 𝐴 ⊔ 𝐵 )