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

Proof

Step Hyp Ref Expression
1 difpr ⊢ A ∖ B C = A ∖ B ∖ C
2 1 a1i ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → A ∖ B C = A ∖ B ∖ C
3 2 fveq2d ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → A ∖ B C = A ∖ B ∖ C
4 diffi ⊢ A ∈ Fin → A ∖ B ∈ Fin
5 necom ⊢ B ≠ C ↔ C ≠ B
6 5 biimpi ⊢ B ≠ C → C ≠ B
7 6 anim2i ⊢ C ∈ A ∧ B ≠ C → C ∈ A ∧ C ≠ B
8 7 3adant1 ⊢ B ∈ A ∧ C ∈ A ∧ B ≠ C → C ∈ A ∧ C ≠ B
9 8 adantl ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → C ∈ A ∧ C ≠ B
10 eldifsn ⊢ C ∈ A ∖ B ↔ C ∈ A ∧ C ≠ B
11 9 10 sylibr ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → C ∈ A ∖ B
12 hashdifsn ⊢ A ∖ B ∈ Fin ∧ C ∈ A ∖ B → A ∖ B ∖ C = A ∖ B − 1
13 4 11 12 syl2an2r ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → A ∖ B ∖ C = A ∖ B − 1
14 hashdifsn ⊢ A ∈ Fin ∧ B ∈ A → A ∖ B = A − 1
15 14 3ad2antr1 ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → A ∖ B = A − 1
16 15 oveq1d ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → A ∖ B − 1 = A - 1 - 1
17 hashcl ⊢ A ∈ Fin → A ∈ ℕ 0
18 17 nn0cnd ⊢ A ∈ Fin → A ∈ ℂ
19 sub1m1 ⊢ A ∈ ℂ → A - 1 - 1 = A − 2
20 18 19 syl ⊢ A ∈ Fin → A - 1 - 1 = A − 2
21 20 adantr ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → A - 1 - 1 = A − 2
22 16 21 eqtrd ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → A ∖ B − 1 = A − 2
23 3 13 22 3eqtrd ⊢ A ∈ Fin ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → A ∖ B C = A − 2