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 ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		djurf1o	⊢ inr : V –1-1-onto→ ( { 1o } × V )
2		f1ofun	⊢ ( inr : V –1-1-onto→ ( { 1o } × V ) → Fun inr )
3		ffvresb	⊢ ( Fun inr → ( ( inr ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ dom inr ∧ ( inr ‘ 𝑥 ) ∈ ( 𝐴 ⊔ 𝐵 ) ) ) )
4	1 2 3	mp2b	⊢ ( ( inr ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ dom inr ∧ ( inr ‘ 𝑥 ) ∈ ( 𝐴 ⊔ 𝐵 ) ) )
5		elex	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ V )
6		opex	⊢ ⟨ 1o , 𝑥 ⟩ ∈ V
7		df-inr	⊢ inr = ( 𝑥 ∈ V ↦ ⟨ 1o , 𝑥 ⟩ )
8	6 7	dmmpti	⊢ dom inr = V
9	5 8	eleqtrrdi	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ dom inr )
10		djurcl	⊢ ( 𝑥 ∈ 𝐵 → ( inr ‘ 𝑥 ) ∈ ( 𝐴 ⊔ 𝐵 ) )
11	9 10	jca	⊢ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ dom inr ∧ ( inr ‘ 𝑥 ) ∈ ( 𝐴 ⊔ 𝐵 ) ) )
12	4 11	mprgbir	⊢ ( inr ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 )