This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ex-hash

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

Ref Expression
Assertion ex-hash ⊢ 0 1 2 = 3

Proof

Step Hyp Ref Expression
1 df-tp ⊢ 0 1 2 = 0 1 ∪ 2
2 1 fveq2i ⊢ 0 1 2 = 0 1 ∪ 2
3 prfi ⊢ 0 1 ∈ Fin
4 snfi ⊢ 2 ∈ Fin
5 2ne0 ⊢ 2 ≠ 0
6 1ne2 ⊢ 1 ≠ 2
7 6 necomi ⊢ 2 ≠ 1
8 5 7 nelpri ⊢ ¬ 2 ∈ 0 1
9 disjsn ⊢ 0 1 ∩ 2 = ∅ ↔ ¬ 2 ∈ 0 1
10 8 9 mpbir ⊢ 0 1 ∩ 2 = ∅
11 hashun ⊢ 0 1 ∈ Fin ∧ 2 ∈ Fin ∧ 0 1 ∩ 2 = ∅ → 0 1 ∪ 2 = 0 1 + 2
12 3 4 10 11 mp3an ⊢ 0 1 ∪ 2 = 0 1 + 2
13 2 12 eqtri ⊢ 0 1 2 = 0 1 + 2
14 prhash2ex ⊢ 0 1 = 2
15 2z ⊢ 2 ∈ ℤ
16 hashsng ⊢ 2 ∈ ℤ → 2 = 1
17 15 16 ax-mp ⊢ 2 = 1
18 14 17 oveq12i ⊢ 0 1 + 2 = 2 + 1
19 2p1e3 ⊢ 2 + 1 = 3
20 18 19 eqtri ⊢ 0 1 + 2 = 3
21 13 20 eqtri ⊢ 0 1 2 = 3