Metamath Proof Explorer

Theorem hashssdif

Description: The size of the difference of a finite set and a subset is the set's size minus the subset's. (Contributed by Steve Rodriguez, 24-Oct-2015)

Ref Expression
Assertion hashssdif ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin )
2 diffi ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ 𝐵 ) ∈ Fin )
3 disjdif ⊢ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅
4 hashun ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝐴 ∖ 𝐵 ) ∈ Fin ∧ ( 𝐵 ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅ ) → ( ♯ ‘ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
5 3 4 mp3an3 ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝐴 ∖ 𝐵 ) ∈ Fin ) → ( ♯ ‘ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
6 1 2 5 syl2an ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ∈ Fin ) → ( ♯ ‘ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
7 6 anabss1 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → ( ♯ ‘ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
8 undif ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴 )
9 8 biimpi ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴 )
10 9 fveqeq2d ⊢ ( 𝐵 ⊆ 𝐴 → ( ( ♯ ‘ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ) ↔ ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ) ) )
11 10 adantl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → ( ( ♯ ‘ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ) ↔ ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ) ) )
12 7 11 mpbid ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ) )
13 12 eqcomd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ) = ( ♯ ‘ 𝐴 ) )
14 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
15 14 nn0cnd ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℂ )
16 hashcl ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
17 1 16 syl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
18 17 nn0cnd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → ( ♯ ‘ 𝐵 ) ∈ ℂ )
19 hashcl ⊢ ( ( 𝐴 ∖ 𝐵 ) ∈ Fin → ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℕ0 )
20 2 19 syl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℕ0 )
21 20 nn0cnd ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℂ )
22 subadd ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℂ ∧ ( ♯ ‘ 𝐵 ) ∈ ℂ ∧ ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ∈ ℂ ) → ( ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ 𝐵 ) ) = ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ↔ ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ) = ( ♯ ‘ 𝐴 ) ) )
23 15 18 21 22 syl3an ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝐴 ∈ Fin ) → ( ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ 𝐵 ) ) = ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ↔ ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ) = ( ♯ ‘ 𝐴 ) ) )
24 23 3anidm13 ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) ) → ( ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ 𝐵 ) ) = ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ↔ ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ) = ( ♯ ‘ 𝐴 ) ) )
25 24 anabss5 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → ( ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ 𝐵 ) ) = ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ↔ ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) ) = ( ♯ ‘ 𝐴 ) ) )
26 13 25 mpbird ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ 𝐵 ) ) = ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) )
27 26 eqcomd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) − ( ♯ ‘ 𝐵 ) ) )