Theorem inlresf1

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

	Ref	Expression
Assertion	inlresf1	⊢ ( inl ↾ 𝐴 ) : 𝐴 –1-1→ ( 𝐴 ⊔ 𝐵 )

Proof

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