Theorem inlresf

Description: The left injection restricted to the left class of a disjoint union is a function from the left class into the disjoint union. (Contributed by AV, 27-Jun-2022)

	Ref	Expression
Assertion	inlresf	⊢ ( inl ↾ 𝐴 ) : 𝐴 ⟶ ( 𝐴 ⊔ 𝐵 )

Proof

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