Theorem f1cnvcnv

Description: Two ways to express that a set A (not necessarily a function) is one-to-one. Each side is equivalent to Definition 6.4(3) of TakeutiZaring p. 24, who use the notation "Un_2 (A)" for one-to-one. We do not introduce a separate notation since we rarely use it. (Contributed by NM, 13-Aug-2004)

	Ref	Expression
Assertion	f1cnvcnv	$$⊢{A^{-1}}^{-1}:\mathrm{dom}A\underset{1-1}{⟶}\mathrm{V}\leftrightarrow \left(\mathrm{Fun}{A}^{-1}\wedge \mathrm{Fun}{A^{-1}}^{-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-f1	$$⊢{A^{-1}}^{-1}:\mathrm{dom}A\underset{1-1}{⟶}\mathrm{V}\leftrightarrow \left({A^{-1}}^{-1}:\mathrm{dom}A⟶\mathrm{V}\wedge \mathrm{Fun}{{A^{-1}}^{-1}}^{-1}\right)$$
2		dffn2	$$⊢{A^{-1}}^{-1}Fn\mathrm{dom}A\leftrightarrow {A^{-1}}^{-1}:\mathrm{dom}A⟶\mathrm{V}$$
3		dmcnvcnv	$$⊢\mathrm{dom}{A^{-1}}^{-1}=\mathrm{dom}A$$
4		df-fn	$$⊢{A^{-1}}^{-1}Fn\mathrm{dom}A\leftrightarrow \left(\mathrm{Fun}{A^{-1}}^{-1}\wedge \mathrm{dom}{A^{-1}}^{-1}=\mathrm{dom}A\right)$$
5	3 4	mpbiran2	$$⊢{A^{-1}}^{-1}Fn\mathrm{dom}A\leftrightarrow \mathrm{Fun}{A^{-1}}^{-1}$$
6	2 5	bitr3i	$$⊢{A^{-1}}^{-1}:\mathrm{dom}A⟶\mathrm{V}\leftrightarrow \mathrm{Fun}{A^{-1}}^{-1}$$
7		relcnv	$$⊢\mathrm{Rel}{A}^{-1}$$
8		dfrel2	$$⊢\mathrm{Rel}{A}^{-1}\leftrightarrow {{A^{-1}}^{-1}}^{-1}=A^{-1}$$
9	7 8	mpbi	$$⊢{{A^{-1}}^{-1}}^{-1}=A^{-1}$$
10	9	funeqi	$$⊢\mathrm{Fun}{{A^{-1}}^{-1}}^{-1}\leftrightarrow \mathrm{Fun}{A}^{-1}$$
11	6 10	anbi12ci	$$⊢\left({A^{-1}}^{-1}:\mathrm{dom}A⟶\mathrm{V}\wedge \mathrm{Fun}{{A^{-1}}^{-1}}^{-1}\right)\leftrightarrow \left(\mathrm{Fun}{A}^{-1}\wedge \mathrm{Fun}{A^{-1}}^{-1}\right)$$
12	1 11	bitri	$$⊢{A^{-1}}^{-1}:\mathrm{dom}A\underset{1-1}{⟶}\mathrm{V}\leftrightarrow \left(\mathrm{Fun}{A}^{-1}\wedge \mathrm{Fun}{A^{-1}}^{-1}\right)$$