Theorem sge0fodjrnlem

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)

	Ref	Expression
Hypotheses	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	sge0fodjrnlem	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sge0fodjrnlem.k	⊢ Ⅎ 𝑘 𝜑
2		sge0fodjrnlem.n	⊢ Ⅎ 𝑛 𝜑
3		sge0fodjrnlem.bd	⊢ ( 𝑘 = 𝐺 → 𝐵 = 𝐷 )
4		sge0fodjrnlem.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5		sge0fodjrnlem.f	⊢ ( 𝜑 → 𝐹 : 𝐶 –onto→ 𝐴 )
6		sge0fodjrnlem.dj	⊢ ( 𝜑 → Disj 𝑛 ∈ 𝐶 ( 𝐹 ‘ 𝑛 ) )
7		sge0fodjrnlem.fng	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 )
8		sge0fodjrnlem.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
9		sge0fodjrnlem.b0	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → 𝐵 = 0 )
10		sge0fodjrnlem.z	⊢ 𝑍 = ( ◡ 𝐹 “ { ∅ } )
11		fornex	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐹 : 𝐶 –onto→ 𝐴 → 𝐴 ∈ V ) )
12	4 5 11	sylc	⊢ ( 𝜑 → 𝐴 ∈ V )
13		difssd	⊢ ( 𝜑 → ( 𝐴 ∖ { ∅ } ) ⊆ 𝐴 )
14		simpl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { ∅ } ) ) → 𝜑 )
15	13	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { ∅ } ) ) → 𝑘 ∈ 𝐴 )
16	14 15 8	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ { ∅ } ) ) → 𝐵 ∈ ( 0 [,] +∞ ) )
17		simpl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) ) → 𝜑 )
18		dfin4	⊢ ( 𝐴 ∩ { ∅ } ) = ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) )
19	18	eqcomi	⊢ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) = ( 𝐴 ∩ { ∅ } )
20		inss2	⊢ ( 𝐴 ∩ { ∅ } ) ⊆ { ∅ }
21	19 20	eqsstri	⊢ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) ⊆ { ∅ }
22		id	⊢ ( 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) → 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) )
23	21 22	sseldi	⊢ ( 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) → 𝑘 ∈ { ∅ } )
24		elsni	⊢ ( 𝑘 ∈ { ∅ } → 𝑘 = ∅ )
25	23 24	syl	⊢ ( 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) → 𝑘 = ∅ )
26	25	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) ) → 𝑘 = ∅ )
27	17 26 9	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { ∅ } ) ) ) → 𝐵 = 0 )
28	1 12 13 16 27	sge0ss	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∖ { ∅ } ) ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
29	28	eqcomd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∖ { ∅ } ) ↦ 𝐵 ) ) )
30		difexg	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐶 ∖ 𝑍 ) ∈ V )
31	4 30	syl	⊢ ( 𝜑 → ( 𝐶 ∖ 𝑍 ) ∈ V )
32		eqid	⊢ ( 𝑛 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑛 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑛 ) )
33		fof	⊢ ( 𝐹 : 𝐶 –onto→ 𝐴 → 𝐹 : 𝐶 ⟶ 𝐴 )
34	5 33	syl	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐴 )
35	34	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 )
36		fveq2	⊢ ( 𝑚 = 𝑛 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) )
37	36	neeq1d	⊢ ( 𝑚 = 𝑛 → ( ( 𝐹 ‘ 𝑚 ) ≠ ∅ ↔ ( 𝐹 ‘ 𝑛 ) ≠ ∅ ) )
38	37	cbvrabv	⊢ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } = { 𝑛 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑛 ) ≠ ∅ }
39	36	cbvmptv	⊢ ( 𝑚 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑚 ) ) = ( 𝑛 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑛 ) )
40	39	rneqi	⊢ ran ( 𝑚 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑚 ) ) = ran ( 𝑛 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑛 ) )
41	40	difeq1i	⊢ ( ran ( 𝑚 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑚 ) ) ∖ { ∅ } ) = ( ran ( 𝑛 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑛 ) ) ∖ { ∅ } )
42	2 32 35 6 38 41	disjf1o	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑛 ) ) ↾ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ) : { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } –1-1-onto→ ( ran ( 𝑚 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑚 ) ) ∖ { ∅ } ) )
43	34	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑛 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑛 ) ) )
44		difssd	⊢ ( 𝜑 → ( 𝐶 ∖ 𝑍 ) ⊆ 𝐶 )
45	44	sselda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) → 𝑛 ∈ 𝐶 )
46		eldifi	⊢ ( 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) → 𝑛 ∈ 𝐶 )
47	46	adantr	⊢ ( ( 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ∧ ( 𝐹 ‘ 𝑛 ) = ∅ ) → 𝑛 ∈ 𝐶 )
48		id	⊢ ( ( 𝐹 ‘ 𝑛 ) = ∅ → ( 𝐹 ‘ 𝑛 ) = ∅ )
49		fvex	⊢ ( 𝐹 ‘ 𝑛 ) ∈ V
50	49	elsn	⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ { ∅ } ↔ ( 𝐹 ‘ 𝑛 ) = ∅ )
51	48 50	sylibr	⊢ ( ( 𝐹 ‘ 𝑛 ) = ∅ → ( 𝐹 ‘ 𝑛 ) ∈ { ∅ } )
52	51	adantl	⊢ ( ( 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ∧ ( 𝐹 ‘ 𝑛 ) = ∅ ) → ( 𝐹 ‘ 𝑛 ) ∈ { ∅ } )
53	47 52	jca	⊢ ( ( 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ∧ ( 𝐹 ‘ 𝑛 ) = ∅ ) → ( 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) ∈ { ∅ } ) )
54	53	adantll	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = ∅ ) → ( 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) ∈ { ∅ } ) )
55	34	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐶 )
56		elpreima	⊢ ( 𝐹 Fn 𝐶 → ( 𝑛 ∈ ( ◡ 𝐹 “ { ∅ } ) ↔ ( 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) ∈ { ∅ } ) ) )
57	55 56	syl	⊢ ( 𝜑 → ( 𝑛 ∈ ( ◡ 𝐹 “ { ∅ } ) ↔ ( 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) ∈ { ∅ } ) ) )
58	57	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = ∅ ) → ( 𝑛 ∈ ( ◡ 𝐹 “ { ∅ } ) ↔ ( 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) ∈ { ∅ } ) ) )
59	54 58	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = ∅ ) → 𝑛 ∈ ( ◡ 𝐹 “ { ∅ } ) )
60	59 10	eleqtrrdi	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = ∅ ) → 𝑛 ∈ 𝑍 )
61		eldifn	⊢ ( 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) → ¬ 𝑛 ∈ 𝑍 )
62	61	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = ∅ ) → ¬ 𝑛 ∈ 𝑍 )
63	60 62	pm2.65da	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) → ¬ ( 𝐹 ‘ 𝑛 ) = ∅ )
64	63	neqned	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) → ( 𝐹 ‘ 𝑛 ) ≠ ∅ )
65	45 64	jca	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) → ( 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) ≠ ∅ ) )
66	37	elrab	⊢ ( 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ↔ ( 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) ≠ ∅ ) )
67	65 66	sylibr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) → 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } )
68	67	ex	⊢ ( 𝜑 → ( 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) → 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ) )
69	66	simplbi	⊢ ( 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } → 𝑛 ∈ 𝐶 )
70	69	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ) → 𝑛 ∈ 𝐶 )
71	10	eleq2i	⊢ ( 𝑛 ∈ 𝑍 ↔ 𝑛 ∈ ( ◡ 𝐹 “ { ∅ } ) )
72	71	biimpi	⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ◡ 𝐹 “ { ∅ } ) )
73	72	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ ( ◡ 𝐹 “ { ∅ } ) )
74	57	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑛 ∈ ( ◡ 𝐹 “ { ∅ } ) ↔ ( 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) ∈ { ∅ } ) ) )
75	73 74	mpbid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) ∈ { ∅ } ) )
76	75	simprd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ { ∅ } )
77		elsni	⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ { ∅ } → ( 𝐹 ‘ 𝑛 ) = ∅ )
78	76 77	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) = ∅ )
79	78	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) = ∅ )
80	66	simprbi	⊢ ( 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } → ( 𝐹 ‘ 𝑛 ) ≠ ∅ )
81	80	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ≠ ∅ )
82	81	neneqd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ) ∧ 𝑛 ∈ 𝑍 ) → ¬ ( 𝐹 ‘ 𝑛 ) = ∅ )
83	79 82	pm2.65da	⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ) → ¬ 𝑛 ∈ 𝑍 )
84	70 83	eldifd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ) → 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) )
85	84	ex	⊢ ( 𝜑 → ( 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } → 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) )
86	2 85	ralrimi	⊢ ( 𝜑 → ∀ 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) )
87		dfss3	⊢ ( { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ⊆ ( 𝐶 ∖ 𝑍 ) ↔ ∀ 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) )
88	86 87	sylibr	⊢ ( 𝜑 → { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ⊆ ( 𝐶 ∖ 𝑍 ) )
89	88	sseld	⊢ ( 𝜑 → ( 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } → 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) )
90	68 89	impbid	⊢ ( 𝜑 → ( 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ↔ 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ) )
91	2 90	alrimi	⊢ ( 𝜑 → ∀ 𝑛 ( 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ↔ 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ) )
92		dfcleq	⊢ ( ( 𝐶 ∖ 𝑍 ) = { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ↔ ∀ 𝑛 ( 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ↔ 𝑛 ∈ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ) )
93	91 92	sylibr	⊢ ( 𝜑 → ( 𝐶 ∖ 𝑍 ) = { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } )
94	43 93	reseq12d	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐶 ∖ 𝑍 ) ) = ( ( 𝑛 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑛 ) ) ↾ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ) )
95	43 39	eqtr4di	⊢ ( 𝜑 → 𝐹 = ( 𝑚 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑚 ) ) )
96	95	eqcomd	⊢ ( 𝜑 → ( 𝑚 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑚 ) ) = 𝐹 )
97	96	rneqd	⊢ ( 𝜑 → ran ( 𝑚 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑚 ) ) = ran 𝐹 )
98		forn	⊢ ( 𝐹 : 𝐶 –onto→ 𝐴 → ran 𝐹 = 𝐴 )
99	5 98	syl	⊢ ( 𝜑 → ran 𝐹 = 𝐴 )
100	97 99	eqtr2d	⊢ ( 𝜑 → 𝐴 = ran ( 𝑚 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑚 ) ) )
101	100	difeq1d	⊢ ( 𝜑 → ( 𝐴 ∖ { ∅ } ) = ( ran ( 𝑚 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑚 ) ) ∖ { ∅ } ) )
102	94 93 101	f1oeq123d	⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐶 ∖ 𝑍 ) ) : ( 𝐶 ∖ 𝑍 ) –1-1-onto→ ( 𝐴 ∖ { ∅ } ) ↔ ( ( 𝑛 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑛 ) ) ↾ { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } ) : { 𝑚 ∈ 𝐶 ∣ ( 𝐹 ‘ 𝑚 ) ≠ ∅ } –1-1-onto→ ( ran ( 𝑚 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑚 ) ) ∖ { ∅ } ) ) )
103	42 102	mpbird	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐶 ∖ 𝑍 ) ) : ( 𝐶 ∖ 𝑍 ) –1-1-onto→ ( 𝐴 ∖ { ∅ } ) )
104		fvres	⊢ ( 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) → ( ( 𝐹 ↾ ( 𝐶 ∖ 𝑍 ) ) ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
105	104	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) → ( ( 𝐹 ↾ ( 𝐶 ∖ 𝑍 ) ) ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
106		simpl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) → 𝜑 )
107	106 45 7	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 )
108	105 107	eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) → ( ( 𝐹 ↾ ( 𝐶 ∖ 𝑍 ) ) ‘ 𝑛 ) = 𝐺 )
109	1 2 3 31 103 108 16	sge0f1o	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝐴 ∖ { ∅ } ) ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ↦ 𝐷 ) ) )
110	7	eqcomd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → 𝐺 = ( 𝐹 ‘ 𝑛 ) )
111	110 35	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → 𝐺 ∈ 𝐴 )
112	106 45 111	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) → 𝐺 ∈ 𝐴 )
113	112	ex	⊢ ( 𝜑 → ( 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) → 𝐺 ∈ 𝐴 ) )
114	113	imdistani	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) → ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) )
115		nfcv	⊢ Ⅎ 𝑘 𝐺
116		nfv	⊢ Ⅎ 𝑘 𝐺 ∈ 𝐴
117	1 116	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝐺 ∈ 𝐴 )
118		nfv	⊢ Ⅎ 𝑘 𝐷 ∈ ( 0 [,] +∞ )
119	117 118	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
120		eleq1	⊢ ( 𝑘 = 𝐺 → ( 𝑘 ∈ 𝐴 ↔ 𝐺 ∈ 𝐴 ) )
121	120	anbi2d	⊢ ( 𝑘 = 𝐺 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) ) )
122	3	eleq1d	⊢ ( 𝑘 = 𝐺 → ( 𝐵 ∈ ( 0 [,] +∞ ) ↔ 𝐷 ∈ ( 0 [,] +∞ ) ) )
123	121 122	imbi12d	⊢ ( 𝑘 = 𝐺 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) ) ↔ ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) → 𝐷 ∈ ( 0 [,] +∞ ) ) ) )
124	115 119 123 8	vtoclgf	⊢ ( 𝐺 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐺 ∈ 𝐴 ) → 𝐷 ∈ ( 0 [,] +∞ ) ) )
125	112 114 124	sylc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ) → 𝐷 ∈ ( 0 [,] +∞ ) )
126		simpl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) ) → 𝜑 )
127		eldifi	⊢ ( 𝑛 ∈ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) → 𝑛 ∈ 𝐶 )
128	127	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) ) → 𝑛 ∈ 𝐶 )
129	126 128 111	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) ) → 𝐺 ∈ 𝐴 )
130		dfin4	⊢ ( 𝑍 ∩ 𝐶 ) = ( 𝑍 ∖ ( 𝑍 ∖ 𝐶 ) )
131		difss	⊢ ( 𝑍 ∖ ( 𝑍 ∖ 𝐶 ) ) ⊆ 𝑍
132	130 131	eqsstri	⊢ ( 𝑍 ∩ 𝐶 ) ⊆ 𝑍
133		inss2	⊢ ( 𝐶 ∩ 𝑍 ) ⊆ 𝑍
134		id	⊢ ( 𝑛 ∈ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) → 𝑛 ∈ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) )
135		dfin4	⊢ ( 𝐶 ∩ 𝑍 ) = ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) )
136	135	eqcomi	⊢ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) = ( 𝐶 ∩ 𝑍 )
137	134 136	eleqtrdi	⊢ ( 𝑛 ∈ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) → 𝑛 ∈ ( 𝐶 ∩ 𝑍 ) )
138	133 137	sseldi	⊢ ( 𝑛 ∈ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) → 𝑛 ∈ 𝑍 )
139	138 127	elind	⊢ ( 𝑛 ∈ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) → 𝑛 ∈ ( 𝑍 ∩ 𝐶 ) )
140	132 139	sseldi	⊢ ( 𝑛 ∈ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) → 𝑛 ∈ 𝑍 )
141	140	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) ) → 𝑛 ∈ 𝑍 )
142	78	eqcomd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∅ = ( 𝐹 ‘ 𝑛 ) )
143		simpl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝜑 )
144	75	simpld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝐶 )
145	143 144 7	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 )
146	142 145	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝐺 = ∅ )
147	126 141 146	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) ) → 𝐺 = ∅ )
148	126 147	jca	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) ) → ( 𝜑 ∧ 𝐺 = ∅ ) )
149		nfv	⊢ Ⅎ 𝑘 𝐺 = ∅
150	1 149	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝐺 = ∅ )
151		nfv	⊢ Ⅎ 𝑘 𝐷 = 0
152	150 151	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐷 = 0 )
153		eqeq1	⊢ ( 𝑘 = 𝐺 → ( 𝑘 = ∅ ↔ 𝐺 = ∅ ) )
154	153	anbi2d	⊢ ( 𝑘 = 𝐺 → ( ( 𝜑 ∧ 𝑘 = ∅ ) ↔ ( 𝜑 ∧ 𝐺 = ∅ ) ) )
155	3	eqeq1d	⊢ ( 𝑘 = 𝐺 → ( 𝐵 = 0 ↔ 𝐷 = 0 ) )
156	154 155	imbi12d	⊢ ( 𝑘 = 𝐺 → ( ( ( 𝜑 ∧ 𝑘 = ∅ ) → 𝐵 = 0 ) ↔ ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐷 = 0 ) ) )
157	115 152 156 9	vtoclgf	⊢ ( 𝐺 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐷 = 0 ) )
158	129 148 157	sylc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐶 ∖ ( 𝐶 ∖ 𝑍 ) ) ) → 𝐷 = 0 )
159	2 4 44 125 158	sge0ss	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ( 𝐶 ∖ 𝑍 ) ↦ 𝐷 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) )
160	29 109 159	3eqtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) )