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