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