Metamath Proof Explorer


Theorem hashdifpr

Description: The size of the difference of a finite set and a proper pair of its elements is the set's size minus 2. (Contributed by AV, 16-Dec-2020)

Ref Expression
Assertion hashdifpr ( ( 𝐴 ∈ Fin ∧ ( 𝐵𝐴𝐶𝐴𝐵𝐶 ) ) → ( ♯ ‘ ( 𝐴 ∖ { 𝐵 , 𝐶 } ) ) = ( ( ♯ ‘ 𝐴 ) − 2 ) )

Proof

Step Hyp Ref Expression
1 difpr ( 𝐴 ∖ { 𝐵 , 𝐶 } ) = ( ( 𝐴 ∖ { 𝐵 } ) ∖ { 𝐶 } )
2 1 a1i ( ( 𝐴 ∈ Fin ∧ ( 𝐵𝐴𝐶𝐴𝐵𝐶 ) ) → ( 𝐴 ∖ { 𝐵 , 𝐶 } ) = ( ( 𝐴 ∖ { 𝐵 } ) ∖ { 𝐶 } ) )
3 2 fveq2d ( ( 𝐴 ∈ Fin ∧ ( 𝐵𝐴𝐶𝐴𝐵𝐶 ) ) → ( ♯ ‘ ( 𝐴 ∖ { 𝐵 , 𝐶 } ) ) = ( ♯ ‘ ( ( 𝐴 ∖ { 𝐵 } ) ∖ { 𝐶 } ) ) )
4 diffi ( 𝐴 ∈ Fin → ( 𝐴 ∖ { 𝐵 } ) ∈ Fin )
5 necom ( 𝐵𝐶𝐶𝐵 )
6 5 biimpi ( 𝐵𝐶𝐶𝐵 )
7 6 anim2i ( ( 𝐶𝐴𝐵𝐶 ) → ( 𝐶𝐴𝐶𝐵 ) )
8 7 3adant1 ( ( 𝐵𝐴𝐶𝐴𝐵𝐶 ) → ( 𝐶𝐴𝐶𝐵 ) )
9 8 adantl ( ( 𝐴 ∈ Fin ∧ ( 𝐵𝐴𝐶𝐴𝐵𝐶 ) ) → ( 𝐶𝐴𝐶𝐵 ) )
10 eldifsn ( 𝐶 ∈ ( 𝐴 ∖ { 𝐵 } ) ↔ ( 𝐶𝐴𝐶𝐵 ) )
11 9 10 sylibr ( ( 𝐴 ∈ Fin ∧ ( 𝐵𝐴𝐶𝐴𝐵𝐶 ) ) → 𝐶 ∈ ( 𝐴 ∖ { 𝐵 } ) )
12 hashdifsn ( ( ( 𝐴 ∖ { 𝐵 } ) ∈ Fin ∧ 𝐶 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ♯ ‘ ( ( 𝐴 ∖ { 𝐵 } ) ∖ { 𝐶 } ) ) = ( ( ♯ ‘ ( 𝐴 ∖ { 𝐵 } ) ) − 1 ) )
13 4 11 12 syl2an2r ( ( 𝐴 ∈ Fin ∧ ( 𝐵𝐴𝐶𝐴𝐵𝐶 ) ) → ( ♯ ‘ ( ( 𝐴 ∖ { 𝐵 } ) ∖ { 𝐶 } ) ) = ( ( ♯ ‘ ( 𝐴 ∖ { 𝐵 } ) ) − 1 ) )
14 hashdifsn ( ( 𝐴 ∈ Fin ∧ 𝐵𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
15 14 3ad2antr1 ( ( 𝐴 ∈ Fin ∧ ( 𝐵𝐴𝐶𝐴𝐵𝐶 ) ) → ( ♯ ‘ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
16 15 oveq1d ( ( 𝐴 ∈ Fin ∧ ( 𝐵𝐴𝐶𝐴𝐵𝐶 ) ) → ( ( ♯ ‘ ( 𝐴 ∖ { 𝐵 } ) ) − 1 ) = ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) )
17 hashcl ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
18 17 nn0cnd ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℂ )
19 sub1m1 ( ( ♯ ‘ 𝐴 ) ∈ ℂ → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) = ( ( ♯ ‘ 𝐴 ) − 2 ) )
20 18 19 syl ( 𝐴 ∈ Fin → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) = ( ( ♯ ‘ 𝐴 ) − 2 ) )
21 20 adantr ( ( 𝐴 ∈ Fin ∧ ( 𝐵𝐴𝐶𝐴𝐵𝐶 ) ) → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) = ( ( ♯ ‘ 𝐴 ) − 2 ) )
22 16 21 eqtrd ( ( 𝐴 ∈ Fin ∧ ( 𝐵𝐴𝐶𝐴𝐵𝐶 ) ) → ( ( ♯ ‘ ( 𝐴 ∖ { 𝐵 } ) ) − 1 ) = ( ( ♯ ‘ 𝐴 ) − 2 ) )
23 3 13 22 3eqtrd ( ( 𝐴 ∈ Fin ∧ ( 𝐵𝐴𝐶𝐴𝐵𝐶 ) ) → ( ♯ ‘ ( 𝐴 ∖ { 𝐵 , 𝐶 } ) ) = ( ( ♯ ‘ 𝐴 ) − 2 ) )