Metamath Proof Explorer

Theorem hasheuni

Description: The cardinality of a disjoint union, not necessarily finite. cf. hashuni . (Contributed by Thierry Arnoux, 19-Nov-2016) (Revised by Thierry Arnoux, 2-Jan-2017) (Revised by Thierry Arnoux, 20-Jun-2017)

Ref Expression
Assertion hasheuni ( ( 𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) → ( ♯ ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 nfdisj1 ⊢ Ⅎ 𝑥 Disj 𝑥 ∈ 𝐴 𝑥
2 nfv ⊢ Ⅎ 𝑥 𝐴 ∈ Fin
3 nfv ⊢ Ⅎ 𝑥 𝐴 ⊆ Fin
4 1 2 3 nf3an ⊢ Ⅎ 𝑥 ( Disj 𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin )
5 simp2 ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → 𝐴 ∈ Fin )
6 simp3 ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → 𝐴 ⊆ Fin )
7 simp1 ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → Disj 𝑥 ∈ 𝐴 𝑥 )
8 4 5 6 7 hashunif ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
9 simpl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → 𝐴 ∈ Fin )
10 dfss3 ⊢ ( 𝐴 ⊆ Fin ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ Fin )
11 hashcl ⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
12 nn0re ⊢ ( ( ♯ ‘ 𝑥 ) ∈ ℕ0 → ( ♯ ‘ 𝑥 ) ∈ ℝ )
13 nn0ge0 ⊢ ( ( ♯ ‘ 𝑥 ) ∈ ℕ0 → 0 ≤ ( ♯ ‘ 𝑥 ) )
14 elrege0 ⊢ ( ( ♯ ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ♯ ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ♯ ‘ 𝑥 ) ) )
15 12 13 14 sylanbrc ⊢ ( ( ♯ ‘ 𝑥 ) ∈ ℕ0 → ( ♯ ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
16 11 15 syl ⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
17 16 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ Fin → ∀ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
18 10 17 sylbi ⊢ ( 𝐴 ⊆ Fin → ∀ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
19 18 r19.21bi ⊢ ( ( 𝐴 ⊆ Fin ∧ 𝑥 ∈ 𝐴 ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
20 19 adantll ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) ∧ 𝑥 ∈ 𝐴 ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
21 9 20 esumpfinval ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
22 21 3adant1 ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
23 8 22 eqtr4d ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
24 23 3adant1l ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
25 24 3expa ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ∧ 𝐴 ∈ Fin ) ∧ 𝐴 ⊆ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
26 uniexg ⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V )
27 10 notbii ⊢ ( ¬ 𝐴 ⊆ Fin ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ Fin )
28 rexnal ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ Fin ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ Fin )
29 27 28 bitr4i ⊢ ( ¬ 𝐴 ⊆ Fin ↔ ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ Fin )
30 elssuni ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴 )
31 ssfi ⊢ ( ( ∪ 𝐴 ∈ Fin ∧ 𝑥 ⊆ ∪ 𝐴 ) → 𝑥 ∈ Fin )
32 31 expcom ⊢ ( 𝑥 ⊆ ∪ 𝐴 → ( ∪ 𝐴 ∈ Fin → 𝑥 ∈ Fin ) )
33 32 con3d ⊢ ( 𝑥 ⊆ ∪ 𝐴 → ( ¬ 𝑥 ∈ Fin → ¬ ∪ 𝐴 ∈ Fin ) )
34 30 33 syl ⊢ ( 𝑥 ∈ 𝐴 → ( ¬ 𝑥 ∈ Fin → ¬ ∪ 𝐴 ∈ Fin ) )
35 34 rexlimiv ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ Fin → ¬ ∪ 𝐴 ∈ Fin )
36 29 35 sylbi ⊢ ( ¬ 𝐴 ⊆ Fin → ¬ ∪ 𝐴 ∈ Fin )
37 hashinf ⊢ ( ( ∪ 𝐴 ∈ V ∧ ¬ ∪ 𝐴 ∈ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = +∞ )
38 26 36 37 syl2an ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ⊆ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = +∞ )
39 vex ⊢ 𝑥 ∈ V
40 hashinf ⊢ ( ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ Fin ) → ( ♯ ‘ 𝑥 ) = +∞ )
41 39 40 mpan ⊢ ( ¬ 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) = +∞ )
42 41 reximi ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ Fin → ∃ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = +∞ )
43 29 42 sylbi ⊢ ( ¬ 𝐴 ⊆ Fin → ∃ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = +∞ )
44 nfv ⊢ Ⅎ 𝑥 𝐴 ∈ 𝑉
45 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = +∞
46 44 45 nfan ⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = +∞ )
47 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = +∞ ) → 𝐴 ∈ 𝑉 )
48 hashf2 ⊢ ♯ : V ⟶ ( 0 [,] +∞ )
49 ffvelcdm ⊢ ( ( ♯ : V ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ V ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
50 48 39 49 mp2an ⊢ ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ )
51 50 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = +∞ ) ∧ 𝑥 ∈ 𝐴 ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
52 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = +∞ ) → ∃ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = +∞ )
53 46 47 51 52 esumpinfval ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = +∞ ) → Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = +∞ )
54 43 53 sylan2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ⊆ Fin ) → Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = +∞ )
55 38 54 eqtr4d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ⊆ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
56 55 3adant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ Fin ∧ ¬ 𝐴 ⊆ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
57 56 3adant1r ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ∧ 𝐴 ∈ Fin ∧ ¬ 𝐴 ⊆ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
58 57 3expa ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ∧ 𝐴 ∈ Fin ) ∧ ¬ 𝐴 ⊆ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
59 25 58 pm2.61dan ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ∧ 𝐴 ∈ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
60 pwfi ⊢ ( ∪ 𝐴 ∈ Fin ↔ 𝒫 ∪ 𝐴 ∈ Fin )
61 pwuni ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
62 ssfi ⊢ ( ( 𝒫 ∪ 𝐴 ∈ Fin ∧ 𝐴 ⊆ 𝒫 ∪ 𝐴 ) → 𝐴 ∈ Fin )
63 61 62 mpan2 ⊢ ( 𝒫 ∪ 𝐴 ∈ Fin → 𝐴 ∈ Fin )
64 60 63 sylbi ⊢ ( ∪ 𝐴 ∈ Fin → 𝐴 ∈ Fin )
65 64 con3i ⊢ ( ¬ 𝐴 ∈ Fin → ¬ ∪ 𝐴 ∈ Fin )
66 26 65 37 syl2an ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = +∞ )
67 nftru ⊢ Ⅎ 𝑥 ⊤
68 unrab ⊢ ( { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∪ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) = { 𝑥 ∈ 𝐴 ∣ ( ( ♯ ‘ 𝑥 ) = 0 ∨ ¬ ( ♯ ‘ 𝑥 ) = 0 ) }
69 exmid ⊢ ( ( ♯ ‘ 𝑥 ) = 0 ∨ ¬ ( ♯ ‘ 𝑥 ) = 0 )
70 69 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 ( ( ♯ ‘ 𝑥 ) = 0 ∨ ¬ ( ♯ ‘ 𝑥 ) = 0 )
71 rabid2 ⊢ ( 𝐴 = { 𝑥 ∈ 𝐴 ∣ ( ( ♯ ‘ 𝑥 ) = 0 ∨ ¬ ( ♯ ‘ 𝑥 ) = 0 ) } ↔ ∀ 𝑥 ∈ 𝐴 ( ( ♯ ‘ 𝑥 ) = 0 ∨ ¬ ( ♯ ‘ 𝑥 ) = 0 ) )
72 70 71 mpbir ⊢ 𝐴 = { 𝑥 ∈ 𝐴 ∣ ( ( ♯ ‘ 𝑥 ) = 0 ∨ ¬ ( ♯ ‘ 𝑥 ) = 0 ) }
73 68 72 eqtr4i ⊢ ( { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∪ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) = 𝐴
74 73 a1i ⊢ ( ⊤ → ( { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∪ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) = 𝐴 )
75 67 74 esumeq1d ⊢ ( ⊤ → Σ* 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∪ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) ( ♯ ‘ 𝑥 ) = Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
76 75 mptru ⊢ Σ* 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∪ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) ( ♯ ‘ 𝑥 ) = Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 )
77 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 }
78 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 }
79 rabexg ⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∈ V )
80 rabexg ⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ∈ V )
81 rabnc ⊢ ( { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∩ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) = ∅
82 81 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∩ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) = ∅ )
83 50 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
84 50 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
85 44 77 78 79 80 82 83 84 esumsplit ⊢ ( 𝐴 ∈ 𝑉 → Σ* 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∪ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) ( ♯ ‘ 𝑥 ) = ( Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) +𝑒 Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ) )
86 76 85 eqtr3id ⊢ ( 𝐴 ∈ 𝑉 → Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = ( Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) +𝑒 Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ) )
87 86 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = ( Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) +𝑒 Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ) )
88 nfv ⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin )
89 80 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ∈ V )
90 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ¬ 𝐴 ∈ Fin )
91 dfrab3 ⊢ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } = ( 𝐴 ∩ { 𝑥 ∣ ( ♯ ‘ 𝑥 ) = 0 } )
92 hasheq0 ⊢ ( 𝑥 ∈ V → ( ( ♯ ‘ 𝑥 ) = 0 ↔ 𝑥 = ∅ ) )
93 39 92 ax-mp ⊢ ( ( ♯ ‘ 𝑥 ) = 0 ↔ 𝑥 = ∅ )
94 93 abbii ⊢ { 𝑥 ∣ ( ♯ ‘ 𝑥 ) = 0 } = { 𝑥 ∣ 𝑥 = ∅ }
95 df-sn ⊢ { ∅ } = { 𝑥 ∣ 𝑥 = ∅ }
96 94 95 eqtr4i ⊢ { 𝑥 ∣ ( ♯ ‘ 𝑥 ) = 0 } = { ∅ }
97 96 ineq2i ⊢ ( 𝐴 ∩ { 𝑥 ∣ ( ♯ ‘ 𝑥 ) = 0 } ) = ( 𝐴 ∩ { ∅ } )
98 91 97 eqtri ⊢ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } = ( 𝐴 ∩ { ∅ } )
99 snfi ⊢ { ∅ } ∈ Fin
100 inss2 ⊢ ( 𝐴 ∩ { ∅ } ) ⊆ { ∅ }
101 ssfi ⊢ ( ( { ∅ } ∈ Fin ∧ ( 𝐴 ∩ { ∅ } ) ⊆ { ∅ } ) → ( 𝐴 ∩ { ∅ } ) ∈ Fin )
102 99 100 101 mp2an ⊢ ( 𝐴 ∩ { ∅ } ) ∈ Fin
103 98 102 eqeltri ⊢ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∈ Fin
104 103 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∈ Fin )
105 difinf ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∈ Fin ) → ¬ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ) ∈ Fin )
106 90 104 105 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ¬ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ) ∈ Fin )
107 notrab ⊢ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ) = { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 }
108 107 eleq1i ⊢ ( ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ) ∈ Fin ↔ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ∈ Fin )
109 106 108 sylnib ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ¬ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ∈ Fin )
110 50 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
111 39 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) → 𝑥 ∈ V )
112 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ ( ♯ ‘ 𝑥 ) = 0 ) )
113 112 bilani ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) → ( 𝑥 ∈ 𝐴 ∧ ¬ ( ♯ ‘ 𝑥 ) = 0 ) )
114 113 simprd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) → ¬ ( ♯ ‘ 𝑥 ) = 0 )
115 93 biimpri ⊢ ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = 0 )
116 115 necon3bi ⊢ ( ¬ ( ♯ ‘ 𝑥 ) = 0 → 𝑥 ≠ ∅ )
117 114 116 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) → 𝑥 ≠ ∅ )
118 hashge1 ⊢ ( ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) → 1 ≤ ( ♯ ‘ 𝑥 ) )
119 111 117 118 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) → 1 ≤ ( ♯ ‘ 𝑥 ) )
120 1xr ⊢ 1 ∈ ℝ*
121 120 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → 1 ∈ ℝ* )
122 0lt1 ⊢ 0 < 1
123 122 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → 0 < 1 )
124 88 78 89 109 110 119 121 123 esumpinfsum ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) = +∞ )
125 124 oveq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) +𝑒 Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ) = ( Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) +𝑒 +∞ ) )
126 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
127 79 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∈ V )
128 50 a1i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
129 128 ralrimiva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
130 77 esumcl ⊢ ( ( { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∈ V ∧ ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
131 127 129 130 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
132 126 131 sselid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ∈ ℝ* )
133 xrge0neqmnf ⊢ ( Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) → Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ≠ -∞ )
134 131 133 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ≠ -∞ )
135 xaddpnf1 ⊢ ( ( Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ∈ ℝ* ∧ Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ≠ -∞ ) → ( Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) +𝑒 +∞ ) = +∞ )
136 132 134 135 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( Σ* 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) +𝑒 +∞ ) = +∞ )
137 87 125 136 3eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = +∞ )
138 66 137 eqtr4d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
139 138 adantlr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
140 59 139 pm2.61dan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥 ) → ( ♯ ‘ ∪ 𝐴 ) = Σ* 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )