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 } u. { 2 } )
2	1	fveq2i	|- ( # ` { 0 , 1 , 2 } ) = ( # ` ( { 0 , 1 } u. { 2 } ) )
3		prfi	|- { 0 , 1 } e. Fin
4		snfi	|- { 2 } e. Fin
5		2ne0	|- 2 =/= 0
6		1ne2	|- 1 =/= 2
7	6	necomi	|- 2 =/= 1
8	5 7	nelpri	|- -. 2 e. { 0 , 1 }
9		disjsn	|- ( ( { 0 , 1 } i^i { 2 } ) = (/) <-> -. 2 e. { 0 , 1 } )
10	8 9	mpbir	|- ( { 0 , 1 } i^i { 2 } ) = (/)
11		hashun	|- ( ( { 0 , 1 } e. Fin /\ { 2 } e. Fin /\ ( { 0 , 1 } i^i { 2 } ) = (/) ) -> ( # ` ( { 0 , 1 } u. { 2 } ) ) = ( ( # ` { 0 , 1 } ) + ( # ` { 2 } ) ) )
12	3 4 10 11	mp3an	|- ( # ` ( { 0 , 1 } u. { 2 } ) ) = ( ( # ` { 0 , 1 } ) + ( # ` { 2 } ) )
13	2 12	eqtri	|- ( # ` { 0 , 1 , 2 } ) = ( ( # ` { 0 , 1 } ) + ( # ` { 2 } ) )
14		prhash2ex	|- ( # ` { 0 , 1 } ) = 2
15		2z	|- 2 e. ZZ
16		hashsng	|- ( 2 e. ZZ -> ( # ` { 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