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

Metamath Proof Explorer

Theorem hashdifsn

Description: The size of the difference of a finite set and a singleton subset is the set's size minus 1. (Contributed by Alexander van der Vekens, 6-Jan-2018)

Ref Expression
Assertion hashdifsn ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )

Proof

Step Hyp Ref Expression
1 snssi ⊢ ( 𝐵 ∈ 𝐴 → { 𝐵 } ⊆ 𝐴 )
2 hashssdif ⊢ ( ( 𝐴 ∈ Fin ∧ { 𝐵 } ⊆ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ { 𝐵 } ) ) )
3 1 2 sylan2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ { 𝐵 } ) ) )
4 hashsng ⊢ ( 𝐵 ∈ 𝐴 → ( ♯ ‘ { 𝐵 } ) = 1 )
5 4 adantl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ { 𝐵 } ) = 1 )
6 5 oveq2d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴 ) → ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
7 3 6 eqtrd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )