hasheuni - Mathbox for Thierry Arnoux

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

Theorem hasheuni 34699

Description: The cardinality of a disjoint union, not necessarily finite. cf. hashuni 15973. (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**
Step	Hyp	Ref	Expression
1		nfdisj1 5084	. . . . . . . 8 ⊢ Ⅎ𝑥Disj 𝑥 ∈ 𝐴 𝑥
2		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑥 𝐴 ∈ Fin
3		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑥 𝐴 ⊆ Fin
4	1, 2, 3	nf3an 1934	. . . . . . 7 ⊢ Ⅎ𝑥(Disj 𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin)
5		simp2 1155	. . . . . . 7 ⊢ ((Disj 𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin)
6		simp3 1156	. . . . . . 7 ⊢ ((Disj 𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ⊆ Fin)
7		simp1 1154	. . . . . . 7 ⊢ ((Disj 𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Disj 𝑥 ∈ 𝐴 𝑥)
8	4, 5, 6, 7	hashunif 33380	. . . . . 6 ⊢ ((Disj 𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ𝑥 ∈ 𝐴 (♯‘𝑥))
9		simpl 488	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin)
10		dfss3 3920	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ Fin ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ Fin)
11		hashcl 14480	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ Fin → (♯‘𝑥) ∈ ℕ₀)
12		nn0re 12596	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑥) ∈ ℕ₀ → (♯‘𝑥) ∈ ℝ)
13		nn0ge0 12612	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑥) ∈ ℕ₀ → 0 ≤ (♯‘𝑥))
14		elrege0 13566	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑥) ∈ (0[,)+∞) ↔ ((♯‘𝑥) ∈ ℝ ∧ 0 ≤ (♯‘𝑥)))
15	12, 13, 14	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑥) ∈ ℕ₀ → (♯‘𝑥) ∈ (0[,)+∞))
16	11, 15	syl 18	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ Fin → (♯‘𝑥) ∈ (0[,)+∞))
17	16	ralimi 3100	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ Fin → ∀𝑥 ∈ 𝐴 (♯‘𝑥) ∈ (0[,)+∞))
18	10, 17	sylbi 220	. . . . . . . . . 10 ⊢ (𝐴 ⊆ Fin → ∀𝑥 ∈ 𝐴 (♯‘𝑥) ∈ (0[,)+∞))
19	18	r19.21bi 3255	. . . . . . . . 9 ⊢ ((𝐴 ⊆ Fin ∧ 𝑥 ∈ 𝐴) → (♯‘𝑥) ∈ (0[,)+∞))
20	19	adantll 727	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑥 ∈ 𝐴) → (♯‘𝑥) ∈ (0[,)+∞))
21	9, 20	esumpfinval 34689	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ^*𝑥 ∈ 𝐴(♯‘𝑥) = Σ𝑥 ∈ 𝐴 (♯‘𝑥))
22	21	3adant1 1148	. . . . . 6 ⊢ ((Disj 𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Σ^*𝑥 ∈ 𝐴(♯‘𝑥) = Σ𝑥 ∈ 𝐴 (♯‘𝑥))
23	8, 22	eqtr4d 2799	. . . . 5 ⊢ ((Disj 𝑥 ∈ 𝐴 𝑥 ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ^*𝑥 ∈ 𝐴(♯‘𝑥))
24	23	3adant1l 1195	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ^*𝑥 ∈ 𝐴(♯‘𝑥))
25	24	3expa 1136	. . 3 ⊢ ((((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) ∧ 𝐴 ∈ Fin) ∧ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ^*𝑥 ∈ 𝐴(♯‘𝑥))
26		uniexg 7746	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
27	10	notbii 323	. . . . . . . . . 10 ⊢ (¬ 𝐴 ⊆ Fin ↔ ¬ ∀𝑥 ∈ 𝐴 𝑥 ∈ Fin)
28		rexnal 3115	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ Fin ↔ ¬ ∀𝑥 ∈ 𝐴 𝑥 ∈ Fin)
29	27, 28	bitr4i 281	. . . . . . . . 9 ⊢ (¬ 𝐴 ⊆ Fin ↔ ∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ Fin)
30		elssuni 4899	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
31		ssfi 9172	. . . . . . . . . . . . 13 ⊢ ((∪ 𝐴 ∈ Fin ∧ 𝑥 ⊆ ∪ 𝐴) → 𝑥 ∈ Fin)
32	31	expcom 419	. . . . . . . . . . . 12 ⊢ (𝑥 ⊆ ∪ 𝐴 → (∪ 𝐴 ∈ Fin → 𝑥 ∈ Fin))
33	32	con3d 153	. . . . . . . . . . 11 ⊢ (𝑥 ⊆ ∪ 𝐴 → (¬ 𝑥 ∈ Fin → ¬ ∪ 𝐴 ∈ Fin))
34	30, 33	syl 18	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → (¬ 𝑥 ∈ Fin → ¬ ∪ 𝐴 ∈ Fin))
35	34	rexlimiv 3157	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ Fin → ¬ ∪ 𝐴 ∈ Fin)
36	29, 35	sylbi 220	. . . . . . . 8 ⊢ (¬ 𝐴 ⊆ Fin → ¬ ∪ 𝐴 ∈ Fin)
37		hashinf 14459	. . . . . . . 8 ⊢ ((∪ 𝐴 ∈ V ∧ ¬ ∪ 𝐴 ∈ Fin) → (♯‘∪ 𝐴) = +∞)
38	26, 36, 37	syl2an 608	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = +∞)
39		vex 3455	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
40		hashinf 14459	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ V ∧ ¬ 𝑥 ∈ Fin) → (♯‘𝑥) = +∞)
41	39, 40	mpan 703	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ Fin → (♯‘𝑥) = +∞)
42	41	reximi 3101	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ Fin → ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞)
43	29, 42	sylbi 220	. . . . . . . 8 ⊢ (¬ 𝐴 ⊆ Fin → ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞)
44		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑉
45		nfre1 3288	. . . . . . . . . 10 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞
46	44, 45	nfan 1932	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞)
47		simpl 488	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞) → 𝐴 ∈ 𝑉)
48		hashf2 34698	. . . . . . . . . . 11 ⊢ ♯:V⟶(0[,]+∞)
49		ffvelcdm 7073	. . . . . . . . . . 11 ⊢ ((♯:V⟶(0[,]+∞) ∧ 𝑥 ∈ V) → (♯‘𝑥) ∈ (0[,]+∞))
50	48, 39, 49	mp2an 705	. . . . . . . . . 10 ⊢ (♯‘𝑥) ∈ (0[,]+∞)
51	50	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞) ∧ 𝑥 ∈ 𝐴) → (♯‘𝑥) ∈ (0[,]+∞))
52		simpr 490	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞) → ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞)
53	46, 47, 51, 52	esumpinfval 34687	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑥 ∈ 𝐴 (♯‘𝑥) = +∞) → Σ^*𝑥 ∈ 𝐴(♯‘𝑥) = +∞)
54	43, 53	sylan2 605	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ⊆ Fin) → Σ^*𝑥 ∈ 𝐴(♯‘𝑥) = +∞)
55	38, 54	eqtr4d 2799	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ^*𝑥 ∈ 𝐴(♯‘𝑥))
56	55	3adant2 1149	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ Fin ∧ ¬ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ^*𝑥 ∈ 𝐴(♯‘𝑥))
57	56	3adant1r 1196	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) ∧ 𝐴 ∈ Fin ∧ ¬ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ^*𝑥 ∈ 𝐴(♯‘𝑥))
58	57	3expa 1136	. . 3 ⊢ ((((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) ∧ 𝐴 ∈ Fin) ∧ ¬ 𝐴 ⊆ Fin) → (♯‘∪ 𝐴) = Σ^*𝑥 ∈ 𝐴(♯‘𝑥))
59	25, 58	pm2.61dan 825	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) ∧ 𝐴 ∈ Fin) → (♯‘∪ 𝐴) = Σ^*𝑥 ∈ 𝐴(♯‘𝑥))
60		pwfi 9294	. . . . . . 7 ⊢ (∪ 𝐴 ∈ Fin ↔ 𝒫 ∪ 𝐴 ∈ Fin)
61		pwuni 4906	. . . . . . . 8 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
62		ssfi 9172	. . . . . . . 8 ⊢ ((𝒫 ∪ 𝐴 ∈ Fin ∧ 𝐴 ⊆ 𝒫 ∪ 𝐴) → 𝐴 ∈ Fin)
63	61, 62	mpan2 704	. . . . . . 7 ⊢ (𝒫 ∪ 𝐴 ∈ Fin → 𝐴 ∈ Fin)
64	60, 63	sylbi 220	. . . . . 6 ⊢ (∪ 𝐴 ∈ Fin → 𝐴 ∈ Fin)
65	64	con3i 155	. . . . 5 ⊢ (¬ 𝐴 ∈ Fin → ¬ ∪ 𝐴 ∈ Fin)
66	26, 65, 37	syl2an 608	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘∪ 𝐴) = +∞)
67		nftru 1837	. . . . . . . . 9 ⊢ Ⅎ𝑥⊤
68		unrab 4261	. . . . . . . . . . 11 ⊢ ({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) = {𝑥 ∈ 𝐴 ∣ ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)}
69		exmid 908	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)
70	69	rgenw 3081	. . . . . . . . . . . 12 ⊢ ∀𝑥 ∈ 𝐴 ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)
71		rabid2 3445	. . . . . . . . . . . 12 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)} ↔ ∀𝑥 ∈ 𝐴 ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0))
72	70, 71	mpbir 234	. . . . . . . . . . 11 ⊢ 𝐴 = {𝑥 ∈ 𝐴 ∣ ((♯‘𝑥) = 0 ∨ ¬ (♯‘𝑥) = 0)}
73	68, 72	eqtr4i 2787	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) = 𝐴
74	73	a1i 11	. . . . . . . . 9 ⊢ (⊤ → ({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) = 𝐴)
75	67, 74	esumeq1d 34649	. . . . . . . 8 ⊢ (⊤ → Σ^𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0})(♯‘𝑥) = Σ^𝑥 ∈ 𝐴(♯‘𝑥))
76	75	mptru 1577	. . . . . . 7 ⊢ Σ^𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0})(♯‘𝑥) = Σ^𝑥 ∈ 𝐴(♯‘𝑥)
77		nfrab1 3432	. . . . . . . 8 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0}
78		nfrab1 3432	. . . . . . . 8 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}
79		rabexg 5299	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∈ V)
80		rabexg 5299	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈ V)
81		rabnc 4341	. . . . . . . . 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 34667	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → Σ^𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∪ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0})(♯‘𝑥) = (Σ^𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +_𝑒 Σ^*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥)))
86	76, 85	eqtr3id 2810	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → Σ^𝑥 ∈ 𝐴(♯‘𝑥) = (Σ^𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +_𝑒 Σ^*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥)))
87	86	adantr 486	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ^𝑥 ∈ 𝐴(♯‘𝑥) = (Σ^𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +_𝑒 Σ^*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥)))
88		nfv 1947	. . . . . . 7 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin)
89	80	adantr 486	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈ V)
90		simpr 490	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ 𝐴 ∈ Fin)
91		dfrab3 4265	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} = (𝐴 ∩ {𝑥 ∣ (♯‘𝑥) = 0})
92		hasheq0 14487	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ V → ((♯‘𝑥) = 0 ↔ 𝑥 = ∅))
93	39, 92	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑥) = 0 ↔ 𝑥 = ∅)
94	93	abbii 2828	. . . . . . . . . . . . . 14 ⊢ {𝑥 ∣ (♯‘𝑥) = 0} = {𝑥 ∣ 𝑥 = ∅}
95		df-sn 4585	. . . . . . . . . . . . . 14 ⊢ {∅} = {𝑥 ∣ 𝑥 = ∅}
96	94, 95	eqtr4i 2787	. . . . . . . . . . . . 13 ⊢ {𝑥 ∣ (♯‘𝑥) = 0} = {∅}
97	96	ineq2i 4163	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ {𝑥 ∣ (♯‘𝑥) = 0}) = (𝐴 ∩ {∅})
98	91, 97	eqtri 2784	. . . . . . . . . . 11 ⊢ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} = (𝐴 ∩ {∅})
99		snfi 9055	. . . . . . . . . . . 12 ⊢ {∅} ∈ Fin
100		inss2 4183	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ {∅}) ⊆ {∅}
101		ssfi 9172	. . . . . . . . . . . 12 ⊢ (({∅} ∈ Fin ∧ (𝐴 ∩ {∅}) ⊆ {∅}) → (𝐴 ∩ {∅}) ∈ Fin)
102	99, 100, 101	mp2an 705	. . . . . . . . . . 11 ⊢ (𝐴 ∩ {∅}) ∈ Fin
103	98, 102	eqeltri 2857	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∈ Fin
104	103	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∈ Fin)
105		difinf 9287	. . . . . . . . 9 ⊢ ((¬ 𝐴 ∈ Fin ∧ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∈ Fin) → ¬ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0}) ∈ Fin)
106	90, 104, 105	syl2anc 596	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0}) ∈ Fin)
107		notrab 4268	. . . . . . . . 9 ⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0}) = {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}
108	107	eleq1i 2852	. . . . . . . 8 ⊢ ((𝐴 ∖ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0}) ∈ Fin ↔ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈ Fin)
109	106, 108	sylnib 331	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ¬ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} ∈ Fin)
110	50	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) → (♯‘𝑥) ∈ (0[,]+∞))
111	39	a1i 11	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 𝑥 ∈ V)
112		rabid 3433	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} ↔ (𝑥 ∈ 𝐴 ∧ ¬ (♯‘𝑥) = 0))
113	112	bilani 510	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) → (𝑥 ∈ 𝐴 ∧ ¬ (♯‘𝑥) = 0))
114	113	simprd 501	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) → ¬ (♯‘𝑥) = 0)
115	93	biimpri 231	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (♯‘𝑥) = 0)
116	115	necon3bi 2982	. . . . . . . . 9 ⊢ (¬ (♯‘𝑥) = 0 → 𝑥 ≠ ∅)
117	114, 116	syl 18	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 𝑥 ≠ ∅)
118		hashge1 14513	. . . . . . . 8 ⊢ ((𝑥 ∈ V ∧ 𝑥 ≠ ∅) → 1 ≤ (♯‘𝑥))
119	111, 117, 118	syl2anc 596	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0}) → 1 ≤ (♯‘𝑥))
120		1xr 11349	. . . . . . . 8 ⊢ 1 ∈ ℝ^*
121	120	a1i 11	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → 1 ∈ ℝ^*)
122		0lt1 11819	. . . . . . . 8 ⊢ 0 < 1
123	122	a1i 11	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → 0 < 1)
124	88, 78, 89, 109, 110, 119, 121, 123	esumpinfsum 34691	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ^*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥) = +∞)
125	124	oveq2d 7428	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (Σ^𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +_𝑒 Σ^𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ (♯‘𝑥) = 0} (♯‘𝑥)) = (Σ^*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +_𝑒 +∞))
126		iccssxr 13542	. . . . . . 7 ⊢ (0[,]+∞) ⊆ ℝ^*
127	79	adantr 486	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∈ V)
128	50	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0}) → (♯‘𝑥) ∈ (0[,]+∞))
129	128	ralrimiva 3155	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ∀𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞))
130	77	esumcl 34644	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} ∈ V ∧ ∀𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞)) → Σ^*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞))
131	127, 129, 130	syl2anc 596	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ^*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞))
132	126, 131	sselid 3929	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ^𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ ℝ^)
133		xrge0neqmnf 13564	. . . . . . 7 ⊢ (Σ^𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ (0[,]+∞) → Σ^𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ≠ -∞)
134	131, 133	syl 18	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ^*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ≠ -∞)
135		xaddpnf1 13337	. . . . . 6 ⊢ ((Σ^𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ∈ ℝ^ ∧ Σ^𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) ≠ -∞) → (Σ^𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +_𝑒 +∞) = +∞)
136	132, 134, 135	syl2anc 596	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (Σ^*𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (♯‘𝑥) = 0} (♯‘𝑥) +_𝑒 +∞) = +∞)
137	87, 125, 136	3eqtrd 2800	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → Σ^*𝑥 ∈ 𝐴(♯‘𝑥) = +∞)
138	66, 137	eqtr4d 2799	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘∪ 𝐴) = Σ^*𝑥 ∈ 𝐴(♯‘𝑥))
139	138	adantlr 728	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) ∧ ¬ 𝐴 ∈ Fin) → (♯‘∪ 𝐴) = Σ^*𝑥 ∈ 𝐴(♯‘𝑥))
140	59, 139	pm2.61dan 825	1 ⊢ ((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) → (♯‘∪ 𝐴) = Σ^*𝑥 ∈ 𝐴(♯‘𝑥))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ⊤wtru 1571 ∈ wcel 2145 {cab 2739 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 {crab 3413 Vcvv 3451 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 𝒫 cpw 4557 {csn 4584 ∪ cuni 4867 Disj wdisj 5070 class class class wbr 5103 ⟶wf 6527 ‘cfv 6531 (class class class)co 7412 Fincfn 8957 ℝcr 11180 0cc0 11181 1c1 11182 +∞cpnf 11321 -∞cmnf 11322 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 ℕ₀cn0 12587 +_𝑒 cxad 13220 [,)cico 13459 [,]cicc 13460 ♯chash 14454 Σcsu 15833 Σ^*cesum 34641

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-inf2 9626 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-pre-sup 11259 ax-addf 11260 ax-mulf 11261

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-disj 5071 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-supp 8162 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-2o 8461 df-oadd 8464 df-er 8701 df-map 8833 df-pm 8834 df-ixp 8910 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-fsupp 9338 df-fi 9387 df-sup 9418 df-inf 9419 df-oi 9488 df-card 10001 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-2 12386 df-3 12387 df-4 12388 df-5 12389 df-6 12390 df-7 12391 df-8 12392 df-9 12393 df-n0 12588 df-xnn0 12661 df-z 12675 df-dec 12796 df-uz 12947 df-q 13057 df-rp 13102 df-xneg 13222 df-xadd 13223 df-xmul 13224 df-ioo 13461 df-ioc 13462 df-ico 13463 df-icc 13464 df-fz 13621 df-fzo 13769 df-fl 13912 df-mod 13990 df-seq 14125 df-exp 14185 df-fac 14398 df-bc 14427 df-hash 14455 df-shft 15200 df-cj 15246 df-re 15247 df-im 15248 df-sqrt 15382 df-abs 15383 df-limsup 15618 df-clim 15635 df-rlim 15636 df-sum 15834 df-ef 16213 df-sin 16215 df-cos 16216 df-pi 16218 df-struct 17305 df-sets 17322 df-slot 17340 df-ndx 17352 df-base 17368 df-ress 17389 df-plusg 17421 df-mulr 17422 df-starv 17423 df-sca 17424 df-vsca 17425 df-ip 17426 df-tset 17427 df-ple 17428 df-ds 17430 df-unif 17431 df-hom 17432 df-cco 17433 df-rest 17573 df-topn 17574 df-0g 17592 df-gsum 17593 df-topgen 17594 df-pt 17595 df-prds 17598 df-ordt 17653 df-xrs 17654 df-qtop 17659 df-imas 17660 df-xps 17662 df-mre 17736 df-mrc 17737 df-acs 17739 df-ps 18720 df-tsr 18721 df-plusf 18795 df-mgm 18796 df-sgrp 18888 df-mnd 18904 df-mhm 18958 df-submnd 18959 df-grp 19127 df-minusg 19128 df-sbg 19129 df-mulg 19258 df-subg 19313 df-cntz 19511 df-cmn 19976 df-abl 19977 df-mgp 20341 df-rng 20355 df-ur 20388 df-ring 20441 df-cring 20442 df-subrng 20778 df-subrg 20802 df-abv 21046 df-lmod 21117 df-scaf 21118 df-sra 21428 df-rgmod 21429 df-psmet 21650 df-xmet 21651 df-met 21652 df-bl 21653 df-mopn 21654 df-fbas 21655 df-fg 21656 df-cnfld 21659 df-top 23192 df-topon 23209 df-topsp 23231 df-bases 23244 df-cld 23317 df-ntr 23318 df-cls 23319 df-nei 23396 df-lp 23434 df-perf 23435 df-cn 23525 df-cnp 23526 df-haus 23613 df-tx 23861 df-hmeo 24054 df-fil 24145 df-fm 24237 df-flim 24238 df-flf 24239 df-tmd 24371 df-tgp 24372 df-tsms 24426 df-trg 24459 df-xms 24619 df-ms 24620 df-tms 24621 df-nm 24881 df-ngp 24882 df-nrg 24884 df-nlm 24885 df-ii 25178 df-cncf 25179 df-limc 26166 df-dv 26167 df-log 26866 df-esum 34642

This theorem is used by: cntmeas 34841

W3C validator