Theorem funALTVss

Description: Subclass theorem for function. (Contributed by NM, 16-Aug-1994) (Proof shortened by Mario Carneiro, 24-Jun-2014) (Revised by Peter Mazsa, 22-Sep-2021)

	Ref	Expression
Assertion	funALTVss	$$⊢A\subseteq B\to \left(FunALTVB\to FunALTVA\right)$$

Proof

Step	Hyp	Ref	Expression
1		cossss	$$⊢A\subseteq B\to \wr A\subseteq \wr B$$
2		sstr2	$$⊢\wr A\subseteq \wr B\to \left(\wr B\subseteq \mathrm{I}\to \wr A\subseteq \mathrm{I}\right)$$
3	1 2	syl	$$⊢A\subseteq B\to \left(\wr B\subseteq \mathrm{I}\to \wr A\subseteq \mathrm{I}\right)$$
4		relss	$$⊢A\subseteq B\to \left(\mathrm{Rel}B\to \mathrm{Rel}A\right)$$
5	3 4	anim12d	$$⊢A\subseteq B\to \left(\left(\wr B\subseteq \mathrm{I}\wedge \mathrm{Rel}B\right)\to \left(\wr A\subseteq \mathrm{I}\wedge \mathrm{Rel}A\right)\right)$$
6		dffunALTV2	$$⊢FunALTVB\leftrightarrow \left(\wr B\subseteq \mathrm{I}\wedge \mathrm{Rel}B\right)$$
7		dffunALTV2	$$⊢FunALTVA\leftrightarrow \left(\wr A\subseteq \mathrm{I}\wedge \mathrm{Rel}A\right)$$
8	5 6 7	3imtr4g	$$⊢A\subseteq B\to \left(FunALTVB\to FunALTVA\right)$$