Theorem sge0fodjrnlem 43055

Description: Re-index a nonnegative extended sum using an onto function with disjoint range, when the empty set is assigned 0 in the sum (this is true, for example, both for measures and outer measures). (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypotheses

Ref	Expression
sge0fodjrnlem.k	⊢ Ⅎ𝑘𝜑
sge0fodjrnlem.n	⊢ Ⅎ𝑛𝜑
sge0fodjrnlem.bd	⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)
sge0fodjrnlem.c	⊢ (𝜑 → 𝐶 ∈ 𝑉)
sge0fodjrnlem.f	⊢ (𝜑 → 𝐹:𝐶–onto→𝐴)
sge0fodjrnlem.dj	⊢ (𝜑 → Disj 𝑛 ∈ 𝐶 (𝐹‘𝑛))
sge0fodjrnlem.fng	⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)
sge0fodjrnlem.b	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
sge0fodjrnlem.b0	⊢ ((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0)
sge0fodjrnlem.z	⊢ 𝑍 = (◡𝐹 “ {∅})

Assertion

Ref	Expression
sge0fodjrnlem	⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))

Distinct variable groups:   𝐴,𝑘,𝑛   𝐵,𝑛   𝐶,𝑘,𝑛   𝐷,𝑘   𝑘,𝐹,𝑛   𝑘,𝐺   𝑘,𝑍,𝑛

Allowed substitution hints:   𝜑(𝑘,𝑛)   𝐵(𝑘)   𝐷(𝑛)   𝐺(𝑛)   𝑉(𝑘,𝑛)

Proof of Theorem sge0fodjrnlem

Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sge0fodjrnlem.k	. . . 4 ⊢ Ⅎ𝑘𝜑
2		sge0fodjrnlem.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
3		sge0fodjrnlem.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝐶–onto→𝐴)
4		fornex 7639	. . . . 5 ⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V))
5	2, 3, 4	sylc 65	. . . 4 ⊢ (𝜑 → 𝐴 ∈ V)
6		difssd 4060	. . . 4 ⊢ (𝜑 → (𝐴 ∖ {∅}) ⊆ 𝐴)
7		simpl 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝜑)
8	6	sselda 3915	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝑘 ∈ 𝐴)
9		sge0fodjrnlem.b	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
10	7, 8, 9	syl2anc 587	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝐵 ∈ (0[,]+∞))
11		simpl 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝜑)
12		dfin4 4194	. . . . . . . . . 10 ⊢ (𝐴 ∩ {∅}) = (𝐴 ∖ (𝐴 ∖ {∅}))
13	12	eqcomi 2807	. . . . . . . . 9 ⊢ (𝐴 ∖ (𝐴 ∖ {∅})) = (𝐴 ∩ {∅})
14		inss2 4156	. . . . . . . . 9 ⊢ (𝐴 ∩ {∅}) ⊆ {∅}
15	13, 14	eqsstri 3949	. . . . . . . 8 ⊢ (𝐴 ∖ (𝐴 ∖ {∅})) ⊆ {∅}
16		id 22	. . . . . . . 8 ⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})))
17	15, 16	sseldi 3913	. . . . . . 7 ⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈ {∅})
18		elsni 4542	. . . . . . 7 ⊢ (𝑘 ∈ {∅} → 𝑘 = ∅)
19	17, 18	syl 17	. . . . . 6 ⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 = ∅)
20	19	adantl 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝑘 = ∅)
21		sge0fodjrnlem.b0	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0)
22	11, 20, 21	syl2anc 587	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝐵 = 0)
23	1, 5, 6, 10, 22	sge0ss 43051	. . 3 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) = (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)))
24	23	eqcomd 2804	. 2 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)))
25		sge0fodjrnlem.n	. . 3 ⊢ Ⅎ𝑛𝜑
26		sge0fodjrnlem.bd	. . 3 ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)
27		difexg 5195	. . . 4 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∖ 𝑍) ∈ V)
28	2, 27	syl 17	. . 3 ⊢ (𝜑 → (𝐶 ∖ 𝑍) ∈ V)
29		eqid 2798	. . . . 5 ⊢ (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
30		fof 6565	. . . . . . 7 ⊢ (𝐹:𝐶–onto→𝐴 → 𝐹:𝐶⟶𝐴)
31	3, 30	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐶⟶𝐴)
32	31	ffvelrnda 6828	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴)
33		sge0fodjrnlem.dj	. . . . 5 ⊢ (𝜑 → Disj 𝑛 ∈ 𝐶 (𝐹‘𝑛))
34		fveq2 6645	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
35	34	neeq1d 3046	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ≠ ∅ ↔ (𝐹‘𝑛) ≠ ∅))
36	35	cbvrabv 3439	. . . . 5 ⊢ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} = {𝑛 ∈ 𝐶 ∣ (𝐹‘𝑛) ≠ ∅}
37	34	cbvmptv 5133	. . . . . . 7 ⊢ (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
38	37	rneqi 5771	. . . . . 6 ⊢ ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
39	38	difeq1i 4046	. . . . 5 ⊢ (ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}) = (ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ∖ {∅})
40	25, 29, 32, 33, 36, 39	disjf1o 41818	. . . 4 ⊢ (𝜑 → ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}))
41	31	feqmptd 6708	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)))
42		difssd 4060	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 ∖ 𝑍) ⊆ 𝐶)
43	42	sselda 3915	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶)
44		eldifi 4054	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝑛 ∈ 𝐶)
45	44	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝐶)
46		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑛) = ∅ → (𝐹‘𝑛) = ∅)
47		fvex 6658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘𝑛) ∈ V
48	47	elsn 4540	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑛) ∈ {∅} ↔ (𝐹‘𝑛) = ∅)
49	46, 48	sylibr 237	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑛) = ∅ → (𝐹‘𝑛) ∈ {∅})
50	49	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → (𝐹‘𝑛) ∈ {∅})
51	45, 50	jca 515	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))
52	51	adantll 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))
53	31	ffnd 6488	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 Fn 𝐶)
54		elpreima 6805	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn 𝐶 → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})))
55	53, 54	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})))
56	55	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})))
57	52, 56	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ (◡𝐹 “ {∅}))
58		sge0fodjrnlem.z	. . . . . . . . . . . . . . 15 ⊢ 𝑍 = (◡𝐹 “ {∅})
59	57, 58	eleqtrrdi 2901	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝑍)
60		eldifn 4055	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → ¬ 𝑛 ∈ 𝑍)
61	60	ad2antlr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → ¬ 𝑛 ∈ 𝑍)
62	59, 61	pm2.65da 816	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ¬ (𝐹‘𝑛) = ∅)
63	62	neqned 2994	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝐹‘𝑛) ≠ ∅)
64	43, 63	jca 515	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ≠ ∅))
65	35	elrab 3628	. . . . . . . . . . 11 ⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ≠ ∅))
66	64, 65	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})
67	66	ex 416	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
68	65	simplbi 501	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ 𝐶)
69	68	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → 𝑛 ∈ 𝐶)
70	58	eleq2i 2881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (◡𝐹 “ {∅}))
71	70	biimpi 219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (◡𝐹 “ {∅}))
72	71	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (◡𝐹 “ {∅}))
73	55	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 ∈ (◡𝐹 “ {∅}) ↔ (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅})))
74	72, 73	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ∈ {∅}))
75	74	simprd 499	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ {∅})
76		elsni 4542	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑛) ∈ {∅} → (𝐹‘𝑛) = ∅)
77	75, 76	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ∅)
78	77	adantlr 714	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ∅)
79	65	simprbi 500	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → (𝐹‘𝑛) ≠ ∅)
80	79	ad2antlr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ≠ ∅)
81	80	neneqd 2992	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → ¬ (𝐹‘𝑛) = ∅)
82	78, 81	pm2.65da 816	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → ¬ 𝑛 ∈ 𝑍)
83	69, 82	eldifd 3892	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → 𝑛 ∈ (𝐶 ∖ 𝑍))
84	83	ex 416	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍)))
85	25, 84	ralrimi 3180	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍))
86		dfss3 3903	. . . . . . . . . . 11 ⊢ ({𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍) ↔ ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍))
87	85, 86	sylibr 237	. . . . . . . . . 10 ⊢ (𝜑 → {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍))
88	87	sseld 3914	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍)))
89	67, 88	impbid 215	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
90	25, 89	alrimi 2211	. . . . . . 7 ⊢ (𝜑 → ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
91		dfcleq 2792	. . . . . . 7 ⊢ ((𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ↔ ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
92	90, 91	sylibr 237	. . . . . 6 ⊢ (𝜑 → (𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})
93	41, 92	reseq12d 5819	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)) = ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
94	41, 37	eqtr4di 2851	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)))
95	94	eqcomd 2804	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = 𝐹)
96	95	rneqd 5772	. . . . . . 7 ⊢ (𝜑 → ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran 𝐹)
97		forn 6568	. . . . . . . 8 ⊢ (𝐹:𝐶–onto→𝐴 → ran 𝐹 = 𝐴)
98	3, 97	syl 17	. . . . . . 7 ⊢ (𝜑 → ran 𝐹 = 𝐴)
99	96, 98	eqtr2d 2834	. . . . . 6 ⊢ (𝜑 → 𝐴 = ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)))
100	99	difeq1d 4049	. . . . 5 ⊢ (𝜑 → (𝐴 ∖ {∅}) = (ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}))
101	93, 92, 100	f1oeq123d 6585	. . . 4 ⊢ (𝜑 → ((𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅}) ↔ ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅})))
102	40, 101	mpbird 260	. . 3 ⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅}))
103		fvres 6664	. . . . 5 ⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = (𝐹‘𝑛))
104	103	adantl 485	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = (𝐹‘𝑛))
105		simpl 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝜑)
106		sge0fodjrnlem.fng	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)
107	105, 43, 106	syl2anc 587	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝐹‘𝑛) = 𝐺)
108	104, 107	eqtrd 2833	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = 𝐺)
109	1, 25, 26, 28, 102, 108, 10	sge0f1o 43021	. 2 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) = (Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷)))
110	106	eqcomd 2804	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 = (𝐹‘𝑛))
111	110, 32	eqeltrd 2890	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 ∈ 𝐴)
112	105, 43, 111	syl2anc 587	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐺 ∈ 𝐴)
113	112	ex 416	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝐺 ∈ 𝐴))
114	113	imdistani 572	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝜑 ∧ 𝐺 ∈ 𝐴))
115		nfcv 2955	. . . . 5 ⊢ Ⅎ𝑘𝐺
116		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑘 𝐺 ∈ 𝐴
117	1, 116	nfan 1900	. . . . . 6 ⊢ Ⅎ𝑘(𝜑 ∧ 𝐺 ∈ 𝐴)
118		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑘 𝐷 ∈ (0[,]+∞)
119	117, 118	nfim 1897	. . . . 5 ⊢ Ⅎ𝑘((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))
120		eleq1 2877	. . . . . . 7 ⊢ (𝑘 = 𝐺 → (𝑘 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴))
121	120	anbi2d 631	. . . . . 6 ⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝐺 ∈ 𝐴)))
122	26	eleq1d 2874	. . . . . 6 ⊢ (𝑘 = 𝐺 → (𝐵 ∈ (0[,]+∞) ↔ 𝐷 ∈ (0[,]+∞)))
123	121, 122	imbi12d 348	. . . . 5 ⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))))
124	115, 119, 123, 9	vtoclgf 3513	. . . 4 ⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞)))
125	112, 114, 124	sylc 65	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐷 ∈ (0[,]+∞))
126		simpl 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝜑)
127		eldifi 4054	. . . . . 6 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶)
128	127	adantl 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝐶)
129	126, 128, 111	syl2anc 587	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 ∈ 𝐴)
130		dfin4 4194	. . . . . . . . 9 ⊢ (𝑍 ∩ 𝐶) = (𝑍 ∖ (𝑍 ∖ 𝐶))
131		difss 4059	. . . . . . . . 9 ⊢ (𝑍 ∖ (𝑍 ∖ 𝐶)) ⊆ 𝑍
132	130, 131	eqsstri 3949	. . . . . . . 8 ⊢ (𝑍 ∩ 𝐶) ⊆ 𝑍
133		inss2 4156	. . . . . . . . . 10 ⊢ (𝐶 ∩ 𝑍) ⊆ 𝑍
134		id 22	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)))
135		dfin4 4194	. . . . . . . . . . . 12 ⊢ (𝐶 ∩ 𝑍) = (𝐶 ∖ (𝐶 ∖ 𝑍))
136	135	eqcomi 2807	. . . . . . . . . . 11 ⊢ (𝐶 ∖ (𝐶 ∖ 𝑍)) = (𝐶 ∩ 𝑍)
137	134, 136	eleqtrdi 2900	. . . . . . . . . 10 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∩ 𝑍))
138	133, 137	sseldi 3913	. . . . . . . . 9 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍)
139	138, 127	elind 4121	. . . . . . . 8 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝑍 ∩ 𝐶))
140	132, 139	sseldi 3913	. . . . . . 7 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍)
141	140	adantl 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝑍)
142	77	eqcomd 2804	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∅ = (𝐹‘𝑛))
143		simpl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝜑)
144	74	simpld 498	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝐶)
145	143, 144, 106	syl2anc 587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = 𝐺)
146	142, 145	eqtr2d 2834	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐺 = ∅)
147	126, 141, 146	syl2anc 587	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 = ∅)
148	126, 147	jca 515	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → (𝜑 ∧ 𝐺 = ∅))
149		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑘 𝐺 = ∅
150	1, 149	nfan 1900	. . . . . 6 ⊢ Ⅎ𝑘(𝜑 ∧ 𝐺 = ∅)
151		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑘 𝐷 = 0
152	150, 151	nfim 1897	. . . . 5 ⊢ Ⅎ𝑘((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0)
153		eqeq1 2802	. . . . . . 7 ⊢ (𝑘 = 𝐺 → (𝑘 = ∅ ↔ 𝐺 = ∅))
154	153	anbi2d 631	. . . . . 6 ⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 = ∅) ↔ (𝜑 ∧ 𝐺 = ∅)))
155	26	eqeq1d 2800	. . . . . 6 ⊢ (𝑘 = 𝐺 → (𝐵 = 0 ↔ 𝐷 = 0))
156	154, 155	imbi12d 348	. . . . 5 ⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0) ↔ ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0)))
157	115, 152, 156, 21	vtoclgf 3513	. . . 4 ⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0))
158	129, 148, 157	sylc 65	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐷 = 0)
159	25, 2, 42, 125, 158	sge0ss 43051	. 2 ⊢ (𝜑 → (Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
160	24, 109, 159	3eqtrd 2837	1 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538  Ⅎwnf 1785   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  {crab 3110  Vcvv 3441   ∖ cdif 3878   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  {csn 4525  Disj wdisj 4995   ↦ cmpt 5110  ^◡ccnv 5518  ran crn 5520   ↾ cres 5521   “ cima 5522   Fn wfn 6319  ⟶wf 6320  –onto→wfo 6322  –1-1-onto→wf1o 6323  ‘cfv 6324  (class class class)co 7135  0cc0 10526  +∞cpnf 10661  [,]cicc 12729  Σ^{^}csumge0 43001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-inf2 9088  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-disj 4996  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-sup 8890  df-oi 8958  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-xadd 12496  df-ico 12732  df-icc 12733  df-fz 12886  df-fzo 13029  df-seq 13365  df-exp 13426  df-hash 13687  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-clim 14837  df-sum 15035  df-sumge0 43002

This theorem is referenced by:  sge0fodjrn  43056