Theorem sge0fodjrnlem 43421

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 7661	. . . . 5 ⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V))
5	2, 3, 4	sylc 65	. . . 4 ⊢ (𝜑 → 𝐴 ∈ V)
6		difssd 4038	. . . 4 ⊢ (𝜑 → (𝐴 ∖ {∅}) ⊆ 𝐴)
7		simpl 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝜑)
8	6	sselda 3892	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝑘 ∈ 𝐴)
9		sge0fodjrnlem.b	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
10	7, 8, 9	syl2anc 587	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ {∅})) → 𝐵 ∈ (0[,]+∞))
11		simpl 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅}))) → 𝜑)
12		dfin4 4172	. . . . . . . . . 10 ⊢ (𝐴 ∩ {∅}) = (𝐴 ∖ (𝐴 ∖ {∅}))
13	12	eqcomi 2767	. . . . . . . . 9 ⊢ (𝐴 ∖ (𝐴 ∖ {∅})) = (𝐴 ∩ {∅})
14		inss2 4134	. . . . . . . . 9 ⊢ (𝐴 ∩ {∅}) ⊆ {∅}
15	13, 14	eqsstri 3926	. . . . . . . 8 ⊢ (𝐴 ∖ (𝐴 ∖ {∅})) ⊆ {∅}
16		id 22	. . . . . . . 8 ⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})))
17	15, 16	sseldi 3890	. . . . . . 7 ⊢ (𝑘 ∈ (𝐴 ∖ (𝐴 ∖ {∅})) → 𝑘 ∈ {∅})
18		elsni 4539	. . . . . . 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 43417	. . 3 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) = (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)))
24	23	eqcomd 2764	. 2 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)))
25		sge0fodjrnlem.n	. . 3 ⊢ Ⅎ𝑛𝜑
26		sge0fodjrnlem.bd	. . 3 ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)
27		difexg 5197	. . . 4 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∖ 𝑍) ∈ V)
28	2, 27	syl 17	. . 3 ⊢ (𝜑 → (𝐶 ∖ 𝑍) ∈ V)
29		eqid 2758	. . . . 5 ⊢ (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
30		fof 6576	. . . . . . 7 ⊢ (𝐹:𝐶–onto→𝐴 → 𝐹:𝐶⟶𝐴)
31	3, 30	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐶⟶𝐴)
32	31	ffvelrnda 6842	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴)
33		sge0fodjrnlem.dj	. . . . 5 ⊢ (𝜑 → Disj 𝑛 ∈ 𝐶 (𝐹‘𝑛))
34		fveq2 6658	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
35	34	neeq1d 3010	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ≠ ∅ ↔ (𝐹‘𝑛) ≠ ∅))
36	35	cbvrabv 3404	. . . . 5 ⊢ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} = {𝑛 ∈ 𝐶 ∣ (𝐹‘𝑛) ≠ ∅}
37	34	cbvmptv 5135	. . . . . . 7 ⊢ (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
38	37	rneqi 5778	. . . . . 6 ⊢ ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛))
39	38	difeq1i 4024	. . . . 5 ⊢ (ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}) = (ran (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ∖ {∅})
40	25, 29, 32, 33, 36, 39	disjf1o 42188	. . . 4 ⊢ (𝜑 → ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}))
41	31	feqmptd 6721	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)))
42		difssd 4038	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 ∖ 𝑍) ⊆ 𝐶)
43	42	sselda 3892	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶)
44		eldifi 4032	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝑛 ∈ 𝐶)
45	44	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (𝐶 ∖ 𝑍) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝐶)
46		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑛) = ∅ → (𝐹‘𝑛) = ∅)
47		fvex 6671	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘𝑛) ∈ V
48	47	elsn 4537	. . . . . . . . . . . . . . . . . . . 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 6499	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 Fn 𝐶)
54		elpreima 6819	. . . . . . . . . . . . . . . . . 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 2863	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → 𝑛 ∈ 𝑍)
60		eldifn 4033	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (𝐶 ∖ 𝑍) → ¬ 𝑛 ∈ 𝑍)
61	60	ad2antlr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) ∧ (𝐹‘𝑛) = ∅) → ¬ 𝑛 ∈ 𝑍)
62	59, 61	pm2.65da 816	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ¬ (𝐹‘𝑛) = ∅)
63	62	neqned 2958	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝐹‘𝑛) ≠ ∅)
64	43, 63	jca 515	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) ≠ ∅))
65	35	elrab 3602	. . . . . . . . . . 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 2843	. . . . . . . . . . . . . . . . . . . . 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 4539	. . . . . . . . . . . . . . . . 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 2956	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) ∧ 𝑛 ∈ 𝑍) → ¬ (𝐹‘𝑛) = ∅)
82	78, 81	pm2.65da 816	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → ¬ 𝑛 ∈ 𝑍)
83	69, 82	eldifd 3869	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}) → 𝑛 ∈ (𝐶 ∖ 𝑍))
84	83	ex 416	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍)))
85	25, 84	ralrimi 3144	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍))
86		dfss3 3880	. . . . . . . . . . 11 ⊢ ({𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍) ↔ ∀𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}𝑛 ∈ (𝐶 ∖ 𝑍))
87	85, 86	sylibr 237	. . . . . . . . . 10 ⊢ (𝜑 → {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ⊆ (𝐶 ∖ 𝑍))
88	87	sseld 3891	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} → 𝑛 ∈ (𝐶 ∖ 𝑍)))
89	67, 88	impbid 215	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
90	25, 89	alrimi 2211	. . . . . . 7 ⊢ (𝜑 → ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
91		dfcleq 2751	. . . . . . 7 ⊢ ((𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅} ↔ ∀𝑛(𝑛 ∈ (𝐶 ∖ 𝑍) ↔ 𝑛 ∈ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
92	90, 91	sylibr 237	. . . . . 6 ⊢ (𝜑 → (𝐶 ∖ 𝑍) = {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅})
93	41, 92	reseq12d 5824	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)) = ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}))
94	41, 37	eqtr4di 2811	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)))
95	94	eqcomd 2764	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = 𝐹)
96	95	rneqd 5779	. . . . . . 7 ⊢ (𝜑 → ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) = ran 𝐹)
97		forn 6579	. . . . . . . 8 ⊢ (𝐹:𝐶–onto→𝐴 → ran 𝐹 = 𝐴)
98	3, 97	syl 17	. . . . . . 7 ⊢ (𝜑 → ran 𝐹 = 𝐴)
99	96, 98	eqtr2d 2794	. . . . . 6 ⊢ (𝜑 → 𝐴 = ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)))
100	99	difeq1d 4027	. . . . 5 ⊢ (𝜑 → (𝐴 ∖ {∅}) = (ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅}))
101	93, 92, 100	f1oeq123d 6596	. . . 4 ⊢ (𝜑 → ((𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅}) ↔ ((𝑛 ∈ 𝐶 ↦ (𝐹‘𝑛)) ↾ {𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}):{𝑚 ∈ 𝐶 ∣ (𝐹‘𝑚) ≠ ∅}–1-1-onto→(ran (𝑚 ∈ 𝐶 ↦ (𝐹‘𝑚)) ∖ {∅})))
102	40, 101	mpbird 260	. . 3 ⊢ (𝜑 → (𝐹 ↾ (𝐶 ∖ 𝑍)):(𝐶 ∖ 𝑍)–1-1-onto→(𝐴 ∖ {∅}))
103		fvres 6677	. . . . 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 2793	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → ((𝐹 ↾ (𝐶 ∖ 𝑍))‘𝑛) = 𝐺)
109	1, 25, 26, 28, 102, 108, 10	sge0f1o 43387	. 2 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝐴 ∖ {∅}) ↦ 𝐵)) = (Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷)))
110	106	eqcomd 2764	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 = (𝐹‘𝑛))
111	110, 32	eqeltrd 2852	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 ∈ 𝐴)
112	105, 43, 111	syl2anc 587	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐺 ∈ 𝐴)
113	112	ex 416	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (𝐶 ∖ 𝑍) → 𝐺 ∈ 𝐴))
114	113	imdistani 572	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → (𝜑 ∧ 𝐺 ∈ 𝐴))
115		nfcv 2919	. . . . 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 2839	. . . . . . 7 ⊢ (𝑘 = 𝐺 → (𝑘 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴))
121	120	anbi2d 631	. . . . . 6 ⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ 𝐺 ∈ 𝐴)))
122	26	eleq1d 2836	. . . . . 6 ⊢ (𝑘 = 𝐺 → (𝐵 ∈ (0[,]+∞) ↔ 𝐷 ∈ (0[,]+∞)))
123	121, 122	imbi12d 348	. . . . 5 ⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞))))
124	115, 119, 123, 9	vtoclgf 3483	. . . 4 ⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 ∈ 𝐴) → 𝐷 ∈ (0[,]+∞)))
125	112, 114, 124	sylc 65	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ 𝑍)) → 𝐷 ∈ (0[,]+∞))
126		simpl 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝜑)
127		eldifi 4032	. . . . . 6 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝐶)
128	127	adantl 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝐶)
129	126, 128, 111	syl2anc 587	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐺 ∈ 𝐴)
130		dfin4 4172	. . . . . . . . 9 ⊢ (𝑍 ∩ 𝐶) = (𝑍 ∖ (𝑍 ∖ 𝐶))
131		difss 4037	. . . . . . . . 9 ⊢ (𝑍 ∖ (𝑍 ∖ 𝐶)) ⊆ 𝑍
132	130, 131	eqsstri 3926	. . . . . . . 8 ⊢ (𝑍 ∩ 𝐶) ⊆ 𝑍
133		inss2 4134	. . . . . . . . . 10 ⊢ (𝐶 ∩ 𝑍) ⊆ 𝑍
134		id 22	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)))
135		dfin4 4172	. . . . . . . . . . . 12 ⊢ (𝐶 ∩ 𝑍) = (𝐶 ∖ (𝐶 ∖ 𝑍))
136	135	eqcomi 2767	. . . . . . . . . . 11 ⊢ (𝐶 ∖ (𝐶 ∖ 𝑍)) = (𝐶 ∩ 𝑍)
137	134, 136	eleqtrdi 2862	. . . . . . . . . 10 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝐶 ∩ 𝑍))
138	133, 137	sseldi 3890	. . . . . . . . 9 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍)
139	138, 127	elind 4099	. . . . . . . 8 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ (𝑍 ∩ 𝐶))
140	132, 139	sseldi 3890	. . . . . . 7 ⊢ (𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍)) → 𝑛 ∈ 𝑍)
141	140	adantl 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝑛 ∈ 𝑍)
142	77	eqcomd 2764	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∅ = (𝐹‘𝑛))
143		simpl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝜑)
144	74	simpld 498	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝐶)
145	143, 144, 106	syl2anc 587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = 𝐺)
146	142, 145	eqtr2d 2794	. . . . . 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 2762	. . . . . . 7 ⊢ (𝑘 = 𝐺 → (𝑘 = ∅ ↔ 𝐺 = ∅))
154	153	anbi2d 631	. . . . . 6 ⊢ (𝑘 = 𝐺 → ((𝜑 ∧ 𝑘 = ∅) ↔ (𝜑 ∧ 𝐺 = ∅)))
155	26	eqeq1d 2760	. . . . . 6 ⊢ (𝑘 = 𝐺 → (𝐵 = 0 ↔ 𝐷 = 0))
156	154, 155	imbi12d 348	. . . . 5 ⊢ (𝑘 = 𝐺 → (((𝜑 ∧ 𝑘 = ∅) → 𝐵 = 0) ↔ ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0)))
157	115, 152, 156, 21	vtoclgf 3483	. . . 4 ⊢ (𝐺 ∈ 𝐴 → ((𝜑 ∧ 𝐺 = ∅) → 𝐷 = 0))
158	129, 148, 157	sylc 65	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐶 ∖ (𝐶 ∖ 𝑍))) → 𝐷 = 0)
159	25, 2, 42, 125, 158	sge0ss 43417	. 2 ⊢ (𝜑 → (Σ^‘(𝑛 ∈ (𝐶 ∖ 𝑍) ↦ 𝐷)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
160	24, 109, 159	3eqtrd 2797	1 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538  Ⅎwnf 1785   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070  {crab 3074  Vcvv 3409   ∖ cdif 3855   ∩ cin 3857   ⊆ wss 3858  ∅c0 4225  {csn 4522  Disj wdisj 4997   ↦ cmpt 5112  ^◡ccnv 5523  ran crn 5525   ↾ cres 5526   “ cima 5527   Fn wfn 6330  ⟶wf 6331  –onto→wfo 6333  –1-1-onto→wf1o 6334  ‘cfv 6335  (class class class)co 7150  0cc0 10575  +∞cpnf 10710  [,]cicc 12782  Σ^{^}csumge0 43367

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 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-inf2 9137  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-pre-sup 10653

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 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-disj 4998  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-se 5484  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-isom 6344  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-1st 7693  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-er 8299  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-sup 8939  df-oi 9007  df-card 9401  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-div 11336  df-nn 11675  df-2 11737  df-3 11738  df-n0 11935  df-z 12021  df-uz 12283  df-rp 12431  df-xadd 12549  df-ico 12785  df-icc 12786  df-fz 12940  df-fzo 13083  df-seq 13419  df-exp 13480  df-hash 13741  df-cj 14506  df-re 14507  df-im 14508  df-sqrt 14642  df-abs 14643  df-clim 14893  df-sum 15091  df-sumge0 43368

This theorem is referenced by:  sge0fodjrn  43422