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 ( 𝐵 ∈ 𝑉 → ( ( 𝐴 ∈ 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 ) ) )