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 (Fun B \to Fun A)$

Step	Hyp	Ref	Expression
1		relss	$⊢ A \subseteq B \to (Rel B \to Rel A)$
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 (B \circ B^{-1} \subseteq I \to A \circ A^{-1} \subseteq I)$
8	6 7	syl	$⊢ A \subseteq B \to (B \circ B^{-1} \subseteq I \to A \circ A^{-1} \subseteq I)$
9	1 8	anim12d	$⊢ A \subseteq B \to ((Rel B \land B \circ B^{-1} \subseteq I) \to (Rel A \land A \circ A^{-1} \subseteq I))$
10		df-fun	$⊢ Fun B \leftrightarrow (Rel B \land B \circ B^{-1} \subseteq I)$
11		df-fun	$⊢ Fun A \leftrightarrow (Rel A \land A \circ A^{-1} \subseteq I)$
12	9 10 11	3imtr4g	$⊢ A \subseteq B \to (Fun B \to Fun A)$

Metamath Proof Explorer