fz0to3un2pr

Description: An integer range from 0 to 3 is the union of two unordered pairs. (Contributed by AV, 7-Feb-2021)

		Ref	Expression
	Assertion	fz0to3un2pr	$⊢ (0 \dots 3) = \{0, 1\} \cup \{2, 3\}$

Step	Hyp	Ref	Expression
1		1nn0	$⊢ 1 \in ℕ_{0}$
2		3nn0	$⊢ 3 \in ℕ_{0}$
3		1le3	$⊢ 1 \leq 3$
4		elfz2nn0	$⊢ 1 \in (0 \dots 3) \leftrightarrow (1 \in ℕ_{0} \land 3 \in ℕ_{0} \land 1 \leq 3)$
5	1 2 3 4	mpbir3an	$⊢ 1 \in (0 \dots 3)$
6		fzsplit	$⊢ 1 \in (0 \dots 3) \to (0 \dots 3) = (0 \dots 1) \cup (1 + 1 \dots 3)$
7	5 6	ax-mp	$⊢ (0 \dots 3) = (0 \dots 1) \cup (1 + 1 \dots 3)$
8		1e0p1	$⊢ 1 = 0 + 1$
9	8	oveq2i	$⊢ (0 \dots 1) = (0 \dots 0 + 1)$
10		0z	$⊢ 0 \in ℤ$
11		fzpr	$⊢ 0 \in ℤ \to (0 \dots 0 + 1) = \{0, 0 + 1\}$
12	10 11	ax-mp	$⊢ (0 \dots 0 + 1) = \{0, 0 + 1\}$
13		0p1e1	$⊢ 0 + 1 = 1$
14	13	preq2i	$⊢ \{0, 0 + 1\} = \{0, 1\}$
15	9 12 14	3eqtri	$⊢ (0 \dots 1) = \{0, 1\}$
16		1p1e2	$⊢ 1 + 1 = 2$
17		df-3	$⊢ 3 = 2 + 1$
18	16 17	oveq12i	$⊢ (1 + 1 \dots 3) = (2 \dots 2 + 1)$
19		2z	$⊢ 2 \in ℤ$
20		fzpr	$⊢ 2 \in ℤ \to (2 \dots 2 + 1) = \{2, 2 + 1\}$
21	19 20	ax-mp	$⊢ (2 \dots 2 + 1) = \{2, 2 + 1\}$
22		2p1e3	$⊢ 2 + 1 = 3$
23	22	preq2i	$⊢ \{2, 2 + 1\} = \{2, 3\}$
24	18 21 23	3eqtri	$⊢ (1 + 1 \dots 3) = \{2, 3\}$
25	15 24	uneq12i	$⊢ (0 \dots 1) \cup (1 + 1 \dots 3) = \{0, 1\} \cup \{2, 3\}$
26	7 25	eqtri	$⊢ (0 \dots 3) = \{0, 1\} \cup \{2, 3\}$

Metamath Proof Explorer