ex-xp

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

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

Proof

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

Metamath Proof Explorer

Theorem ex-xp

Proof