Theorem cnvcnvsn

Description: Double converse of a singleton of an ordered pair. (Unlike cnvsn , this does not need any sethood assumptions on A and B .) (Contributed by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	cnvcnvsn	$$⊢{{\left\{⟨A,B⟩\right\}}^{-1}}^{-1}={\left\{⟨B,A⟩\right\}}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{{\left\{⟨A,B⟩\right\}}^{-1}}^{-1}$$
2		relcnv	$$⊢\mathrm{Rel}{\left\{⟨B,A⟩\right\}}^{-1}$$
3		vex	$$⊢x\in \mathrm{V}$$
4		vex	$$⊢y\in \mathrm{V}$$
5	3 4	opelcnv	$$⊢⟨x,y⟩\in {{\left\{⟨A,B⟩\right\}}^{-1}}^{-1}\leftrightarrow ⟨y,x⟩\in {\left\{⟨A,B⟩\right\}}^{-1}$$
6		ancom	$$⊢\left(x=A\wedge y=B\right)\leftrightarrow \left(y=B\wedge x=A\right)$$
7	3 4	opth	$$⊢⟨x,y⟩=⟨A,B⟩\leftrightarrow \left(x=A\wedge y=B\right)$$
8	4 3	opth	$$⊢⟨y,x⟩=⟨B,A⟩\leftrightarrow \left(y=B\wedge x=A\right)$$
9	6 7 8	3bitr4i	$$⊢⟨x,y⟩=⟨A,B⟩\leftrightarrow ⟨y,x⟩=⟨B,A⟩$$
10		opex	$$⊢⟨x,y⟩\in \mathrm{V}$$
11	10	elsn	$$⊢⟨x,y⟩\in \left\{⟨A,B⟩\right\}\leftrightarrow ⟨x,y⟩=⟨A,B⟩$$
12		opex	$$⊢⟨y,x⟩\in \mathrm{V}$$
13	12	elsn	$$⊢⟨y,x⟩\in \left\{⟨B,A⟩\right\}\leftrightarrow ⟨y,x⟩=⟨B,A⟩$$
14	9 11 13	3bitr4i	$$⊢⟨x,y⟩\in \left\{⟨A,B⟩\right\}\leftrightarrow ⟨y,x⟩\in \left\{⟨B,A⟩\right\}$$
15	4 3	opelcnv	$$⊢⟨y,x⟩\in {\left\{⟨A,B⟩\right\}}^{-1}\leftrightarrow ⟨x,y⟩\in \left\{⟨A,B⟩\right\}$$
16	3 4	opelcnv	$$⊢⟨x,y⟩\in {\left\{⟨B,A⟩\right\}}^{-1}\leftrightarrow ⟨y,x⟩\in \left\{⟨B,A⟩\right\}$$
17	14 15 16	3bitr4i	$$⊢⟨y,x⟩\in {\left\{⟨A,B⟩\right\}}^{-1}\leftrightarrow ⟨x,y⟩\in {\left\{⟨B,A⟩\right\}}^{-1}$$
18	5 17	bitri	$$⊢⟨x,y⟩\in {{\left\{⟨A,B⟩\right\}}^{-1}}^{-1}\leftrightarrow ⟨x,y⟩\in {\left\{⟨B,A⟩\right\}}^{-1}$$
19	1 2 18	eqrelriiv	$$⊢{{\left\{⟨A,B⟩\right\}}^{-1}}^{-1}={\left\{⟨B,A⟩\right\}}^{-1}$$