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