# Metamath Proof Explorer

## 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\}×\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\}×\left\{2,7\right\}=\left(\left\{1\right\}\cup \left\{5\right\}\right)×\left(\left\{2\right\}\cup \left\{7\right\}\right)$
4 xpun ${⊢}\left(\left\{1\right\}\cup \left\{5\right\}\right)×\left(\left\{2\right\}\cup \left\{7\right\}\right)=\left(\left(\left\{1\right\}×\left\{2\right\}\right)\cup \left(\left\{1\right\}×\left\{7\right\}\right)\right)\cup \left(\left(\left\{5\right\}×\left\{2\right\}\right)\cup \left(\left\{5\right\}×\left\{7\right\}\right)\right)$
5 1ex ${⊢}1\in \mathrm{V}$
6 2nn ${⊢}2\in ℕ$
7 6 elexi ${⊢}2\in \mathrm{V}$
8 5 7 xpsn ${⊢}\left\{1\right\}×\left\{2\right\}=\left\{⟨1,2⟩\right\}$
9 7nn ${⊢}7\in ℕ$
10 9 elexi ${⊢}7\in \mathrm{V}$
11 5 10 xpsn ${⊢}\left\{1\right\}×\left\{7\right\}=\left\{⟨1,7⟩\right\}$
12 8 11 uneq12i ${⊢}\left(\left\{1\right\}×\left\{2\right\}\right)\cup \left(\left\{1\right\}×\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\}×\left\{2\right\}\right)\cup \left(\left\{1\right\}×\left\{7\right\}\right)=\left\{⟨1,2⟩,⟨1,7⟩\right\}$
15 5nn ${⊢}5\in ℕ$
16 15 elexi ${⊢}5\in \mathrm{V}$
17 16 7 xpsn ${⊢}\left\{5\right\}×\left\{2\right\}=\left\{⟨5,2⟩\right\}$
18 16 10 xpsn ${⊢}\left\{5\right\}×\left\{7\right\}=\left\{⟨5,7⟩\right\}$
19 17 18 uneq12i ${⊢}\left(\left\{5\right\}×\left\{2\right\}\right)\cup \left(\left\{5\right\}×\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\}×\left\{2\right\}\right)\cup \left(\left\{5\right\}×\left\{7\right\}\right)=\left\{⟨5,2⟩,⟨5,7⟩\right\}$
22 14 21 uneq12i ${⊢}\left(\left(\left\{1\right\}×\left\{2\right\}\right)\cup \left(\left\{1\right\}×\left\{7\right\}\right)\right)\cup \left(\left(\left\{5\right\}×\left\{2\right\}\right)\cup \left(\left\{5\right\}×\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\}×\left\{2,7\right\}=\left\{⟨1,2⟩,⟨1,7⟩\right\}\cup \left\{⟨5,2⟩,⟨5,7⟩\right\}$