Metamath Proof Explorer

Theorem hash2iun1dif1

Description: The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022)

Ref Expression
Hypotheses hash2iun1dif1.a ⊢ φ → A ∈ Fin
hash2iun1dif1.b ⊢ B = A ∖ x
hash2iun1dif1.c ⊢ φ ∧ x ∈ A ∧ y ∈ B → C ∈ Fin
hash2iun1dif1.da ⊢ φ → Disj x ∈ A ⋃ y ∈ B C
hash2iun1dif1.db ⊢ φ ∧ x ∈ A → Disj y ∈ B C
hash2iun1dif1.1 ⊢ φ ∧ x ∈ A ∧ y ∈ B → C = 1
Assertion hash2iun1dif1 ⊢ φ → ⋃ x ∈ A ⋃ y ∈ B C = A ⁢ A − 1

Proof

Step Hyp Ref Expression
1 hash2iun1dif1.a ⊢ φ → A ∈ Fin
2 hash2iun1dif1.b ⊢ B = A ∖ x
3 hash2iun1dif1.c ⊢ φ ∧ x ∈ A ∧ y ∈ B → C ∈ Fin
4 hash2iun1dif1.da ⊢ φ → Disj x ∈ A ⋃ y ∈ B C
5 hash2iun1dif1.db ⊢ φ ∧ x ∈ A → Disj y ∈ B C
6 hash2iun1dif1.1 ⊢ φ ∧ x ∈ A ∧ y ∈ B → C = 1
7 diffi ⊢ A ∈ Fin → A ∖ x ∈ Fin
8 1 7 syl ⊢ φ → A ∖ x ∈ Fin
9 8 adantr ⊢ φ ∧ x ∈ A → A ∖ x ∈ Fin
10 2 9 eqeltrid ⊢ φ ∧ x ∈ A → B ∈ Fin
11 1 10 3 4 5 hash2iun ⊢ φ → ⋃ x ∈ A ⋃ y ∈ B C = ∑ x ∈ A ∑ y ∈ B C
12 6 2sumeq2dv ⊢ φ → ∑ x ∈ A ∑ y ∈ B C = ∑ x ∈ A ∑ y ∈ B 1
13 1cnd ⊢ φ ∧ x ∈ A → 1 ∈ ℂ
14 fsumconst ⊢ B ∈ Fin ∧ 1 ∈ ℂ → ∑ y ∈ B 1 = B ⋅ 1
15 10 13 14 syl2anc ⊢ φ ∧ x ∈ A → ∑ y ∈ B 1 = B ⋅ 1
16 15 sumeq2dv ⊢ φ → ∑ x ∈ A ∑ y ∈ B 1 = ∑ x ∈ A B ⋅ 1
17 2 a1i ⊢ φ ∧ x ∈ A → B = A ∖ x
18 17 fveq2d ⊢ φ ∧ x ∈ A → B = A ∖ x
19 hashdifsn ⊢ A ∈ Fin ∧ x ∈ A → A ∖ x = A − 1
20 1 19 sylan ⊢ φ ∧ x ∈ A → A ∖ x = A − 1
21 18 20 eqtrd ⊢ φ ∧ x ∈ A → B = A − 1
22 21 oveq1d ⊢ φ ∧ x ∈ A → B ⋅ 1 = A − 1 ⋅ 1
23 22 sumeq2dv ⊢ φ → ∑ x ∈ A B ⋅ 1 = ∑ x ∈ A A − 1 ⋅ 1
24 hashcl ⊢ A ∈ Fin → A ∈ ℕ 0
25 1 24 syl ⊢ φ → A ∈ ℕ 0
26 25 nn0cnd ⊢ φ → A ∈ ℂ
27 peano2cnm ⊢ A ∈ ℂ → A − 1 ∈ ℂ
28 26 27 syl ⊢ φ → A − 1 ∈ ℂ
29 28 mulridd ⊢ φ → A − 1 ⋅ 1 = A − 1
30 29 sumeq2sdv ⊢ φ → ∑ x ∈ A A − 1 ⋅ 1 = ∑ x ∈ A A − 1
31 fsumconst ⊢ A ∈ Fin ∧ A − 1 ∈ ℂ → ∑ x ∈ A A − 1 = A ⁢ A − 1
32 1 28 31 syl2anc ⊢ φ → ∑ x ∈ A A − 1 = A ⁢ A − 1
33 30 32 eqtrd ⊢ φ → ∑ x ∈ A A − 1 ⋅ 1 = A ⁢ A − 1
34 16 23 33 3eqtrd ⊢ φ → ∑ x ∈ A ∑ y ∈ B 1 = A ⁢ A − 1
35 11 12 34 3eqtrd ⊢ φ → ⋃ x ∈ A ⋃ y ∈ B C = A ⁢ A − 1