Theorem funcnvsn

Description: The converse singleton of an ordered pair is a function. This is equivalent to funsn via cnvsn , but stating it this way allows us to skip the sethood assumptions on A and B . (Contributed by NM, 30-Apr-2015)

	Ref	Expression
Assertion	funcnvsn	$$⊢\mathrm{Fun}{\left\{⟨A,B⟩\right\}}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{\left\{⟨A,B⟩\right\}}^{-1}$$
2		moeq	$$⊢{\exists }^{*}yy=A$$
3		vex	$$⊢x\in \mathrm{V}$$
4		vex	$$⊢y\in \mathrm{V}$$
5	3 4	brcnv	$$⊢x{\left\{⟨A,B⟩\right\}}^{-1}y\leftrightarrow y\left\{⟨A,B⟩\right\}x$$
6		df-br	$$⊢y\left\{⟨A,B⟩\right\}x\leftrightarrow ⟨y,x⟩\in \left\{⟨A,B⟩\right\}$$
7	5 6	bitri	$$⊢x{\left\{⟨A,B⟩\right\}}^{-1}y\leftrightarrow ⟨y,x⟩\in \left\{⟨A,B⟩\right\}$$
8		elsni	$$⊢⟨y,x⟩\in \left\{⟨A,B⟩\right\}\to ⟨y,x⟩=⟨A,B⟩$$
9	4 3	opth1	$$⊢⟨y,x⟩=⟨A,B⟩\to y=A$$
10	8 9	syl	$$⊢⟨y,x⟩\in \left\{⟨A,B⟩\right\}\to y=A$$
11	7 10	sylbi	$$⊢x{\left\{⟨A,B⟩\right\}}^{-1}y\to y=A$$
12	11	moimi	$$⊢{\exists }^{*}yy=A\to {\exists }^{*}yx{\left\{⟨A,B⟩\right\}}^{-1}y$$
13	2 12	ax-mp	$$⊢{\exists }^{*}yx{\left\{⟨A,B⟩\right\}}^{-1}y$$
14	13	ax-gen	$$⊢\forall x{\exists }^{*}yx{\left\{⟨A,B⟩\right\}}^{-1}y$$
15		dffun6	$$⊢\mathrm{Fun}{\left\{⟨A,B⟩\right\}}^{-1}\leftrightarrow \left(\mathrm{Rel}{\left\{⟨A,B⟩\right\}}^{-1}\wedge \forall x{\exists }^{*}yx{\left\{⟨A,B⟩\right\}}^{-1}y\right)$$
16	1 14 15	mpbir2an	$$⊢\mathrm{Fun}{\left\{⟨A,B⟩\right\}}^{-1}$$