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	⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		disjsn	⊢ ( ( 𝐴 ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ 𝐴 )
2		snfi	⊢ { 𝐵 } ∈ Fin
3		hashun	⊢ ( ( 𝐴 ∈ Fin ∧ { 𝐵 } ∈ Fin ∧ ( 𝐴 ∩ { 𝐵 } ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ { 𝐵 } ) ) )
4	2 3	mp3an2	⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐴 ∩ { 𝐵 } ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ { 𝐵 } ) ) )
5	1 4	sylan2br	⊢ ( ( 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ { 𝐵 } ) ) )
6		hashsng	⊢ ( 𝐵 ∈ 𝑉 → ( ♯ ‘ { 𝐵 } ) = 1 )
7	6	oveq2d	⊢ ( 𝐵 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) + 1 ) )
8	5 7	sylan9eq	⊢ ( ( ( 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ 𝐴 ) ∧ 𝐵 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) + 1 ) )
9	8	expcom	⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) + 1 ) ) )