Theorem funss

Description: Subclass theorem for function predicate. (Contributed by NM, 16-Aug-1994) (Proof shortened by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Assertion	funss	$$⊢A\subseteq B\to \left(\mathrm{Fun}B\to \mathrm{Fun}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		relss	$$⊢A\subseteq B\to \left(\mathrm{Rel}B\to \mathrm{Rel}A\right)$$
2		coss1	$$⊢A\subseteq B\to A\circ A^{-1}\subseteq B\circ A^{-1}$$
3		cnvss	$$⊢A\subseteq B\to A^{-1}\subseteq B^{-1}$$
4		coss2	$$⊢A^{-1}\subseteq B^{-1}\to B\circ A^{-1}\subseteq B\circ B^{-1}$$
5	3 4	syl	$$⊢A\subseteq B\to B\circ A^{-1}\subseteq B\circ B^{-1}$$
6	2 5	sstrd	$$⊢A\subseteq B\to A\circ A^{-1}\subseteq B\circ B^{-1}$$
7		sstr2	$$⊢A\circ A^{-1}\subseteq B\circ B^{-1}\to \left(B\circ B^{-1}\subseteq \mathrm{I}\to A\circ A^{-1}\subseteq \mathrm{I}\right)$$
8	6 7	syl	$$⊢A\subseteq B\to \left(B\circ B^{-1}\subseteq \mathrm{I}\to A\circ A^{-1}\subseteq \mathrm{I}\right)$$
9	1 8	anim12d	$$⊢A\subseteq B\to \left(\left(\mathrm{Rel}B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)\to \left(\mathrm{Rel}A\wedge A\circ A^{-1}\subseteq \mathrm{I}\right)\right)$$
10		df-fun	$$⊢\mathrm{Fun}B\leftrightarrow \left(\mathrm{Rel}B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)$$
11		df-fun	$$⊢\mathrm{Fun}A\leftrightarrow \left(\mathrm{Rel}A\wedge A\circ A^{-1}\subseteq \mathrm{I}\right)$$
12	9 10 11	3imtr4g	$$⊢A\subseteq B\to \left(\mathrm{Fun}B\to \mathrm{Fun}A\right)$$