Metamath Proof Explorer

Theorem hashdifpr

Description: The size of the difference of a finite set and a proper ordered pair subset 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 ) )