This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )