Theorem f1mptrn

Description: Express injection for a mapping operation. (Contributed by Thierry Arnoux, 3-May-2020)

	Ref	Expression
Hypotheses	f1mptrn.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
	f1mptrn.2	$$⊢\left(\phi \wedge y\in C\right)\to \exists !x\in Ay=B$$
Assertion	f1mptrn	$$⊢\phi \to \mathrm{Fun}{\left(x\in A⟼B\right)}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		f1mptrn.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
2		f1mptrn.2	$$⊢\left(\phi \wedge y\in C\right)\to \exists !x\in Ay=B$$
3	1	ralrimiva	$$⊢\phi \to \forall x\in AB\in C$$
4	2	ralrimiva	$$⊢\phi \to \forall y\in C\exists !x\in Ay=B$$
5		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
6	5	f1ompt	$$⊢\left(x\in A⟼B\right):A\underset{1-1\; onto}{⟶}C\leftrightarrow \left(\forall x\in AB\in C\wedge \forall y\in C\exists !x\in Ay=B\right)$$
7		dff1o2	$$⊢\left(x\in A⟼B\right):A\underset{1-1\; onto}{⟶}C\leftrightarrow \left(\left(x\in A⟼B\right)FnA\wedge \mathrm{Fun}{\left(x\in A⟼B\right)}^{-1}\wedge \mathrm{ran}\left(x\in A⟼B\right)=C\right)$$
8	7	simp2bi	$$⊢\left(x\in A⟼B\right):A\underset{1-1\; onto}{⟶}C\to \mathrm{Fun}{\left(x\in A⟼B\right)}^{-1}$$
9	6 8	sylbir	$$⊢\left(\forall x\in AB\in C\wedge \forall y\in C\exists !x\in Ay=B\right)\to \mathrm{Fun}{\left(x\in A⟼B\right)}^{-1}$$
10	3 4 9	syl2anc	$$⊢\phi \to \mathrm{Fun}{\left(x\in A⟼B\right)}^{-1}$$