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