Theorem 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	$$⊢\left(0\dots 3\right)=\left\{0,1\right\}\cup \left\{2,3\right\}$$

Proof

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