Theorem ex-hash

Description: Example for df-hash . (Contributed by AV, 4-Sep-2021)

	Ref	Expression
Assertion	ex-hash	$$⊢\left|\left\{0,1,2\right\}\right|=3$$

Proof

Step	Hyp	Ref	Expression
1		df-tp	$$⊢\left\{0,1,2\right\}=\left\{0,1\right\}\cup \left\{2\right\}$$
2	1	fveq2i	$$⊢\left|\left\{0,1,2\right\}\right|=\left|\left\{0,1\right\}\cup \left\{2\right\}\right|$$
3		prfi	$$⊢\left\{0,1\right\}\in \mathrm{Fin}$$
4		snfi	$$⊢\left\{2\right\}\in \mathrm{Fin}$$
5		2ne0	$$⊢2\ne 0$$
6		1ne2	$$⊢1\ne 2$$
7	6	necomi	$$⊢2\ne 1$$
8	5 7	nelpri	$$⊢\neg 2\in \left\{0,1\right\}$$
9		disjsn	$$⊢\left\{0,1\right\}\cap \left\{2\right\}=\varnothing \leftrightarrow \neg 2\in \left\{0,1\right\}$$
10	8 9	mpbir	$$⊢\left\{0,1\right\}\cap \left\{2\right\}=\varnothing$$
11		hashun	$$⊢\left(\left\{0,1\right\}\in \mathrm{Fin}\wedge \left\{2\right\}\in \mathrm{Fin}\wedge \left\{0,1\right\}\cap \left\{2\right\}=\varnothing \right)\to \left|\left\{0,1\right\}\cup \left\{2\right\}\right|=\left|\left\{0,1\right\}\right|+\left|\left\{2\right\}\right|$$
12	3 4 10 11	mp3an	$$⊢\left|\left\{0,1\right\}\cup \left\{2\right\}\right|=\left|\left\{0,1\right\}\right|+\left|\left\{2\right\}\right|$$
13	2 12	eqtri	$$⊢\left|\left\{0,1,2\right\}\right|=\left|\left\{0,1\right\}\right|+\left|\left\{2\right\}\right|$$
14		prhash2ex	$$⊢\left|\left\{0,1\right\}\right|=2$$
15		2z	$$⊢2\in \mathbb{Z}$$
16		hashsng	$$⊢2\in \mathbb{Z}\to \left|\left\{2\right\}\right|=1$$
17	15 16	ax-mp	$$⊢\left|\left\{2\right\}\right|=1$$
18	14 17	oveq12i	$$⊢\left|\left\{0,1\right\}\right|+\left|\left\{2\right\}\right|=2+1$$
19		2p1e3	$$⊢2+1=3$$
20	18 19	eqtri	$$⊢\left|\left\{0,1\right\}\right|+\left|\left\{2\right\}\right|=3$$
21	13 20	eqtri	$$⊢\left|\left\{0,1,2\right\}\right|=3$$