Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hasheuni Structured version   Visualization version   GIF version

Theorem hasheuni 30529
Description: The cardinality of a disjoint union, not necessarily finite. cf. hashuni 14844. (Contributed by Thierry Arnoux, 19-Nov-2016.) (Revised by Thierry Arnoux, 2-Jan-2017.) (Revised by Thierry Arnoux, 20-Jun-2017.)
Assertion
Ref Expression
hasheuni ((𝐴𝑉Disj 𝑥𝐴 𝑥) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑉

Proof of Theorem hasheuni
StepHypRef Expression
1 nfdisj1 4790 . . . . . . . 8 𝑥Disj 𝑥𝐴 𝑥
2 nfv 2009 . . . . . . . 8 𝑥 𝐴 ∈ Fin
3 nfv 2009 . . . . . . . 8 𝑥 𝐴 ⊆ Fin
41, 2, 3nf3an 2000 . . . . . . 7 𝑥(Disj 𝑥𝐴 𝑥𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin)
5 simp2 1167 . . . . . . 7 ((Disj 𝑥𝐴 𝑥𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin)
6 simp3 1168 . . . . . . 7 ((Disj 𝑥𝐴 𝑥𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ⊆ Fin)
7 simp1 1166 . . . . . . 7 ((Disj 𝑥𝐴 𝑥𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Disj 𝑥𝐴 𝑥)
84, 5, 6, 7hashunif 29946 . . . . . 6 ((Disj 𝑥𝐴 𝑥𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ𝑥𝐴 (♯‘𝑥))
9 simpl 474 . . . . . . . 8 ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin)
10 dfss3 3750 . . . . . . . . . . 11 (𝐴 ⊆ Fin ↔ ∀𝑥𝐴 𝑥 ∈ Fin)
11 hashcl 13349 . . . . . . . . . . . . 13 (𝑥 ∈ Fin → (♯‘𝑥) ∈ ℕ0)
12 nn0re 11548 . . . . . . . . . . . . . 14 ((♯‘𝑥) ∈ ℕ0 → (♯‘𝑥) ∈ ℝ)
13 nn0ge0 11565 . . . . . . . . . . . . . 14 ((♯‘𝑥) ∈ ℕ0 → 0 ≤ (♯‘𝑥))
14 elrege0 12482 . . . . . . . . . . . . . 14 ((♯‘𝑥) ∈ (0[,)+∞) ↔ ((♯‘𝑥) ∈ ℝ ∧ 0 ≤ (♯‘𝑥)))
1512, 13, 14sylanbrc 578 . . . . . . . . . . . . 13 ((♯‘𝑥) ∈ ℕ0 → (♯‘𝑥) ∈ (0[,)+∞))
1611, 15syl 17 . . . . . . . . . . . 12 (𝑥 ∈ Fin → (♯‘𝑥) ∈ (0[,)+∞))
1716ralimi 3099 . . . . . . . . . . 11 (∀𝑥𝐴 𝑥 ∈ Fin → ∀𝑥𝐴 (♯‘𝑥) ∈ (0[,)+∞))
1810, 17sylbi 208 . . . . . . . . . 10 (𝐴 ⊆ Fin → ∀𝑥𝐴 (♯‘𝑥) ∈ (0[,)+∞))
1918r19.21bi 3079 . . . . . . . . 9 ((𝐴 ⊆ Fin ∧ 𝑥𝐴) → (♯‘𝑥) ∈ (0[,)+∞))
2019adantll 705 . . . . . . . 8 (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑥𝐴) → (♯‘𝑥) ∈ (0[,)+∞))
219, 20esumpfinval 30519 . . . . . . 7 ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ*𝑥𝐴(♯‘𝑥) = Σ𝑥𝐴 (♯‘𝑥))
22213adant1 1160 . . . . . 6 ((Disj 𝑥𝐴 𝑥𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ*𝑥𝐴(♯‘𝑥) = Σ𝑥𝐴 (♯‘𝑥))
238, 22eqtr4d 2802 . . . . 5 ((Disj 𝑥𝐴 𝑥𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
24233adant1l 1221 . . . 4 (((𝐴𝑉Disj 𝑥𝐴 𝑥) ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
25243expa 1147 . . 3 ((((𝐴𝑉Disj 𝑥𝐴 𝑥) ∧ 𝐴 ∈ Fin) ∧ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
26 uniexg 7153 . . . . . . . 8 (𝐴𝑉 𝐴 ∈ V)
2710notbii 311 . . . . . . . . . 10 𝐴 ⊆ Fin ↔ ¬ ∀𝑥𝐴 𝑥 ∈ Fin)
28 rexnal 3141 . . . . . . . . . 10 (∃𝑥𝐴 ¬ 𝑥 ∈ Fin ↔ ¬ ∀𝑥𝐴 𝑥 ∈ Fin)
2927, 28bitr4i 269 . . . . . . . . 9 𝐴 ⊆ Fin ↔ ∃𝑥𝐴 ¬ 𝑥 ∈ Fin)
30 elssuni 4625 . . . . . . . . . . 11 (𝑥𝐴𝑥 𝐴)
31 ssfi 8387 . . . . . . . . . . . . 13 (( 𝐴 ∈ Fin ∧ 𝑥 𝐴) → 𝑥 ∈ Fin)
3231expcom 402 . . . . . . . . . . . 12 (𝑥 𝐴 → ( 𝐴 ∈ Fin → 𝑥 ∈ Fin))
3332con3d 149 . . . . . . . . . . 11 (𝑥 𝐴 → (¬ 𝑥 ∈ Fin → ¬ 𝐴 ∈ Fin))
3430, 33syl 17 . . . . . . . . . 10 (𝑥𝐴 → (¬ 𝑥 ∈ Fin → ¬ 𝐴 ∈ Fin))
3534rexlimiv 3174 . . . . . . . . 9 (∃𝑥𝐴 ¬ 𝑥 ∈ Fin → ¬ 𝐴 ∈ Fin)
3629, 35sylbi 208 . . . . . . . 8 𝐴 ⊆ Fin → ¬ 𝐴 ∈ Fin)
37 hashinf 13326 . . . . . . . 8 (( 𝐴 ∈ V ∧ ¬ 𝐴 ∈ Fin) → (♯‘ 𝐴) = +∞)
3826, 36, 37syl2an 589 . . . . . . 7 ((𝐴𝑉 ∧ ¬ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = +∞)
39 vex 3353 . . . . . . . . . . 11 𝑥 ∈ V
40 hashinf 13326 . . . . . . . . . . 11 ((𝑥 ∈ V ∧ ¬ 𝑥 ∈ Fin) → (♯‘𝑥) = +∞)
4139, 40mpan 681 . . . . . . . . . 10 𝑥 ∈ Fin → (♯‘𝑥) = +∞)
4241reximi 3157 . . . . . . . . 9 (∃𝑥𝐴 ¬ 𝑥 ∈ Fin → ∃𝑥𝐴 (♯‘𝑥) = +∞)
4329, 42sylbi 208 . . . . . . . 8 𝐴 ⊆ Fin → ∃𝑥𝐴 (♯‘𝑥) = +∞)
44 nfv 2009 . . . . . . . . . 10 𝑥 𝐴𝑉
45 nfre1 3151 . . . . . . . . . 10 𝑥𝑥𝐴 (♯‘𝑥) = +∞
4644, 45nfan 1998 . . . . . . . . 9 𝑥(𝐴𝑉 ∧ ∃𝑥𝐴 (♯‘𝑥) = +∞)
47 simpl 474 . . . . . . . . 9 ((𝐴𝑉 ∧ ∃𝑥𝐴 (♯‘𝑥) = +∞) → 𝐴𝑉)
48 hashf2 30528 . . . . . . . . . . 11 ♯:V⟶(0[,]+∞)
49 ffvelrn 6547 . . . . . . . . . . 11 ((♯:V⟶(0[,]+∞) ∧ 𝑥 ∈ V) → (♯‘𝑥) ∈ (0[,]+∞))
5048, 39, 49mp2an 683 . . . . . . . . . 10 (♯‘𝑥) ∈ (0[,]+∞)
5150a1i 11 . . . . . . . . 9 (((𝐴𝑉 ∧ ∃𝑥𝐴 (♯‘𝑥) = +∞) ∧ 𝑥𝐴) → (♯‘𝑥) ∈ (0[,]+∞))
52 simpr 477 . . . . . . . . 9 ((𝐴𝑉 ∧ ∃𝑥𝐴 (♯‘𝑥) = +∞) → ∃𝑥𝐴 (♯‘𝑥) = +∞)
5346, 47, 51, 52esumpinfval 30517 . . . . . . . 8 ((𝐴𝑉 ∧ ∃𝑥𝐴 (♯‘𝑥) = +∞) → Σ*𝑥𝐴(♯‘𝑥) = +∞)
5443, 53sylan2 586 . . . . . . 7 ((𝐴𝑉 ∧ ¬ 𝐴 ⊆ Fin) → Σ*𝑥𝐴(♯‘𝑥) = +∞)
5538, 54eqtr4d 2802 . . . . . 6 ((𝐴𝑉 ∧ ¬ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
56553adant2 1161 . . . . 5 ((𝐴𝑉𝐴 ∈ Fin ∧ ¬ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
57563adant1r 1223 . . . 4 (((𝐴𝑉Disj 𝑥𝐴 𝑥) ∧ 𝐴 ∈ Fin ∧ ¬ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
58573expa 1147 . . 3 ((((𝐴𝑉Disj 𝑥𝐴 𝑥) ∧ 𝐴 ∈ Fin) ∧ ¬ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
5925, 58pm2.61dan 847 . 2 (((𝐴𝑉Disj 𝑥𝐴 𝑥) ∧ 𝐴 ∈ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
60 pwfi 8468 . . . . . . 7 ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
61 pwuni 4632 . . . . . . . 8 𝐴 ⊆ 𝒫 𝐴
62 ssfi 8387 . . . . . . . 8 ((𝒫 𝐴 ∈ Fin ∧ 𝐴 ⊆ 𝒫 𝐴) → 𝐴 ∈ Fin)
6361, 62mpan2 682 . . . . . . 7 (𝒫 𝐴 ∈ Fin → 𝐴 ∈ Fin)
6460, 63sylbi 208 . . . . . 6 ( 𝐴 ∈ Fin → 𝐴 ∈ Fin)
6564con3i 151 . . . . 5 𝐴 ∈ Fin → ¬ 𝐴 ∈ Fin)
6626, 65, 37syl2an 589 . . . 4 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘ 𝐴) = +∞)
67 nftru 1899 . . . . . . . . 9 𝑥
68 unrab 4062 . . . . . . . . . . 11 ({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) = {𝑥𝐴 ∣ ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)}
69 exmid 918 . . . . . . . . . . . . 13 ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)
7069rgenw 3071 . . . . . . . . . . . 12 𝑥𝐴 ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)
71 rabid2 3266 . . . . . . . . . . . 12 (𝐴 = {𝑥𝐴 ∣ ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)} ↔ ∀𝑥𝐴 ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0))
7270, 71mpbir 222 . . . . . . . . . . 11 𝐴 = {𝑥𝐴 ∣ ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)}
7368, 72eqtr4i 2790 . . . . . . . . . 10 ({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) = 𝐴
7473a1i 11 . . . . . . . . 9 (⊤ → ({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) = 𝐴)
7567, 74esumeq1d 30479 . . . . . . . 8 (⊤ → Σ*𝑥 ∈ ({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0})(♯‘𝑥) = Σ*𝑥𝐴(♯‘𝑥))
7675mptru 1660 . . . . . . 7 Σ*𝑥 ∈ ({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0})(♯‘𝑥) = Σ*𝑥𝐴(♯‘𝑥)
77 nfrab1 3270 . . . . . . . 8 𝑥{𝑥𝐴 ∣ (♯‘𝑥) = 0}
78 nfrab1 3270 . . . . . . . 8 𝑥{𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}
79 rabexg 4972 . . . . . . . 8 (𝐴𝑉 → {𝑥𝐴 ∣ (♯‘𝑥) = 0} ∈ V)
80 rabexg 4972 . . . . . . . 8 (𝐴𝑉 → {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈ V)
81 rabnc 4124 . . . . . . . . 9 ({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∩ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) = ∅
8281a1i 11 . . . . . . . 8 (𝐴𝑉 → ({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∩ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) = ∅)
8350a1i 11 . . . . . . . 8 ((𝐴𝑉𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0}) → (♯‘𝑥) ∈ (0[,]+∞))
8450a1i 11 . . . . . . . 8 ((𝐴𝑉𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → (♯‘𝑥) ∈ (0[,]+∞))
8544, 77, 78, 79, 80, 82, 83, 84esumsplit 30497 . . . . . . 7 (𝐴𝑉 → Σ*𝑥 ∈ ({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0})(♯‘𝑥) = (Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒 Σ*𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥)))
8676, 85syl5eqr 2813 . . . . . 6 (𝐴𝑉 → Σ*𝑥𝐴(♯‘𝑥) = (Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒 Σ*𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥)))
8786adantr 472 . . . . 5 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥𝐴(♯‘𝑥) = (Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒 Σ*𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥)))
88 nfv 2009 . . . . . . 7 𝑥(𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin)
8980adantr 472 . . . . . . 7 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈ V)
90 simpr 477 . . . . . . . . 9 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ 𝐴 ∈ Fin)
91 dfrab3 4066 . . . . . . . . . . . 12 {𝑥𝐴 ∣ (♯‘𝑥) = 0} = (𝐴 ∩ {𝑥 ∣ (♯‘𝑥) = 0})
92 hasheq0 13356 . . . . . . . . . . . . . . . 16 (𝑥 ∈ V → ((♯‘𝑥) = 0 ↔ 𝑥 = ∅))
9339, 92ax-mp 5 . . . . . . . . . . . . . . 15 ((♯‘𝑥) = 0 ↔ 𝑥 = ∅)
9493abbii 2882 . . . . . . . . . . . . . 14 {𝑥 ∣ (♯‘𝑥) = 0} = {𝑥𝑥 = ∅}
95 df-sn 4335 . . . . . . . . . . . . . 14 {∅} = {𝑥𝑥 = ∅}
9694, 95eqtr4i 2790 . . . . . . . . . . . . 13 {𝑥 ∣ (♯‘𝑥) = 0} = {∅}
9796ineq2i 3973 . . . . . . . . . . . 12 (𝐴 ∩ {𝑥 ∣ (♯‘𝑥) = 0}) = (𝐴 ∩ {∅})
9891, 97eqtri 2787 . . . . . . . . . . 11 {𝑥𝐴 ∣ (♯‘𝑥) = 0} = (𝐴 ∩ {∅})
99 snfi 8245 . . . . . . . . . . . 12 {∅} ∈ Fin
100 inss2 3993 . . . . . . . . . . . 12 (𝐴 ∩ {∅}) ⊆ {∅}
101 ssfi 8387 . . . . . . . . . . . 12 (({∅} ∈ Fin ∧ (𝐴 ∩ {∅}) ⊆ {∅}) → (𝐴 ∩ {∅}) ∈ Fin)
10299, 100, 101mp2an 683 . . . . . . . . . . 11 (𝐴 ∩ {∅}) ∈ Fin
10398, 102eqeltri 2840 . . . . . . . . . 10 {𝑥𝐴 ∣ (♯‘𝑥) = 0} ∈ Fin
104103a1i 11 . . . . . . . . 9 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → {𝑥𝐴 ∣ (♯‘𝑥) = 0} ∈ Fin)
105 difinf 8437 . . . . . . . . 9 ((¬ 𝐴 ∈ Fin ∧ {𝑥𝐴 ∣ (♯‘𝑥) = 0} ∈ Fin) → ¬ (𝐴 ∖ {𝑥𝐴 ∣ (♯‘𝑥) = 0}) ∈ Fin)
10690, 104, 105syl2anc 579 . . . . . . . 8 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (𝐴 ∖ {𝑥𝐴 ∣ (♯‘𝑥) = 0}) ∈ Fin)
107 notrab 4068 . . . . . . . . 9 (𝐴 ∖ {𝑥𝐴 ∣ (♯‘𝑥) = 0}) = {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}
108107eleq1i 2835 . . . . . . . 8 ((𝐴 ∖ {𝑥𝐴 ∣ (♯‘𝑥) = 0}) ∈ Fin ↔ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈ Fin)
109106, 108sylnib 319 . . . . . . 7 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈ Fin)
11050a1i 11 . . . . . . 7 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → (♯‘𝑥) ∈ (0[,]+∞))
11139a1i 11 . . . . . . . 8 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 𝑥 ∈ V)
112 simpr 477 . . . . . . . . . . 11 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0})
113 rabid 3263 . . . . . . . . . . 11 (𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} ↔ (𝑥𝐴 ∧ ¬ (♯‘𝑥) = 0))
114112, 113sylib 209 . . . . . . . . . 10 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → (𝑥𝐴 ∧ ¬ (♯‘𝑥) = 0))
115114simprd 489 . . . . . . . . 9 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → ¬ (♯‘𝑥) = 0)
11693biimpri 219 . . . . . . . . . 10 (𝑥 = ∅ → (♯‘𝑥) = 0)
117116necon3bi 2963 . . . . . . . . 9 (¬ (♯‘𝑥) = 0 → 𝑥 ≠ ∅)
118115, 117syl 17 . . . . . . . 8 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 𝑥 ≠ ∅)
119 hashge1 13380 . . . . . . . 8 ((𝑥 ∈ V ∧ 𝑥 ≠ ∅) → 1 ≤ (♯‘𝑥))
120111, 118, 119syl2anc 579 . . . . . . 7 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 1 ≤ (♯‘𝑥))
121 1re 10293 . . . . . . . . 9 1 ∈ ℝ
122121rexri 10351 . . . . . . . 8 1 ∈ ℝ*
123122a1i 11 . . . . . . 7 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → 1 ∈ ℝ*)
124 0lt1 10804 . . . . . . . 8 0 < 1
125124a1i 11 . . . . . . 7 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → 0 < 1)
12688, 78, 89, 109, 110, 120, 123, 125esumpinfsum 30521 . . . . . 6 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥) = +∞)
127126oveq2d 6858 . . . . 5 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → (Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒 Σ*𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥)) = (Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒 +∞))
128 iccssxr 12458 . . . . . . 7 (0[,]+∞) ⊆ ℝ*
12979adantr 472 . . . . . . . 8 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → {𝑥𝐴 ∣ (♯‘𝑥) = 0} ∈ V)
13050a1i 11 . . . . . . . . 9 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0}) → (♯‘𝑥) ∈ (0[,]+∞))
131130ralrimiva 3113 . . . . . . . 8 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → ∀𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞))
13277esumcl 30474 . . . . . . . 8 (({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∈ V ∧ ∀𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞)) → Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞))
133129, 131, 132syl2anc 579 . . . . . . 7 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞))
134128, 133sseldi 3759 . . . . . 6 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ ℝ*)
135 xrge0neqmnf 12479 . . . . . . 7 *𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞) → Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ≠ -∞)
136133, 135syl 17 . . . . . 6 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ≠ -∞)
137 xaddpnf1 12259 . . . . . 6 ((Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ ℝ* ∧ Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ≠ -∞) → (Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒 +∞) = +∞)
138134, 136, 137syl2anc 579 . . . . 5 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → (Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒 +∞) = +∞)
13987, 127, 1383eqtrd 2803 . . . 4 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥𝐴(♯‘𝑥) = +∞)
14066, 139eqtr4d 2802 . . 3 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
141140adantlr 706 . 2 (((𝐴𝑉Disj 𝑥𝐴 𝑥) ∧ ¬ 𝐴 ∈ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
14259, 141pm2.61dan 847 1 ((𝐴𝑉Disj 𝑥𝐴 𝑥) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wtru 1653  wcel 2155  {cab 2751  wne 2937  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  cdif 3729  cun 3730  cin 3731  wss 3732  c0 4079  𝒫 cpw 4315  {csn 4334   cuni 4594  Disj wdisj 4777   class class class wbr 4809  wf 6064  cfv 6068  (class class class)co 6842  Fincfn 8160  cr 10188  0cc0 10189  1c1 10190  +∞cpnf 10325  -∞cmnf 10326  *cxr 10327   < clt 10328  cle 10329  0cn0 11538   +𝑒 cxad 12144  [,)cico 12379  [,]cicc 12380  chash 13321  Σcsu 14703  Σ*cesum 30471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-disj 4778  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-supp 7498  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fsupp 8483  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-xnn0 11611  df-z 11625  df-dec 11741  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ioo 12381  df-ioc 12382  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-fac 13265  df-bc 13294  df-hash 13322  df-shft 14094  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-limsup 14489  df-clim 14506  df-rlim 14507  df-sum 14704  df-ef 15082  df-sin 15084  df-cos 15085  df-pi 15087  df-struct 16134  df-ndx 16135  df-slot 16136  df-base 16138  df-sets 16139  df-ress 16140  df-plusg 16229  df-mulr 16230  df-starv 16231  df-sca 16232  df-vsca 16233  df-ip 16234  df-tset 16235  df-ple 16236  df-ds 16238  df-unif 16239  df-hom 16240  df-cco 16241  df-rest 16351  df-topn 16352  df-0g 16370  df-gsum 16371  df-topgen 16372  df-pt 16373  df-prds 16376  df-ordt 16429  df-xrs 16430  df-qtop 16435  df-imas 16436  df-xps 16438  df-mre 16514  df-mrc 16515  df-acs 16517  df-ps 17468  df-tsr 17469  df-plusf 17509  df-mgm 17510  df-sgrp 17552  df-mnd 17563  df-mhm 17603  df-submnd 17604  df-grp 17694  df-minusg 17695  df-sbg 17696  df-mulg 17810  df-subg 17857  df-cntz 18015  df-cmn 18461  df-abl 18462  df-mgp 18757  df-ur 18769  df-ring 18816  df-cring 18817  df-subrg 19047  df-abv 19086  df-lmod 19134  df-scaf 19135  df-sra 19446  df-rgmod 19447  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-fbas 20016  df-fg 20017  df-cnfld 20020  df-top 20978  df-topon 20995  df-topsp 21017  df-bases 21030  df-cld 21103  df-ntr 21104  df-cls 21105  df-nei 21182  df-lp 21220  df-perf 21221  df-cn 21311  df-cnp 21312  df-haus 21399  df-tx 21645  df-hmeo 21838  df-fil 21929  df-fm 22021  df-flim 22022  df-flf 22023  df-tmd 22155  df-tgp 22156  df-tsms 22209  df-trg 22242  df-xms 22404  df-ms 22405  df-tms 22406  df-nm 22666  df-ngp 22667  df-nrg 22669  df-nlm 22670  df-ii 22959  df-cncf 22960  df-limc 23921  df-dv 23922  df-log 24594  df-esum 30472
This theorem is referenced by:  cntmeas  30671
  Copyright terms: Public domain W3C validator