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 ⊢ A ∈ Fin ∧ B ⊆ A → A ∖ B = A − B

Proof

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