f1ssf1

Description: A subset of an injective function is injective. (Contributed by AV, 20-Nov-2020)

		Ref	Expression
	Assertion	f1ssf1	$⊢ (Fun F \land Fun F^{-1} \land G \subseteq F) \to Fun G^{-1}$

Step	Hyp	Ref	Expression
1		funssres	$⊢ (Fun F \land G \subseteq F) \to {F ↾}_{dom G} = G$
2		funres11	$⊢ Fun F^{-1} \to Fun {({F ↾}_{dom G})}^{-1}$
3		cnveq	$⊢ G = {F ↾}_{dom G} \to G^{-1} = {({F ↾}_{dom G})}^{-1}$
4	3	funeqd	$⊢ G = {F ↾}_{dom G} \to (Fun G^{-1} \leftrightarrow Fun {({F ↾}_{dom G})}^{-1})$
5	2 4	imbitrrid	$⊢ G = {F ↾}_{dom G} \to (Fun F^{-1} \to Fun G^{-1})$
6	5	eqcoms	$⊢ {F ↾}_{dom G} = G \to (Fun F^{-1} \to Fun G^{-1})$
7	1 6	syl	$⊢ (Fun F \land G \subseteq F) \to (Fun F^{-1} \to Fun G^{-1})$
8	7	ex	$⊢ Fun F \to (G \subseteq F \to (Fun F^{-1} \to Fun G^{-1}))$
9	8	com23	$⊢ Fun F \to (Fun F^{-1} \to (G \subseteq F \to Fun G^{-1}))$
10	9	3imp	$⊢ (Fun F \land Fun F^{-1} \land G \subseteq F) \to Fun G^{-1}$

Metamath Proof Explorer