Theorem ex-cnv

Description: Example for df-cnv . Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Assertion	ex-cnv	$$⊢{\left\{⟨2,6⟩,⟨3,9⟩\right\}}^{-1}=\left\{⟨6,2⟩,⟨9,3⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cnvun	$$⊢{\left(\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}\right)}^{-1}={\left\{⟨2,6⟩\right\}}^{-1}\cup {\left\{⟨3,9⟩\right\}}^{-1}$$
2		2nn	$$⊢2\in \mathbb{N}$$
3	2	elexi	$$⊢2\in \mathrm{V}$$
4		6nn	$$⊢6\in \mathbb{N}$$
5	4	elexi	$$⊢6\in \mathrm{V}$$
6	3 5	cnvsn	$$⊢{\left\{⟨2,6⟩\right\}}^{-1}=\left\{⟨6,2⟩\right\}$$
7		3nn	$$⊢3\in \mathbb{N}$$
8	7	elexi	$$⊢3\in \mathrm{V}$$
9		9nn	$$⊢9\in \mathbb{N}$$
10	9	elexi	$$⊢9\in \mathrm{V}$$
11	8 10	cnvsn	$$⊢{\left\{⟨3,9⟩\right\}}^{-1}=\left\{⟨9,3⟩\right\}$$
12	6 11	uneq12i	$$⊢{\left\{⟨2,6⟩\right\}}^{-1}\cup {\left\{⟨3,9⟩\right\}}^{-1}=\left\{⟨6,2⟩\right\}\cup \left\{⟨9,3⟩\right\}$$
13	1 12	eqtri	$$⊢{\left(\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}\right)}^{-1}=\left\{⟨6,2⟩\right\}\cup \left\{⟨9,3⟩\right\}$$
14		df-pr	$$⊢\left\{⟨2,6⟩,⟨3,9⟩\right\}=\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}$$
15	14	cnveqi	$$⊢{\left\{⟨2,6⟩,⟨3,9⟩\right\}}^{-1}={\left(\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}\right)}^{-1}$$
16		df-pr	$$⊢\left\{⟨6,2⟩,⟨9,3⟩\right\}=\left\{⟨6,2⟩\right\}\cup \left\{⟨9,3⟩\right\}$$
17	13 15 16	3eqtr4i	$$⊢{\left\{⟨2,6⟩,⟨3,9⟩\right\}}^{-1}=\left\{⟨6,2⟩,⟨9,3⟩\right\}$$