f1orescnv

Description: The converse of a one-to-one-onto restricted function. (Contributed by Paul Chapman, 21-Apr-2008)

		Ref	Expression
	Assertion	f1orescnv	$⊢ (Fun F^{-1} \land ({F ↾}_{R}) : R \underset{1-1 onto}{⟶} P) \to ({F^{-1} ↾}_{P}) : P \underset{1-1 onto}{⟶} R$

Step	Hyp	Ref	Expression
1		f1ocnv	$⊢ ({F ↾}_{R}) : R \underset{1-1 onto}{⟶} P \to {({F ↾}_{R})}^{-1} : P \underset{1-1 onto}{⟶} R$
2	1	adantl	$⊢ (Fun F^{-1} \land ({F ↾}_{R}) : R \underset{1-1 onto}{⟶} P) \to {({F ↾}_{R})}^{-1} : P \underset{1-1 onto}{⟶} R$
3		funcnvres	$⊢ Fun F^{-1} \to {({F ↾}_{R})}^{-1} = {F^{-1} ↾}_{F [R]}$
4		df-ima	$⊢ F [R] = ran ({F ↾}_{R})$
5		dff1o5	$⊢ ({F ↾}_{R}) : R \underset{1-1 onto}{⟶} P \leftrightarrow (({F ↾}_{R}) : R \underset{1-1}{⟶} P \land ran ({F ↾}_{R}) = P)$
6	5	simprbi	$⊢ ({F ↾}_{R}) : R \underset{1-1 onto}{⟶} P \to ran ({F ↾}_{R}) = P$
7	4 6	syl5eq	$⊢ ({F ↾}_{R}) : R \underset{1-1 onto}{⟶} P \to F [R] = P$
8	7	reseq2d	$⊢ ({F ↾}_{R}) : R \underset{1-1 onto}{⟶} P \to {F^{-1} ↾}_{F [R]} = {F^{-1} ↾}_{P}$
9	3 8	sylan9eq	$⊢ (Fun F^{-1} \land ({F ↾}_{R}) : R \underset{1-1 onto}{⟶} P) \to {({F ↾}_{R})}^{-1} = {F^{-1} ↾}_{P}$
10		f1oeq1	$⊢ {({F ↾}_{R})}^{-1} = {F^{-1} ↾}_{P} \to ({({F ↾}_{R})}^{-1} : P \underset{1-1 onto}{⟶} R \leftrightarrow ({F^{-1} ↾}_{P}) : P \underset{1-1 onto}{⟶} R)$
11	9 10	syl	$⊢ (Fun F^{-1} \land ({F ↾}_{R}) : R \underset{1-1 onto}{⟶} P) \to ({({F ↾}_{R})}^{-1} : P \underset{1-1 onto}{⟶} R \leftrightarrow ({F^{-1} ↾}_{P}) : P \underset{1-1 onto}{⟶} R)$
12	2 11	mpbid	$⊢ (Fun F^{-1} \land ({F ↾}_{R}) : R \underset{1-1 onto}{⟶} P) \to ({F^{-1} ↾}_{P}) : P \underset{1-1 onto}{⟶} R$

Metamath Proof Explorer