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