Theorem hashunsng

Description: The size of the union of a finite set with a disjoint singleton is one more than the size of the set. (Contributed by Paul Chapman, 30-Nov-2012)

	Ref	Expression
Assertion	hashunsng	|- ( B e. V -> ( ( A e. Fin /\ -. B e. A ) -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		disjsn	|- ( ( A i^i { B } ) = (/) <-> -. B e. A )
2		snfi	|- { B } e. Fin
3		hashun	|- ( ( A e. Fin /\ { B } e. Fin /\ ( A i^i { B } ) = (/) ) -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) + ( # ` { B } ) ) )
4	2 3	mp3an2	|- ( ( A e. Fin /\ ( A i^i { B } ) = (/) ) -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) + ( # ` { B } ) ) )
5	1 4	sylan2br	|- ( ( A e. Fin /\ -. B e. A ) -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) + ( # ` { B } ) ) )
6		hashsng	|- ( B e. V -> ( # ` { B } ) = 1 )
7	6	oveq2d	|- ( B e. V -> ( ( # ` A ) + ( # ` { B } ) ) = ( ( # ` A ) + 1 ) )
8	5 7	sylan9eq	|- ( ( ( A e. Fin /\ -. B e. A ) /\ B e. V ) -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) + 1 ) )
9	8	expcom	|- ( B e. V -> ( ( A e. Fin /\ -. B e. A ) -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) + 1 ) ) )