Proof of Theorem hasheuni
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nfdisj1 5124 | . . . . . . . 8
⊢
Ⅎ𝑥Disj
𝑥 ∈ 𝐴 𝑥 | 
| 2 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑥 𝐴 ∈ Fin | 
| 3 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑥 𝐴 ⊆ Fin | 
| 4 | 1, 2, 3 | nf3an 1901 | . . . . . . 7
⊢
Ⅎ𝑥(Disj
𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) | 
| 5 |  | simp2 1138 | . . . . . . 7
⊢
((Disj 𝑥
∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin) | 
| 6 |  | simp3 1139 | . . . . . . 7
⊢
((Disj 𝑥
∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ⊆ Fin) | 
| 7 |  | simp1 1137 | . . . . . . 7
⊢
((Disj 𝑥
∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Disj 𝑥 ∈ 𝐴 𝑥) | 
| 8 | 4, 5, 6, 7 | hashunif 32810 | . . . . . 6
⊢
((Disj 𝑥
∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) =
Σ𝑥 ∈ 𝐴 (♯‘𝑥)) | 
| 9 |  | simpl 482 | . . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin) | 
| 10 |  | dfss3 3972 | . . . . . . . . . . 11
⊢ (𝐴 ⊆ Fin ↔
∀𝑥 ∈ 𝐴 𝑥 ∈ Fin) | 
| 11 |  | hashcl 14395 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ Fin →
(♯‘𝑥) ∈
ℕ0) | 
| 12 |  | nn0re 12535 | . . . . . . . . . . . . . 14
⊢
((♯‘𝑥)
∈ ℕ0 → (♯‘𝑥) ∈ ℝ) | 
| 13 |  | nn0ge0 12551 | . . . . . . . . . . . . . 14
⊢
((♯‘𝑥)
∈ ℕ0 → 0 ≤ (♯‘𝑥)) | 
| 14 |  | elrege0 13494 | . . . . . . . . . . . . . 14
⊢
((♯‘𝑥)
∈ (0[,)+∞) ↔ ((♯‘𝑥) ∈ ℝ ∧ 0 ≤
(♯‘𝑥))) | 
| 15 | 12, 13, 14 | sylanbrc 583 | . . . . . . . . . . . . 13
⊢
((♯‘𝑥)
∈ ℕ0 → (♯‘𝑥) ∈ (0[,)+∞)) | 
| 16 | 11, 15 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ Fin →
(♯‘𝑥) ∈
(0[,)+∞)) | 
| 17 | 16 | ralimi 3083 | . . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 𝑥 ∈ Fin → ∀𝑥 ∈ 𝐴 (♯‘𝑥) ∈ (0[,)+∞)) | 
| 18 | 10, 17 | sylbi 217 | . . . . . . . . . 10
⊢ (𝐴 ⊆ Fin →
∀𝑥 ∈ 𝐴 (♯‘𝑥) ∈
(0[,)+∞)) | 
| 19 | 18 | r19.21bi 3251 | . . . . . . . . 9
⊢ ((𝐴 ⊆ Fin ∧ 𝑥 ∈ 𝐴) → (♯‘𝑥) ∈ (0[,)+∞)) | 
| 20 | 19 | adantll 714 | . . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑥 ∈ 𝐴) → (♯‘𝑥) ∈ (0[,)+∞)) | 
| 21 | 9, 20 | esumpfinval 34076 | . . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ*𝑥 ∈
𝐴(♯‘𝑥) = Σ𝑥 ∈ 𝐴 (♯‘𝑥)) | 
| 22 | 21 | 3adant1 1131 | . . . . . 6
⊢
((Disj 𝑥
∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ*𝑥 ∈
𝐴(♯‘𝑥) = Σ𝑥 ∈ 𝐴 (♯‘𝑥)) | 
| 23 | 8, 22 | eqtr4d 2780 | . . . . 5
⊢
((Disj 𝑥
∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) =
Σ*𝑥 ∈
𝐴(♯‘𝑥)) | 
| 24 | 23 | 3adant1l 1177 | . . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) =
Σ*𝑥 ∈
𝐴(♯‘𝑥)) | 
| 25 | 24 | 3expa 1119 | . . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) ∧ 𝐴 ∈ Fin) ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) =
Σ*𝑥 ∈
𝐴(♯‘𝑥)) | 
| 26 |  | uniexg 7760 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | 
| 27 | 10 | notbii 320 | . . . . . . . . . 10
⊢ (¬
𝐴 ⊆ Fin ↔ ¬
∀𝑥 ∈ 𝐴 𝑥 ∈ Fin) | 
| 28 |  | rexnal 3100 | . . . . . . . . . 10
⊢
(∃𝑥 ∈
𝐴 ¬ 𝑥 ∈ Fin ↔ ¬ ∀𝑥 ∈ 𝐴 𝑥 ∈ Fin) | 
| 29 | 27, 28 | bitr4i 278 | . . . . . . . . 9
⊢ (¬
𝐴 ⊆ Fin ↔
∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ Fin) | 
| 30 |  | elssuni 4937 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴) | 
| 31 |  | ssfi 9213 | . . . . . . . . . . . . 13
⊢ ((∪ 𝐴
∈ Fin ∧ 𝑥 ⊆
∪ 𝐴) → 𝑥 ∈ Fin) | 
| 32 | 31 | expcom 413 | . . . . . . . . . . . 12
⊢ (𝑥 ⊆ ∪ 𝐴
→ (∪ 𝐴 ∈ Fin → 𝑥 ∈ Fin)) | 
| 33 | 32 | con3d 152 | . . . . . . . . . . 11
⊢ (𝑥 ⊆ ∪ 𝐴
→ (¬ 𝑥 ∈ Fin
→ ¬ ∪ 𝐴 ∈ Fin)) | 
| 34 | 30, 33 | syl 17 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → (¬ 𝑥 ∈ Fin → ¬ ∪ 𝐴
∈ Fin)) | 
| 35 | 34 | rexlimiv 3148 | . . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 ¬ 𝑥 ∈ Fin → ¬ ∪ 𝐴
∈ Fin) | 
| 36 | 29, 35 | sylbi 217 | . . . . . . . 8
⊢ (¬
𝐴 ⊆ Fin → ¬
∪ 𝐴 ∈ Fin) | 
| 37 |  | hashinf 14374 | . . . . . . . 8
⊢ ((∪ 𝐴
∈ V ∧ ¬ ∪ 𝐴 ∈ Fin) → (♯‘∪ 𝐴) =
+∞) | 
| 38 | 26, 36, 37 | syl2an 596 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) =
+∞) | 
| 39 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑥 ∈ V | 
| 40 |  | hashinf 14374 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ V ∧ ¬ 𝑥 ∈ Fin) →
(♯‘𝑥) =
+∞) | 
| 41 | 39, 40 | mpan 690 | . . . . . . . . . 10
⊢ (¬
𝑥 ∈ Fin →
(♯‘𝑥) =
+∞) | 
| 42 | 41 | reximi 3084 | . . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 ¬ 𝑥 ∈ Fin → ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞) | 
| 43 | 29, 42 | sylbi 217 | . . . . . . . 8
⊢ (¬
𝐴 ⊆ Fin →
∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞) | 
| 44 |  | nfv 1914 | . . . . . . . . . 10
⊢
Ⅎ𝑥 𝐴 ∈ 𝑉 | 
| 45 |  | nfre1 3285 | . . . . . . . . . 10
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞ | 
| 46 | 44, 45 | nfan 1899 | . . . . . . . . 9
⊢
Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞) | 
| 47 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞) → 𝐴 ∈ 𝑉) | 
| 48 |  | hashf2 34085 | . . . . . . . . . . 11
⊢
♯:V⟶(0[,]+∞) | 
| 49 |  | ffvelcdm 7101 | . . . . . . . . . . 11
⊢
((♯:V⟶(0[,]+∞) ∧ 𝑥 ∈ V) → (♯‘𝑥) ∈
(0[,]+∞)) | 
| 50 | 48, 39, 49 | mp2an 692 | . . . . . . . . . 10
⊢
(♯‘𝑥)
∈ (0[,]+∞) | 
| 51 | 50 | a1i 11 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞) ∧ 𝑥 ∈ 𝐴) → (♯‘𝑥) ∈ (0[,]+∞)) | 
| 52 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞) → ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞) | 
| 53 | 46, 47, 51, 52 | esumpinfval 34074 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞) → Σ*𝑥 ∈ 𝐴(♯‘𝑥) = +∞) | 
| 54 | 43, 53 | sylan2 593 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ⊆ Fin) →
Σ*𝑥 ∈
𝐴(♯‘𝑥) = +∞) | 
| 55 | 38, 54 | eqtr4d 2780 | . . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) =
Σ*𝑥 ∈
𝐴(♯‘𝑥)) | 
| 56 | 55 | 3adant2 1132 | . . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ Fin ∧ ¬ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) =
Σ*𝑥 ∈
𝐴(♯‘𝑥)) | 
| 57 | 56 | 3adant1r 1178 | . . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) ∧ 𝐴 ∈ Fin ∧ ¬ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) =
Σ*𝑥 ∈
𝐴(♯‘𝑥)) | 
| 58 | 57 | 3expa 1119 | . . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) ∧ 𝐴 ∈ Fin) ∧ ¬ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) =
Σ*𝑥 ∈
𝐴(♯‘𝑥)) | 
| 59 | 25, 58 | pm2.61dan 813 | . 2
⊢ (((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) ∧ 𝐴 ∈ Fin) → (♯‘∪ 𝐴) =
Σ*𝑥 ∈
𝐴(♯‘𝑥)) | 
| 60 |  | pwfi 9357 | . . . . . . 7
⊢ (∪ 𝐴
∈ Fin ↔ 𝒫 ∪ 𝐴 ∈ Fin) | 
| 61 |  | pwuni 4945 | . . . . . . . 8
⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴 | 
| 62 |  | ssfi 9213 | . . . . . . . 8
⊢
((𝒫 ∪ 𝐴 ∈ Fin ∧ 𝐴 ⊆ 𝒫 ∪ 𝐴)
→ 𝐴 ∈
Fin) | 
| 63 | 61, 62 | mpan2 691 | . . . . . . 7
⊢
(𝒫 ∪ 𝐴 ∈ Fin → 𝐴 ∈ Fin) | 
| 64 | 60, 63 | sylbi 217 | . . . . . 6
⊢ (∪ 𝐴
∈ Fin → 𝐴 ∈
Fin) | 
| 65 | 64 | con3i 154 | . . . . 5
⊢ (¬
𝐴 ∈ Fin → ¬
∪ 𝐴 ∈ Fin) | 
| 66 | 26, 65, 37 | syl2an 596 | . . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘∪ 𝐴) =
+∞) | 
| 67 |  | nftru 1804 | . . . . . . . . 9
⊢
Ⅎ𝑥⊤ | 
| 68 |  | unrab 4315 | . . . . . . . . . . 11
⊢ ({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) = {𝑥 ∈ 𝐴 ∣ ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)} | 
| 69 |  | exmid 895 | . . . . . . . . . . . . 13
⊢
((♯‘𝑥) =
0 ∨ ¬ (♯‘𝑥) = 0) | 
| 70 | 69 | rgenw 3065 | . . . . . . . . . . . 12
⊢
∀𝑥 ∈
𝐴 ((♯‘𝑥) = 0 ∨ ¬
(♯‘𝑥) =
0) | 
| 71 |  | rabid2 3470 | . . . . . . . . . . . 12
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)} ↔ ∀𝑥 ∈ 𝐴 ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)) | 
| 72 | 70, 71 | mpbir 231 | . . . . . . . . . . 11
⊢ 𝐴 = {𝑥 ∈ 𝐴 ∣ ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)} | 
| 73 | 68, 72 | eqtr4i 2768 | . . . . . . . . . 10
⊢ ({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) = 𝐴 | 
| 74 | 73 | a1i 11 | . . . . . . . . 9
⊢ (⊤
→ ({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) = 𝐴) | 
| 75 | 67, 74 | esumeq1d 34036 | . . . . . . . 8
⊢ (⊤
→ Σ*𝑥
∈ ({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0})(♯‘𝑥) = Σ*𝑥 ∈ 𝐴(♯‘𝑥)) | 
| 76 | 75 | mptru 1547 | . . . . . . 7
⊢
Σ*𝑥
∈ ({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0})(♯‘𝑥) = Σ*𝑥 ∈ 𝐴(♯‘𝑥) | 
| 77 |  | nfrab1 3457 | . . . . . . . 8
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} | 
| 78 |  | nfrab1 3457 | . . . . . . . 8
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} | 
| 79 |  | rabexg 5337 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∈ V) | 
| 80 |  | rabexg 5337 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈
V) | 
| 81 |  | rabnc 4391 | . . . . . . . . 9
⊢ ({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∩ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) =
∅ | 
| 82 | 81 | a1i 11 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∩ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) =
∅) | 
| 83 | 50 | a1i 11 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0}) → (♯‘𝑥) ∈
(0[,]+∞)) | 
| 84 | 50 | a1i 11 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) →
(♯‘𝑥) ∈
(0[,]+∞)) | 
| 85 | 44, 77, 78, 79, 80, 82, 83, 84 | esumsplit 34054 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → Σ*𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0})(♯‘𝑥) = (Σ*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒
Σ*𝑥 ∈
{𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥))) | 
| 86 | 76, 85 | eqtr3id 2791 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → Σ*𝑥 ∈ 𝐴(♯‘𝑥) = (Σ*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒
Σ*𝑥 ∈
{𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥))) | 
| 87 | 86 | adantr 480 | . . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥 ∈ 𝐴(♯‘𝑥) = (Σ*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒
Σ*𝑥 ∈
{𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥))) | 
| 88 |  | nfv 1914 | . . . . . . 7
⊢
Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) | 
| 89 | 80 | adantr 480 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈
V) | 
| 90 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ 𝐴 ∈ Fin) | 
| 91 |  | dfrab3 4319 | . . . . . . . . . . . 12
⊢ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} = (𝐴 ∩ {𝑥 ∣ (♯‘𝑥) = 0}) | 
| 92 |  | hasheq0 14402 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ V →
((♯‘𝑥) = 0
↔ 𝑥 =
∅)) | 
| 93 | 39, 92 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢
((♯‘𝑥) =
0 ↔ 𝑥 =
∅) | 
| 94 | 93 | abbii 2809 | . . . . . . . . . . . . . 14
⊢ {𝑥 ∣ (♯‘𝑥) = 0} = {𝑥 ∣ 𝑥 = ∅} | 
| 95 |  | df-sn 4627 | . . . . . . . . . . . . . 14
⊢ {∅}
= {𝑥 ∣ 𝑥 = ∅} | 
| 96 | 94, 95 | eqtr4i 2768 | . . . . . . . . . . . . 13
⊢ {𝑥 ∣ (♯‘𝑥) = 0} =
{∅} | 
| 97 | 96 | ineq2i 4217 | . . . . . . . . . . . 12
⊢ (𝐴 ∩ {𝑥 ∣ (♯‘𝑥) = 0}) = (𝐴 ∩ {∅}) | 
| 98 | 91, 97 | eqtri 2765 | . . . . . . . . . . 11
⊢ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} = (𝐴 ∩ {∅}) | 
| 99 |  | snfi 9083 | . . . . . . . . . . . 12
⊢ {∅}
∈ Fin | 
| 100 |  | inss2 4238 | . . . . . . . . . . . 12
⊢ (𝐴 ∩ {∅}) ⊆
{∅} | 
| 101 |  | ssfi 9213 | . . . . . . . . . . . 12
⊢
(({∅} ∈ Fin ∧ (𝐴 ∩ {∅}) ⊆ {∅}) →
(𝐴 ∩ {∅}) ∈
Fin) | 
| 102 | 99, 100, 101 | mp2an 692 | . . . . . . . . . . 11
⊢ (𝐴 ∩ {∅}) ∈
Fin | 
| 103 | 98, 102 | eqeltri 2837 | . . . . . . . . . 10
⊢ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∈ Fin | 
| 104 | 103 | a1i 11 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∈ Fin) | 
| 105 |  | difinf 9349 | . . . . . . . . 9
⊢ ((¬
𝐴 ∈ Fin ∧ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∈ Fin) → ¬ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0}) ∈ Fin) | 
| 106 | 90, 104, 105 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0}) ∈ Fin) | 
| 107 |  | notrab 4322 | . . . . . . . . 9
⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0}) = {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} | 
| 108 | 107 | eleq1i 2832 | . . . . . . . 8
⊢ ((𝐴 ∖ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0}) ∈ Fin ↔ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈
Fin) | 
| 109 | 106, 108 | sylnib 328 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈
Fin) | 
| 110 | 50 | a1i 11 | . . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) →
(♯‘𝑥) ∈
(0[,]+∞)) | 
| 111 | 39 | a1i 11 | . . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 𝑥 ∈ V) | 
| 112 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) | 
| 113 |  | rabid 3458 | . . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} ↔ (𝑥 ∈ 𝐴 ∧ ¬ (♯‘𝑥) = 0)) | 
| 114 | 112, 113 | sylib 218 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) → (𝑥 ∈ 𝐴 ∧ ¬ (♯‘𝑥) = 0)) | 
| 115 | 114 | simprd 495 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) → ¬
(♯‘𝑥) =
0) | 
| 116 | 93 | biimpri 228 | . . . . . . . . . 10
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
0) | 
| 117 | 116 | necon3bi 2967 | . . . . . . . . 9
⊢ (¬
(♯‘𝑥) = 0
→ 𝑥 ≠
∅) | 
| 118 | 115, 117 | syl 17 | . . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 𝑥 ≠ ∅) | 
| 119 |  | hashge1 14428 | . . . . . . . 8
⊢ ((𝑥 ∈ V ∧ 𝑥 ≠ ∅) → 1 ≤
(♯‘𝑥)) | 
| 120 | 111, 118,
119 | syl2anc 584 | . . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 1 ≤
(♯‘𝑥)) | 
| 121 |  | 1xr 11320 | . . . . . . . 8
⊢ 1 ∈
ℝ* | 
| 122 | 121 | a1i 11 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → 1 ∈
ℝ*) | 
| 123 |  | 0lt1 11785 | . . . . . . . 8
⊢ 0 <
1 | 
| 124 | 123 | a1i 11 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → 0 <
1) | 
| 125 | 88, 78, 89, 109, 110, 120, 122, 124 | esumpinfsum 34078 | . . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥) = +∞) | 
| 126 | 125 | oveq2d 7447 | . . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) →
(Σ*𝑥
∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒
Σ*𝑥 ∈
{𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥)) = (Σ*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒
+∞)) | 
| 127 |  | iccssxr 13470 | . . . . . . 7
⊢
(0[,]+∞) ⊆ ℝ* | 
| 128 | 79 | adantr 480 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∈ V) | 
| 129 | 50 | a1i 11 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0}) → (♯‘𝑥) ∈
(0[,]+∞)) | 
| 130 | 129 | ralrimiva 3146 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ∀𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞)) | 
| 131 | 77 | esumcl 34031 | . . . . . . . 8
⊢ (({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∈ V ∧ ∀𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞)) →
Σ*𝑥 ∈
{𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞)) | 
| 132 | 128, 130,
131 | syl2anc 584 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞)) | 
| 133 | 127, 132 | sselid 3981 | . . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈
ℝ*) | 
| 134 |  | xrge0neqmnf 13492 | . . . . . . 7
⊢
(Σ*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞) →
Σ*𝑥 ∈
{𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ≠ -∞) | 
| 135 | 132, 134 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ≠ -∞) | 
| 136 |  | xaddpnf1 13268 | . . . . . 6
⊢
((Σ*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ ℝ* ∧
Σ*𝑥 ∈
{𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ≠ -∞) →
(Σ*𝑥
∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒
+∞) = +∞) | 
| 137 | 133, 135,
136 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) →
(Σ*𝑥
∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒
+∞) = +∞) | 
| 138 | 87, 126, 137 | 3eqtrd 2781 | . . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥 ∈ 𝐴(♯‘𝑥) = +∞) | 
| 139 | 66, 138 | eqtr4d 2780 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘∪ 𝐴) =
Σ*𝑥 ∈
𝐴(♯‘𝑥)) | 
| 140 | 139 | adantlr 715 | . 2
⊢ (((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) ∧ ¬ 𝐴 ∈ Fin) → (♯‘∪ 𝐴) =
Σ*𝑥 ∈
𝐴(♯‘𝑥)) | 
| 141 | 59, 140 | pm2.61dan 813 | 1
⊢ ((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) → (♯‘∪ 𝐴) =
Σ*𝑥 ∈
𝐴(♯‘𝑥)) |