Theorem ex-xp

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

	Ref	Expression
Assertion	ex-xp	$$⊢\left\{1,5\right\}\times \left\{2,7\right\}=\left\{⟨1,2⟩,⟨1,7⟩\right\}\cup \left\{⟨5,2⟩,⟨5,7⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-pr	$$⊢\left\{1,5\right\}=\left\{1\right\}\cup \left\{5\right\}$$
2		df-pr	$$⊢\left\{2,7\right\}=\left\{2\right\}\cup \left\{7\right\}$$
3	1 2	xpeq12i	$$⊢\left\{1,5\right\}\times \left\{2,7\right\}=\left(\left\{1\right\}\cup \left\{5\right\}\right)\times \left(\left\{2\right\}\cup \left\{7\right\}\right)$$
4		xpun	$$⊢\left(\left\{1\right\}\cup \left\{5\right\}\right)\times \left(\left\{2\right\}\cup \left\{7\right\}\right)=\left(\left(\left\{1\right\}\times \left\{2\right\}\right)\cup \left(\left\{1\right\}\times \left\{7\right\}\right)\right)\cup \left(\left(\left\{5\right\}\times \left\{2\right\}\right)\cup \left(\left\{5\right\}\times \left\{7\right\}\right)\right)$$
5		1ex	$$⊢1\in \mathrm{V}$$
6		2nn	$$⊢2\in \mathbb{N}$$
7	6	elexi	$$⊢2\in \mathrm{V}$$
8	5 7	xpsn	$$⊢\left\{1\right\}\times \left\{2\right\}=\left\{⟨1,2⟩\right\}$$
9		7nn	$$⊢7\in \mathbb{N}$$
10	9	elexi	$$⊢7\in \mathrm{V}$$
11	5 10	xpsn	$$⊢\left\{1\right\}\times \left\{7\right\}=\left\{⟨1,7⟩\right\}$$
12	8 11	uneq12i	$$⊢\left(\left\{1\right\}\times \left\{2\right\}\right)\cup \left(\left\{1\right\}\times \left\{7\right\}\right)=\left\{⟨1,2⟩\right\}\cup \left\{⟨1,7⟩\right\}$$
13		df-pr	$$⊢\left\{⟨1,2⟩,⟨1,7⟩\right\}=\left\{⟨1,2⟩\right\}\cup \left\{⟨1,7⟩\right\}$$
14	12 13	eqtr4i	$$⊢\left(\left\{1\right\}\times \left\{2\right\}\right)\cup \left(\left\{1\right\}\times \left\{7\right\}\right)=\left\{⟨1,2⟩,⟨1,7⟩\right\}$$
15		5nn	$$⊢5\in \mathbb{N}$$
16	15	elexi	$$⊢5\in \mathrm{V}$$
17	16 7	xpsn	$$⊢\left\{5\right\}\times \left\{2\right\}=\left\{⟨5,2⟩\right\}$$
18	16 10	xpsn	$$⊢\left\{5\right\}\times \left\{7\right\}=\left\{⟨5,7⟩\right\}$$
19	17 18	uneq12i	$$⊢\left(\left\{5\right\}\times \left\{2\right\}\right)\cup \left(\left\{5\right\}\times \left\{7\right\}\right)=\left\{⟨5,2⟩\right\}\cup \left\{⟨5,7⟩\right\}$$
20		df-pr	$$⊢\left\{⟨5,2⟩,⟨5,7⟩\right\}=\left\{⟨5,2⟩\right\}\cup \left\{⟨5,7⟩\right\}$$
21	19 20	eqtr4i	$$⊢\left(\left\{5\right\}\times \left\{2\right\}\right)\cup \left(\left\{5\right\}\times \left\{7\right\}\right)=\left\{⟨5,2⟩,⟨5,7⟩\right\}$$
22	14 21	uneq12i	$$⊢\left(\left(\left\{1\right\}\times \left\{2\right\}\right)\cup \left(\left\{1\right\}\times \left\{7\right\}\right)\right)\cup \left(\left(\left\{5\right\}\times \left\{2\right\}\right)\cup \left(\left\{5\right\}\times \left\{7\right\}\right)\right)=\left\{⟨1,2⟩,⟨1,7⟩\right\}\cup \left\{⟨5,2⟩,⟨5,7⟩\right\}$$
23	3 4 22	3eqtri	$$⊢\left\{1,5\right\}\times \left\{2,7\right\}=\left\{⟨1,2⟩,⟨1,7⟩\right\}\cup \left\{⟨5,2⟩,⟨5,7⟩\right\}$$