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 31231
Description: The cardinality of a disjoint union, not necessarily finite. cf. hashuni 15173. (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 5041 . . . . . . . 8 𝑥Disj 𝑥𝐴 𝑥
2 nfv 1908 . . . . . . . 8 𝑥 𝐴 ∈ Fin
3 nfv 1908 . . . . . . . 8 𝑥 𝐴 ⊆ Fin
41, 2, 3nf3an 1895 . . . . . . 7 𝑥(Disj 𝑥𝐴 𝑥𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin)
5 simp2 1131 . . . . . . 7 ((Disj 𝑥𝐴 𝑥𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin)
6 simp3 1132 . . . . . . 7 ((Disj 𝑥𝐴 𝑥𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ⊆ Fin)
7 simp1 1130 . . . . . . 7 ((Disj 𝑥𝐴 𝑥𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Disj 𝑥𝐴 𝑥)
84, 5, 6, 7hashunif 30442 . . . . . 6 ((Disj 𝑥𝐴 𝑥𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ𝑥𝐴 (♯‘𝑥))
9 simpl 483 . . . . . . . 8 ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin)
10 dfss3 3959 . . . . . . . . . . 11 (𝐴 ⊆ Fin ↔ ∀𝑥𝐴 𝑥 ∈ Fin)
11 hashcl 13710 . . . . . . . . . . . . 13 (𝑥 ∈ Fin → (♯‘𝑥) ∈ ℕ0)
12 nn0re 11898 . . . . . . . . . . . . . 14 ((♯‘𝑥) ∈ ℕ0 → (♯‘𝑥) ∈ ℝ)
13 nn0ge0 11914 . . . . . . . . . . . . . 14 ((♯‘𝑥) ∈ ℕ0 → 0 ≤ (♯‘𝑥))
14 elrege0 12835 . . . . . . . . . . . . . 14 ((♯‘𝑥) ∈ (0[,)+∞) ↔ ((♯‘𝑥) ∈ ℝ ∧ 0 ≤ (♯‘𝑥)))
1512, 13, 14sylanbrc 583 . . . . . . . . . . . . 13 ((♯‘𝑥) ∈ ℕ0 → (♯‘𝑥) ∈ (0[,)+∞))
1611, 15syl 17 . . . . . . . . . . . 12 (𝑥 ∈ Fin → (♯‘𝑥) ∈ (0[,)+∞))
1716ralimi 3164 . . . . . . . . . . 11 (∀𝑥𝐴 𝑥 ∈ Fin → ∀𝑥𝐴 (♯‘𝑥) ∈ (0[,)+∞))
1810, 17sylbi 218 . . . . . . . . . 10 (𝐴 ⊆ Fin → ∀𝑥𝐴 (♯‘𝑥) ∈ (0[,)+∞))
1918r19.21bi 3212 . . . . . . . . 9 ((𝐴 ⊆ Fin ∧ 𝑥𝐴) → (♯‘𝑥) ∈ (0[,)+∞))
2019adantll 710 . . . . . . . 8 (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑥𝐴) → (♯‘𝑥) ∈ (0[,)+∞))
219, 20esumpfinval 31221 . . . . . . 7 ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ*𝑥𝐴(♯‘𝑥) = Σ𝑥𝐴 (♯‘𝑥))
22213adant1 1124 . . . . . 6 ((Disj 𝑥𝐴 𝑥𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ*𝑥𝐴(♯‘𝑥) = Σ𝑥𝐴 (♯‘𝑥))
238, 22eqtr4d 2863 . . . . 5 ((Disj 𝑥𝐴 𝑥𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
24233adant1l 1170 . . . 4 (((𝐴𝑉Disj 𝑥𝐴 𝑥) ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
25243expa 1112 . . 3 ((((𝐴𝑉Disj 𝑥𝐴 𝑥) ∧ 𝐴 ∈ Fin) ∧ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
26 uniexg 7460 . . . . . . . 8 (𝐴𝑉 𝐴 ∈ V)
2710notbii 321 . . . . . . . . . 10 𝐴 ⊆ Fin ↔ ¬ ∀𝑥𝐴 𝑥 ∈ Fin)
28 rexnal 3242 . . . . . . . . . 10 (∃𝑥𝐴 ¬ 𝑥 ∈ Fin ↔ ¬ ∀𝑥𝐴 𝑥 ∈ Fin)
2927, 28bitr4i 279 . . . . . . . . 9 𝐴 ⊆ Fin ↔ ∃𝑥𝐴 ¬ 𝑥 ∈ Fin)
30 elssuni 4865 . . . . . . . . . . 11 (𝑥𝐴𝑥 𝐴)
31 ssfi 8730 . . . . . . . . . . . . 13 (( 𝐴 ∈ Fin ∧ 𝑥 𝐴) → 𝑥 ∈ Fin)
3231expcom 414 . . . . . . . . . . . 12 (𝑥 𝐴 → ( 𝐴 ∈ Fin → 𝑥 ∈ Fin))
3332con3d 155 . . . . . . . . . . 11 (𝑥 𝐴 → (¬ 𝑥 ∈ Fin → ¬ 𝐴 ∈ Fin))
3430, 33syl 17 . . . . . . . . . 10 (𝑥𝐴 → (¬ 𝑥 ∈ Fin → ¬ 𝐴 ∈ Fin))
3534rexlimiv 3284 . . . . . . . . 9 (∃𝑥𝐴 ¬ 𝑥 ∈ Fin → ¬ 𝐴 ∈ Fin)
3629, 35sylbi 218 . . . . . . . 8 𝐴 ⊆ Fin → ¬ 𝐴 ∈ Fin)
37 hashinf 13688 . . . . . . . 8 (( 𝐴 ∈ V ∧ ¬ 𝐴 ∈ Fin) → (♯‘ 𝐴) = +∞)
3826, 36, 37syl2an 595 . . . . . . 7 ((𝐴𝑉 ∧ ¬ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = +∞)
39 vex 3502 . . . . . . . . . . 11 𝑥 ∈ V
40 hashinf 13688 . . . . . . . . . . 11 ((𝑥 ∈ V ∧ ¬ 𝑥 ∈ Fin) → (♯‘𝑥) = +∞)
4139, 40mpan 686 . . . . . . . . . 10 𝑥 ∈ Fin → (♯‘𝑥) = +∞)
4241reximi 3247 . . . . . . . . 9 (∃𝑥𝐴 ¬ 𝑥 ∈ Fin → ∃𝑥𝐴 (♯‘𝑥) = +∞)
4329, 42sylbi 218 . . . . . . . 8 𝐴 ⊆ Fin → ∃𝑥𝐴 (♯‘𝑥) = +∞)
44 nfv 1908 . . . . . . . . . 10 𝑥 𝐴𝑉
45 nfre1 3310 . . . . . . . . . 10 𝑥𝑥𝐴 (♯‘𝑥) = +∞
4644, 45nfan 1893 . . . . . . . . 9 𝑥(𝐴𝑉 ∧ ∃𝑥𝐴 (♯‘𝑥) = +∞)
47 simpl 483 . . . . . . . . 9 ((𝐴𝑉 ∧ ∃𝑥𝐴 (♯‘𝑥) = +∞) → 𝐴𝑉)
48 hashf2 31230 . . . . . . . . . . 11 ♯:V⟶(0[,]+∞)
49 ffvelrn 6844 . . . . . . . . . . 11 ((♯:V⟶(0[,]+∞) ∧ 𝑥 ∈ V) → (♯‘𝑥) ∈ (0[,]+∞))
5048, 39, 49mp2an 688 . . . . . . . . . 10 (♯‘𝑥) ∈ (0[,]+∞)
5150a1i 11 . . . . . . . . 9 (((𝐴𝑉 ∧ ∃𝑥𝐴 (♯‘𝑥) = +∞) ∧ 𝑥𝐴) → (♯‘𝑥) ∈ (0[,]+∞))
52 simpr 485 . . . . . . . . 9 ((𝐴𝑉 ∧ ∃𝑥𝐴 (♯‘𝑥) = +∞) → ∃𝑥𝐴 (♯‘𝑥) = +∞)
5346, 47, 51, 52esumpinfval 31219 . . . . . . . 8 ((𝐴𝑉 ∧ ∃𝑥𝐴 (♯‘𝑥) = +∞) → Σ*𝑥𝐴(♯‘𝑥) = +∞)
5443, 53sylan2 592 . . . . . . 7 ((𝐴𝑉 ∧ ¬ 𝐴 ⊆ Fin) → Σ*𝑥𝐴(♯‘𝑥) = +∞)
5538, 54eqtr4d 2863 . . . . . 6 ((𝐴𝑉 ∧ ¬ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
56553adant2 1125 . . . . 5 ((𝐴𝑉𝐴 ∈ Fin ∧ ¬ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
57563adant1r 1171 . . . 4 (((𝐴𝑉Disj 𝑥𝐴 𝑥) ∧ 𝐴 ∈ Fin ∧ ¬ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
58573expa 1112 . . 3 ((((𝐴𝑉Disj 𝑥𝐴 𝑥) ∧ 𝐴 ∈ Fin) ∧ ¬ 𝐴 ⊆ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
5925, 58pm2.61dan 809 . 2 (((𝐴𝑉Disj 𝑥𝐴 𝑥) ∧ 𝐴 ∈ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
60 pwfi 8811 . . . . . . 7 ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
61 pwuni 4872 . . . . . . . 8 𝐴 ⊆ 𝒫 𝐴
62 ssfi 8730 . . . . . . . 8 ((𝒫 𝐴 ∈ Fin ∧ 𝐴 ⊆ 𝒫 𝐴) → 𝐴 ∈ Fin)
6361, 62mpan2 687 . . . . . . 7 (𝒫 𝐴 ∈ Fin → 𝐴 ∈ Fin)
6460, 63sylbi 218 . . . . . 6 ( 𝐴 ∈ Fin → 𝐴 ∈ Fin)
6564con3i 157 . . . . 5 𝐴 ∈ Fin → ¬ 𝐴 ∈ Fin)
6626, 65, 37syl2an 595 . . . 4 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘ 𝐴) = +∞)
67 nftru 1798 . . . . . . . . 9 𝑥
68 unrab 4277 . . . . . . . . . . 11 ({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) = {𝑥𝐴 ∣ ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)}
69 exmid 890 . . . . . . . . . . . . 13 ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)
7069rgenw 3154 . . . . . . . . . . . 12 𝑥𝐴 ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)
71 rabid2 3386 . . . . . . . . . . . 12 (𝐴 = {𝑥𝐴 ∣ ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)} ↔ ∀𝑥𝐴 ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0))
7270, 71mpbir 232 . . . . . . . . . . 11 𝐴 = {𝑥𝐴 ∣ ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)}
7368, 72eqtr4i 2851 . . . . . . . . . 10 ({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) = 𝐴
7473a1i 11 . . . . . . . . 9 (⊤ → ({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) = 𝐴)
7567, 74esumeq1d 31181 . . . . . . . 8 (⊤ → Σ*𝑥 ∈ ({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0})(♯‘𝑥) = Σ*𝑥𝐴(♯‘𝑥))
7675mptru 1537 . . . . . . 7 Σ*𝑥 ∈ ({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0})(♯‘𝑥) = Σ*𝑥𝐴(♯‘𝑥)
77 nfrab1 3389 . . . . . . . 8 𝑥{𝑥𝐴 ∣ (♯‘𝑥) = 0}
78 nfrab1 3389 . . . . . . . 8 𝑥{𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}
79 rabexg 5230 . . . . . . . 8 (𝐴𝑉 → {𝑥𝐴 ∣ (♯‘𝑥) = 0} ∈ V)
80 rabexg 5230 . . . . . . . 8 (𝐴𝑉 → {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈ V)
81 rabnc 4344 . . . . . . . . 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 31199 . . . . . . 7 (𝐴𝑉 → Σ*𝑥 ∈ ({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0})(♯‘𝑥) = (Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒 Σ*𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥)))
8676, 85syl5eqr 2874 . . . . . 6 (𝐴𝑉 → Σ*𝑥𝐴(♯‘𝑥) = (Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒 Σ*𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥)))
8786adantr 481 . . . . 5 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥𝐴(♯‘𝑥) = (Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒 Σ*𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥)))
88 nfv 1908 . . . . . . 7 𝑥(𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin)
8980adantr 481 . . . . . . 7 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈ V)
90 simpr 485 . . . . . . . . 9 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ 𝐴 ∈ Fin)
91 dfrab3 4281 . . . . . . . . . . . 12 {𝑥𝐴 ∣ (♯‘𝑥) = 0} = (𝐴 ∩ {𝑥 ∣ (♯‘𝑥) = 0})
92 hasheq0 13717 . . . . . . . . . . . . . . . 16 (𝑥 ∈ V → ((♯‘𝑥) = 0 ↔ 𝑥 = ∅))
9339, 92ax-mp 5 . . . . . . . . . . . . . . 15 ((♯‘𝑥) = 0 ↔ 𝑥 = ∅)
9493abbii 2890 . . . . . . . . . . . . . 14 {𝑥 ∣ (♯‘𝑥) = 0} = {𝑥𝑥 = ∅}
95 df-sn 4564 . . . . . . . . . . . . . 14 {∅} = {𝑥𝑥 = ∅}
9694, 95eqtr4i 2851 . . . . . . . . . . . . 13 {𝑥 ∣ (♯‘𝑥) = 0} = {∅}
9796ineq2i 4189 . . . . . . . . . . . 12 (𝐴 ∩ {𝑥 ∣ (♯‘𝑥) = 0}) = (𝐴 ∩ {∅})
9891, 97eqtri 2848 . . . . . . . . . . 11 {𝑥𝐴 ∣ (♯‘𝑥) = 0} = (𝐴 ∩ {∅})
99 snfi 8586 . . . . . . . . . . . 12 {∅} ∈ Fin
100 inss2 4209 . . . . . . . . . . . 12 (𝐴 ∩ {∅}) ⊆ {∅}
101 ssfi 8730 . . . . . . . . . . . 12 (({∅} ∈ Fin ∧ (𝐴 ∩ {∅}) ⊆ {∅}) → (𝐴 ∩ {∅}) ∈ Fin)
10299, 100, 101mp2an 688 . . . . . . . . . . 11 (𝐴 ∩ {∅}) ∈ Fin
10398, 102eqeltri 2913 . . . . . . . . . 10 {𝑥𝐴 ∣ (♯‘𝑥) = 0} ∈ Fin
104103a1i 11 . . . . . . . . 9 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → {𝑥𝐴 ∣ (♯‘𝑥) = 0} ∈ Fin)
105 difinf 8780 . . . . . . . . 9 ((¬ 𝐴 ∈ Fin ∧ {𝑥𝐴 ∣ (♯‘𝑥) = 0} ∈ Fin) → ¬ (𝐴 ∖ {𝑥𝐴 ∣ (♯‘𝑥) = 0}) ∈ Fin)
10690, 104, 105syl2anc 584 . . . . . . . 8 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (𝐴 ∖ {𝑥𝐴 ∣ (♯‘𝑥) = 0}) ∈ Fin)
107 notrab 4283 . . . . . . . . 9 (𝐴 ∖ {𝑥𝐴 ∣ (♯‘𝑥) = 0}) = {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}
108107eleq1i 2907 . . . . . . . 8 ((𝐴 ∖ {𝑥𝐴 ∣ (♯‘𝑥) = 0}) ∈ Fin ↔ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈ Fin)
109106, 108sylnib 329 . . . . . . 7 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈ Fin)
11050a1i 11 . . . . . . 7 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → (♯‘𝑥) ∈ (0[,]+∞))
11139a1i 11 . . . . . . . 8 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 𝑥 ∈ V)
112 simpr 485 . . . . . . . . . . 11 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0})
113 rabid 3383 . . . . . . . . . . 11 (𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} ↔ (𝑥𝐴 ∧ ¬ (♯‘𝑥) = 0))
114112, 113sylib 219 . . . . . . . . . 10 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → (𝑥𝐴 ∧ ¬ (♯‘𝑥) = 0))
115114simprd 496 . . . . . . . . 9 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → ¬ (♯‘𝑥) = 0)
11693biimpri 229 . . . . . . . . . 10 (𝑥 = ∅ → (♯‘𝑥) = 0)
117116necon3bi 3046 . . . . . . . . 9 (¬ (♯‘𝑥) = 0 → 𝑥 ≠ ∅)
118115, 117syl 17 . . . . . . . 8 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 𝑥 ≠ ∅)
119 hashge1 13743 . . . . . . . 8 ((𝑥 ∈ V ∧ 𝑥 ≠ ∅) → 1 ≤ (♯‘𝑥))
120111, 118, 119syl2anc 584 . . . . . . 7 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 1 ≤ (♯‘𝑥))
121 1xr 10692 . . . . . . . 8 1 ∈ ℝ*
122121a1i 11 . . . . . . 7 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → 1 ∈ ℝ*)
123 0lt1 11154 . . . . . . . 8 0 < 1
124123a1i 11 . . . . . . 7 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → 0 < 1)
12588, 78, 89, 109, 110, 120, 122, 124esumpinfsum 31223 . . . . . 6 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥) = +∞)
126125oveq2d 7167 . . . . 5 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → (Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒 Σ*𝑥 ∈ {𝑥𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥)) = (Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒 +∞))
127 iccssxr 12812 . . . . . . 7 (0[,]+∞) ⊆ ℝ*
12879adantr 481 . . . . . . . 8 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → {𝑥𝐴 ∣ (♯‘𝑥) = 0} ∈ V)
12950a1i 11 . . . . . . . . 9 (((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0}) → (♯‘𝑥) ∈ (0[,]+∞))
130129ralrimiva 3186 . . . . . . . 8 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → ∀𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞))
13177esumcl 31176 . . . . . . . 8 (({𝑥𝐴 ∣ (♯‘𝑥) = 0} ∈ V ∧ ∀𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞)) → Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞))
132128, 130, 131syl2anc 584 . . . . . . 7 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞))
133127, 132sseldi 3968 . . . . . 6 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ ℝ*)
134 xrge0neqmnf 12833 . . . . . . 7 *𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞) → Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ≠ -∞)
135132, 134syl 17 . . . . . 6 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ≠ -∞)
136 xaddpnf1 12612 . . . . . 6 ((Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ ℝ* ∧ Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ≠ -∞) → (Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒 +∞) = +∞)
137133, 135, 136syl2anc 584 . . . . 5 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → (Σ*𝑥 ∈ {𝑥𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +𝑒 +∞) = +∞)
13887, 126, 1373eqtrd 2864 . . . 4 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ*𝑥𝐴(♯‘𝑥) = +∞)
13966, 138eqtr4d 2863 . . 3 ((𝐴𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
140139adantlr 711 . 2 (((𝐴𝑉Disj 𝑥𝐴 𝑥) ∧ ¬ 𝐴 ∈ Fin) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
14159, 140pm2.61dan 809 1 ((𝐴𝑉Disj 𝑥𝐴 𝑥) → (♯‘ 𝐴) = Σ*𝑥𝐴(♯‘𝑥))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 843  w3a 1081   = wceq 1530  wtru 1531  wcel 2106  {cab 2802  wne 3020  wral 3142  wrex 3143  {crab 3146  Vcvv 3499  cdif 3936  cun 3937  cin 3938  wss 3939  c0 4294  𝒫 cpw 4541  {csn 4563   cuni 4836  Disj wdisj 5027   class class class wbr 5062  wf 6347  cfv 6351  (class class class)co 7151  Fincfn 8501  cr 10528  0cc0 10529  1c1 10530  +∞cpnf 10664  -∞cmnf 10665  *cxr 10666   < clt 10667  cle 10668  0cn0 11889   +𝑒 cxad 12498  [,)cico 12733  [,]cicc 12734  chash 13683  Σcsu 15035  Σ*cesum 31173
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-13 2385  ax-ext 2796  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-inf2 9096  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2615  df-eu 2649  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-iin 4919  df-disj 5028  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-se 5513  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-isom 6360  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7402  df-om 7572  df-1st 7683  df-2nd 7684  df-supp 7825  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-er 8282  df-map 8401  df-pm 8402  df-ixp 8454  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-fsupp 8826  df-fi 8867  df-sup 8898  df-inf 8899  df-oi 8966  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-xnn0 11960  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12383  df-xneg 12500  df-xadd 12501  df-xmul 12502  df-ioo 12735  df-ioc 12736  df-ico 12737  df-icc 12738  df-fz 12886  df-fzo 13027  df-fl 13155  df-mod 13231  df-seq 13363  df-exp 13423  df-fac 13627  df-bc 13656  df-hash 13684  df-shft 14419  df-cj 14451  df-re 14452  df-im 14453  df-sqrt 14587  df-abs 14588  df-limsup 14821  df-clim 14838  df-rlim 14839  df-sum 15036  df-ef 15413  df-sin 15415  df-cos 15416  df-pi 15418  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-hom 16581  df-cco 16582  df-rest 16688  df-topn 16689  df-0g 16707  df-gsum 16708  df-topgen 16709  df-pt 16710  df-prds 16713  df-ordt 16766  df-xrs 16767  df-qtop 16772  df-imas 16773  df-xps 16775  df-mre 16849  df-mrc 16850  df-acs 16852  df-ps 17802  df-tsr 17803  df-plusf 17843  df-mgm 17844  df-sgrp 17892  df-mnd 17903  df-mhm 17946  df-submnd 17947  df-grp 18038  df-minusg 18039  df-sbg 18040  df-mulg 18157  df-subg 18208  df-cntz 18379  df-cmn 18830  df-abl 18831  df-mgp 19162  df-ur 19174  df-ring 19221  df-cring 19222  df-subrg 19455  df-abv 19510  df-lmod 19558  df-scaf 19559  df-sra 19866  df-rgmod 19867  df-psmet 20453  df-xmet 20454  df-met 20455  df-bl 20456  df-mopn 20457  df-fbas 20458  df-fg 20459  df-cnfld 20462  df-top 21418  df-topon 21435  df-topsp 21457  df-bases 21470  df-cld 21543  df-ntr 21544  df-cls 21545  df-nei 21622  df-lp 21660  df-perf 21661  df-cn 21751  df-cnp 21752  df-haus 21839  df-tx 22086  df-hmeo 22279  df-fil 22370  df-fm 22462  df-flim 22463  df-flf 22464  df-tmd 22596  df-tgp 22597  df-tsms 22650  df-trg 22683  df-xms 22845  df-ms 22846  df-tms 22847  df-nm 23107  df-ngp 23108  df-nrg 23110  df-nlm 23111  df-ii 23400  df-cncf 23401  df-limc 24379  df-dv 24380  df-log 25053  df-esum 31174
This theorem is referenced by:  cntmeas  31372
  Copyright terms: Public domain W3C validator