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 ffvelrn ( ( ♯ : 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 simpr ( ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) → 𝑥 ∈ { 𝑥𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } )
113 rabid ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ↔ ( 𝑥𝐴 ∧ ¬ ( ♯ ‘ 𝑥 ) = 0 ) )
114 112 113 sylib ( ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) → ( 𝑥𝐴 ∧ ¬ ( ♯ ‘ 𝑥 ) = 0 ) )
115 114 simprd ( ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) → ¬ ( ♯ ‘ 𝑥 ) = 0 )
116 93 biimpri ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = 0 )
117 116 necon3bi ( ¬ ( ♯ ‘ 𝑥 ) = 0 → 𝑥 ≠ ∅ )
118 115 117 syl ( ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) → 𝑥 ≠ ∅ )
119 hashge1 ( ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) → 1 ≤ ( ♯ ‘ 𝑥 ) )
120 111 118 119 syl2anc ( ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ) → 1 ≤ ( ♯ ‘ 𝑥 ) )
121 1xr 1 ∈ ℝ*
122 121 a1i ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) → 1 ∈ ℝ* )
123 0lt1 0 < 1
124 123 a1i ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) → 0 < 1 )
125 88 78 89 109 110 120 122 124 esumpinfsum ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) → Σ* 𝑥 ∈ { 𝑥𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) = +∞ )
126 125 oveq2d ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( Σ* 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) +𝑒 Σ* 𝑥 ∈ { 𝑥𝐴 ∣ ¬ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ) = ( Σ* 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) +𝑒 +∞ ) )
127 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
128 79 adantr ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) → { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∈ V )
129 50 a1i ( ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ) → ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
130 129 ralrimiva ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ∀ 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
131 77 esumcl ( ( { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ∈ V ∧ ∀ 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
132 128 130 131 syl2anc ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) → Σ* 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
133 127 132 sselid ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) → Σ* 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ∈ ℝ* )
134 xrge0neqmnf ( Σ* 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) → Σ* 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ≠ -∞ )
135 132 134 syl ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) → Σ* 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ≠ -∞ )
136 xaddpnf1 ( ( Σ* 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ∈ ℝ* ∧ Σ* 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) ≠ -∞ ) → ( Σ* 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) +𝑒 +∞ ) = +∞ )
137 133 135 136 syl2anc ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( Σ* 𝑥 ∈ { 𝑥𝐴 ∣ ( ♯ ‘ 𝑥 ) = 0 } ( ♯ ‘ 𝑥 ) +𝑒 +∞ ) = +∞ )
138 87 126 137 3eqtrd ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) → Σ* 𝑥𝐴 ( ♯ ‘ 𝑥 ) = +∞ )
139 66 138 eqtr4d ( ( 𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = Σ* 𝑥𝐴 ( ♯ ‘ 𝑥 ) )
140 139 adantlr ( ( ( 𝐴𝑉Disj 𝑥𝐴 𝑥 ) ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = Σ* 𝑥𝐴 ( ♯ ‘ 𝑥 ) )
141 59 140 pm2.61dan ( ( 𝐴𝑉Disj 𝑥𝐴 𝑥 ) → ( ♯ ‘ 𝐴 ) = Σ* 𝑥𝐴 ( ♯ ‘ 𝑥 ) )