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	$$⊢\left({inl\upharpoonright }_A\right):A\underset{1-1}{⟶}\left(A\mathrm{\bigsqcup ︀}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		djulf1o	$$⊢inl:\mathrm{V}\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\times \mathrm{V}$$
2		f1of1	$$⊢inl:\mathrm{V}\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\times \mathrm{V}\to inl:\mathrm{V}\underset{1-1}{⟶}\left\{\varnothing \right\}\times \mathrm{V}$$
3	1 2	ax-mp	$$⊢inl:\mathrm{V}\underset{1-1}{⟶}\left\{\varnothing \right\}\times \mathrm{V}$$
4		ssv	$$⊢A\subseteq \mathrm{V}$$
5		inlresf	$$⊢\left({inl\upharpoonright }_A\right):A⟶\left(A\mathrm{\bigsqcup ︀}B\right)$$
6		f1resf1	$$⊢\left(inl:\mathrm{V}\underset{1-1}{⟶}\left\{\varnothing \right\}\times \mathrm{V}\wedge A\subseteq \mathrm{V}\wedge \left({inl\upharpoonright }_A\right):A⟶\left(A\mathrm{\bigsqcup ︀}B\right)\right)\to \left({inl\upharpoonright }_A\right):A\underset{1-1}{⟶}\left(A\mathrm{\bigsqcup ︀}B\right)$$
7	3 4 5 6	mp3an	$$⊢\left({inl\upharpoonright }_A\right):A\underset{1-1}{⟶}\left(A\mathrm{\bigsqcup ︀}B\right)$$