# Metamath Proof Explorer

## 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 ${⊢}¬2\in \left\{0,1\right\}$
9 disjsn ${⊢}\left\{0,1\right\}\cap \left\{2\right\}=\varnothing ↔¬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 ℤ$
16 hashsng ${⊢}2\in ℤ\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$