sge0f1o - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sge0f1o		Structured version Visualization version GIF version

Theorem sge0f1o 41113

Description: Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

**Hypotheses**
Ref	Expression
sge0f1o.1	⊢ Ⅎ𝑘𝜑
sge0f1o.2	⊢ Ⅎ𝑛𝜑
sge0f1o.3	⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)
sge0f1o.4	⊢ (𝜑 → 𝐶 ∈ 𝑉)
sge0f1o.5	⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)
sge0f1o.6	⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)
sge0f1o.7	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))

**Assertion**
Ref	Expression
sge0f1o	⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))

Distinct variable groups: 𝐴,𝑘,𝑛 𝐵,𝑛 𝐶,𝑘,𝑛 𝐷,𝑘 𝑘,𝐹,𝑛 𝑘,𝐺 Allowed substitution hints: 𝜑(𝑘,𝑛) 𝐵(𝑘) 𝐷(𝑛) 𝐺(𝑛) 𝑉(𝑘,𝑛)

Proof of Theorem sge0f1o Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sge0f1o.4	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
2		sge0f1o.5	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)
3		f1ofo 6286	. . . . . . 7 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–onto→𝐴)
4	2, 3	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐶–onto→𝐴)
5		fornex 7285	. . . . . 6 ⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V))
6	1, 4, 5	sylc 65	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ V)
7	6	adantr 466	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V)
8		sge0f1o.1	. . . . . 6 ⊢ Ⅎ𝑘𝜑
9		sge0f1o.7	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
10		eqid 2771	. . . . . 6 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵)
11	8, 9, 10	fmptdf 6531	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞))
12	11	adantr 466	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞))
13		pnfex 10298	. . . . . . . 8 ⊢ +∞ ∈ V
14		eqid 2771	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝐶 ↦ 𝐷) = (𝑛 ∈ 𝐶 ↦ 𝐷)
15	14	elrnmpt 5509	. . . . . . . 8 ⊢ (+∞ ∈ V → (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷))
16	13, 15	ax-mp 5	. . . . . . 7 ⊢ (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷)
17	16	biimpi 206	. . . . . 6 ⊢ (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) → ∃𝑛 ∈ 𝐶 +∞ = 𝐷)
18	17	adantl 467	. . . . 5 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ∃𝑛 ∈ 𝐶 +∞ = 𝐷)
19		sge0f1o.2	. . . . . . 7 ⊢ Ⅎ𝑛𝜑
20		nfv 1995	. . . . . . 7 ⊢ Ⅎ𝑛+∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)
21		simp3 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = 𝐷)
22		f1of 6279	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴)
23	2, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:𝐶⟶𝐴)
24	23	ffvelrnda 6504	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴)
25		sge0f1o.6	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)
26		nfcv 2913	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝐹‘𝑛)
27		nfv 1995	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝐹‘𝑛) = 𝐺
28	26	nfcsb1 3697	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵
29		nfcv 2913	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝐷
30	28, 29	nfeq 2925	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷
31	27, 30	nfim 1977	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
32		eqeq1 2775	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 = 𝐺 ↔ (𝐹‘𝑛) = 𝐺))
33		csbeq1a 3691	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
34	33	eqeq1d 2773	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 = 𝐷 ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷))
35	32, 34	imbi12d 333	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → ((𝑘 = 𝐺 → 𝐵 = 𝐷) ↔ ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)))
36		sge0f1o.3	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)
37	26, 31, 35, 36	vtoclgf 3415	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷))
38	24, 25, 37	sylc 65	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
39	38	eqcomd 2777	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
40	39	3adant3 1126	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
41	21, 40	eqtrd 2805	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
42		simpl 468	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝜑)
43	42, 24	jca 501	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴))
44		nfv 1995	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝐹‘𝑛) ∈ 𝐴
45	8, 44	nfan 1980	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴)
46	28	nfel1 2928	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)
47	45, 46	nfim 1977	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))
48		eleq1 2838	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 ∈ 𝐴 ↔ (𝐹‘𝑛) ∈ 𝐴))
49	48	anbi2d 614	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴)))
50	33	eleq1d 2835	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 ∈ (0[,]+∞) ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)))
51	49, 50	imbi12d 333	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐹‘𝑛) → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))))
52	26, 47, 51, 9	vtoclgf 3415	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)))
53	24, 43, 52	sylc 65	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))
54	28, 10, 33	elrnmpt1sf 39895	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑛) ∈ 𝐴 ∧ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
55	24, 53, 54	syl2anc 573	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
56	55	3adant3 1126	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
57	41, 56	eqeltrd 2850	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
58	57	3exp 1112	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝐶 → (+∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))))
59	19, 20, 58	rexlimd 3174	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))
60	59	adantr 466	. . . . 5 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (∃𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))
61	18, 60	mpd 15	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
62	7, 12, 61	sge0pnfval 41104	. . 3 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = +∞)
63	1	adantr 466	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉)
64	39, 53	eqeltrd 2850	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,]+∞))
65	19, 64, 14	fmptdf 6531	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞))
66	65	adantr 466	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞))
67		simpr 471	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
68	63, 66, 67	sge0pnfval 41104	. . 3 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = +∞)
69	62, 68	eqtr4d 2808	. 2 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
70		sumex 14625	. . . . . . 7 ⊢ Σ𝑘 ∈ 𝑦 𝐵 ∈ V
71	70	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 ∈ V)
72		cnvimass 5625	. . . . . . . . . . . . 13 ⊢ (^◡𝐹 “ 𝑦) ⊆ dom 𝐹
73	72	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ⊆ dom 𝐹)
74	23	fdmd 6193	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝐹 = 𝐶)
75	73, 74	sseqtrd 3790	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ⊆ 𝐶)
76		fex 6635	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐶⟶𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐹 ∈ V)
77	23, 1, 76	syl2anc 573	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ V)
78		cnvexg 7262	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ V → ^◡𝐹 ∈ V)
79	77, 78	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ^◡𝐹 ∈ V)
80		imaexg 7253	. . . . . . . . . . . . 13 ⊢ (^◡𝐹 ∈ V → (^◡𝐹 “ 𝑦) ∈ V)
81	79, 80	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ∈ V)
82		elpwg 4306	. . . . . . . . . . . 12 ⊢ ((^◡𝐹 “ 𝑦) ∈ V → ((^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (^◡𝐹 “ 𝑦) ⊆ 𝐶))
83	81, 82	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (^◡𝐹 “ 𝑦) ⊆ 𝐶))
84	75, 83	mpbird 247	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
85	84	adantr 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
86		f1ocnv 6291	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → ^◡𝐹:𝐴–1-1-onto→𝐶)
87	2, 86	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ^◡𝐹:𝐴–1-1-onto→𝐶)
88		f1ofun 6281	. . . . . . . . . . . 12 ⊢ (^◡𝐹:𝐴–1-1-onto→𝐶 → Fun ^◡𝐹)
89	87, 88	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → Fun ^◡𝐹)
90	89	adantr 466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Fun ^◡𝐹)
91		elinel2 3951	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
92	91	adantl 467	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin)
93		imafi 8418	. . . . . . . . . 10 ⊢ ((Fun ^◡𝐹 ∧ 𝑦 ∈ Fin) → (^◡𝐹 “ 𝑦) ∈ Fin)
94	90, 92, 93	syl2anc 573	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ Fin)
95	85, 94	elind 3949	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
96	95	adantlr 694	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
97		nfv 1995	. . . . . . . . . 10 ⊢ Ⅎ𝑘 ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
98	8, 97	nfan 1980	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
99		nfv 1995	. . . . . . . . 9 ⊢ Ⅎ𝑘 𝑦 ∈ (𝒫 𝐴 ∩ Fin)
100	98, 99	nfan 1980	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
101		nfcv 2913	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛+∞
102		nfmpt1 4882	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(𝑛 ∈ 𝐶 ↦ 𝐷)
103	102	nfrn 5505	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛ran (𝑛 ∈ 𝐶 ↦ 𝐷)
104	101, 103	nfel 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑛+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
105	104	nfn 1935	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
106	19, 105	nfan 1980	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
107		nfv 1995	. . . . . . . . 9 ⊢ Ⅎ𝑛 𝑦 ∈ (𝒫 𝐴 ∩ Fin)
108	106, 107	nfan 1980	. . . . . . . 8 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
109	94	adantlr 694	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ Fin)
110		f1of1 6278	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–1-1→𝐴)
111	2, 110	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐶–1-1→𝐴)
112	111	adantr 466	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐶–1-1→𝐴)
113	83	adantr 466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (^◡𝐹 “ 𝑦) ⊆ 𝐶))
114	85, 113	mpbid 222	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ⊆ 𝐶)
115		f1ores 6293	. . . . . . . . . . 11 ⊢ ((𝐹:𝐶–1-1→𝐴 ∧ (^◡𝐹 “ 𝑦) ⊆ 𝐶) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)))
116	112, 114, 115	syl2anc 573	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)))
117	4	adantr 466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐶–onto→𝐴)
118		elpwinss 39737	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴)
119	118	adantl 467	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ⊆ 𝐴)
120		foimacnv 6296	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝐹 “ (^◡𝐹 “ 𝑦)) = 𝑦)
121	117, 119, 120	syl2anc 573	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ (^◡𝐹 “ 𝑦)) = 𝑦)
122	121	f1oeq3d 6276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)) ↔ (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦))
123	116, 122	mpbid 222	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦)
124	123	adantlr 694	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦)
125	81	ad2antrr 705	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → (^◡𝐹 “ 𝑦) ∈ V)
126		simpll 750	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → 𝜑)
127	95	adantr 466	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
128		simpr 471	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → 𝑛 ∈ (^◡𝐹 “ 𝑦))
129	126, 127, 128	jca31 504	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)))
130		eleq1 2838	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↔ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)))
131	130	anbi2d 614	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ (𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))))
132		eleq2 2839	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑛 ∈ 𝑥 ↔ 𝑛 ∈ (^◡𝐹 “ 𝑦)))
133	131, 132	anbi12d 616	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) ↔ ((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦))))
134		reseq2 5528	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝐹 ↾ 𝑥) = (𝐹 ↾ (^◡𝐹 “ 𝑦)))
135	134	fveq1d 6335	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((𝐹 ↾ 𝑥)‘𝑛) = ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛))
136	135	eqeq1d 2773	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝐹 ↾ 𝑥)‘𝑛) = 𝐺 ↔ ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺))
137	133, 136	imbi12d 333	. . . . . . . . . . 11 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺) ↔ (((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)))
138		fvres 6350	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑥 → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛))
139	138	adantl 467	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛))
140		simpll 750	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝜑)
141		elpwinss 39737	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ⊆ 𝐶)
142	141	adantl 467	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ⊆ 𝐶)
143	142	sselda 3752	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝑛 ∈ 𝐶)
144	140, 143, 25	syl2anc 573	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → (𝐹‘𝑛) = 𝐺)
145	139, 144	eqtrd 2805	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺)
146	137, 145	vtoclg 3417	. . . . . . . . . 10 ⊢ ((^◡𝐹 “ 𝑦) ∈ V → (((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺))
147	125, 129, 146	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)
148	147	adantllr 698	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)
149	81	ad3antrrr 709	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ V)
150		simpll 750	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)))
151	84	ad3antrrr 709	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
152	109	adantr 466	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ Fin)
153	151, 152	elind 3949	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
154		simpr 471	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑦)
155	121	eqcomd 2777	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 = (𝐹 “ (^◡𝐹 “ 𝑦)))
156	155	adantr 466	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑦 = (𝐹 “ (^◡𝐹 “ 𝑦)))
157	154, 156	eleqtrd 2852	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))
158	157	adantllr 698	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))
159	150, 153, 158	jca31 504	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))))
160	130	anbi2d 614	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))))
161		imaeq2 5602	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝐹 “ 𝑥) = (𝐹 “ (^◡𝐹 “ 𝑦)))
162	161	eleq2d 2836	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑘 ∈ (𝐹 “ 𝑥) ↔ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))))
163	160, 162	anbi12d 616	. . . . . . . . . . 11 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) ↔ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))))
164	163	imbi1d 330	. . . . . . . . . 10 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ) ↔ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ)))
165		rge0ssre 12486	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ ℝ
166		ax-resscn 10198	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
167	165, 166	sstri 3761	. . . . . . . . . . . 12 ⊢ (0[,)+∞) ⊆ ℂ
168		simplll 758	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝜑)
169		simpllr 760	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
170		fimass 6222	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐶⟶𝐴 → (𝐹 “ 𝑥) ⊆ 𝐴)
171	23, 170	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 “ 𝑥) ⊆ 𝐴)
172	171	ad2antrr 705	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → (𝐹 “ 𝑥) ⊆ 𝐴)
173		simpr 471	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ (𝐹 “ 𝑥))
174	172, 173	sseldd 3753	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴)
175	174	adantllr 698	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴)
176		foelrni 6388	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
177	4, 176	sylan 569	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
178	177	adantlr 694	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
179		nfv 1995	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛 𝑘 ∈ 𝐴
180	106, 179	nfan 1980	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴)
181		nfv 1995	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛 𝐵 ∈ (0[,)+∞)
182		csbid 3690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ⦋𝑘 / 𝑘⦌𝐵 = 𝐵
183	182	eqcomi 2780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 = ⦋𝑘 / 𝑘⦌𝐵
184	183	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = ⦋𝑘 / 𝑘⦌𝐵)
185		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑛) = 𝑘 → (𝐹‘𝑛) = 𝑘)
186	185	eqcomd 2777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑛) = 𝑘 → 𝑘 = (𝐹‘𝑛))
187	186	csbeq1d 3689	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑛) = 𝑘 → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
188	187	3ad2ant3 1129	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
189	38	idi 2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
190	189	3adant3 1126	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
191	184, 188, 190	3eqtrd 2809	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷)
192	191	3adant1r 1187	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷)
193		0xr 10291	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ∈ ℝ^*
194	193	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 0 ∈ ℝ^*)
195		pnfxr 10297	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ +∞ ∈ ℝ^*
196	195	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ℝ^*)
197	64	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈ (0[,]+∞))
198		simpr 471	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬ 𝐷 ∈ (0[,)+∞))
199	194, 196, 197, 198	eliccnelico 40271	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 = +∞)
200	199	eqcomd 2777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ = 𝐷)
201		simpr 471	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝑛 ∈ 𝐶)
202	64	idi 2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,]+∞))
203	14	elrnmpt1 5511	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ 𝐶 ∧ 𝐷 ∈ (0[,]+∞)) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
204	201, 202, 203	syl2anc 573	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
205	204	adantr 466	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
206	200, 205	eqeltrd 2850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
207	206	adantllr 698	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
208		simpllr 760	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
209	207, 208	condan 819	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,)+∞))
210	209	3adant3 1126	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐷 ∈ (0[,)+∞))
211	192, 210	eqeltrd 2850	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 ∈ (0[,)+∞))
212	211	3exp 1112	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞))))
213	212	adantr 466	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞))))
214	180, 181, 213	rexlimd 3174	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞)))
215	178, 214	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))
216	168, 169, 175, 215	syl21anc 1475	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ (0[,)+∞))
217	167, 216	sseldi 3750	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ)
218	217	idi 2	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ)
219	164, 218	vtoclg 3417	. . . . . . . . 9 ⊢ ((^◡𝐹 “ 𝑦) ∈ V → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ))
220	149, 159, 219	sylc 65	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℂ)
221	100, 108, 36, 109, 124, 148, 220	fsumf1of 40321	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷)
222		sumeq1 14626	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷)
223	222	eqeq2d 2781	. . . . . . . 8 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷 ↔ Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷))
224	223	rspcev 3460	. . . . . . 7 ⊢ (((^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin) ∧ Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
225	96, 221, 224	syl2anc 573	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
226	71, 225	rnmptssrn 39887	. . . . 5 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) ⊆ ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷))
227		sumex 14625	. . . . . . 7 ⊢ Σ𝑛 ∈ 𝑥 𝐷 ∈ V
228	227	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 ∈ V)
229	6, 171	ssexd 4940	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 “ 𝑥) ∈ V)
230		elpwg 4306	. . . . . . . . . . . 12 ⊢ ((𝐹 “ 𝑥) ∈ V → ((𝐹 “ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐹 “ 𝑥) ⊆ 𝐴))
231	229, 230	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹 “ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐹 “ 𝑥) ⊆ 𝐴))
232	171, 231	mpbird 247	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 “ 𝑥) ∈ 𝒫 𝐴)
233	232	adantr 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ 𝒫 𝐴)
234	23	ffund 6188	. . . . . . . . . . 11 ⊢ (𝜑 → Fun 𝐹)
235	234	adantr 466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Fun 𝐹)
236		elinel2 3951	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ∈ Fin)
237	236	adantl 467	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ∈ Fin)
238		imafi 8418	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ Fin) → (𝐹 “ 𝑥) ∈ Fin)
239	235, 237, 238	syl2anc 573	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ Fin)
240	233, 239	elind 3949	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin))
241	240	adantlr 694	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin))
242		nfv 1995	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑥 ∈ (𝒫 𝐶 ∩ Fin)
243	98, 242	nfan 1980	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin))
244		nfv 1995	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝑥 ∈ (𝒫 𝐶 ∩ Fin)
245	106, 244	nfan 1980	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin))
246	236	adantl 467	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ∈ Fin)
247	111	adantr 466	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝐹:𝐶–1-1→𝐴)
248		f1ores 6293	. . . . . . . . . . 11 ⊢ ((𝐹:𝐶–1-1→𝐴 ∧ 𝑥 ⊆ 𝐶) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
249	247, 142, 248	syl2anc 573	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
250	249	adantlr 694	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
251	145	adantllr 698	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺)
252	243, 245, 36, 246, 250, 251, 217	fsumf1of 40321	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
253	252	eqcomd 2777	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵)
254		sumeq1 14626	. . . . . . . . 9 ⊢ (𝑦 = (𝐹 “ 𝑥) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵)
255	254	eqeq2d 2781	. . . . . . . 8 ⊢ (𝑦 = (𝐹 “ 𝑥) → (Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵 ↔ Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵))
256	255	rspcev 3460	. . . . . . 7 ⊢ (((𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵)
257	241, 253, 256	syl2anc 573	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵)
258	228, 257	rnmptssrn 39887	. . . . 5 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷) ⊆ ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵))
259	226, 258	eqssd 3769	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) = ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷))
260	259	supeq1d 8511	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ^, < ) = sup(ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ^, < ))
261	6	adantr 466	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V)
262	98, 261, 215	sge0revalmpt 41109	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ^*, < ))
263	1	adantr 466	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉)
264	106, 263, 209	sge0revalmpt 41109	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = sup(ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ^*, < ))
265	260, 262, 264	3eqtr4d 2815	. 2 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
266	69, 265	pm2.61dan 814	1 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 382 ∧ w3a 1071 = wceq 1631 Ⅎwnf 1856 ∈ wcel 2145 ∃wrex 3062 Vcvv 3351 ⦋csb 3682 ∩ cin 3722 ⊆ wss 3723 𝒫 cpw 4298 ↦ cmpt 4864 ^◡ccnv 5249 dom cdm 5250 ran crn 5251 ↾ cres 5252 “ cima 5253 Fun wfun 6024 ⟶wf 6026 –1-1→wf1 6027 –onto→wfo 6028 –1-1-onto→wf1o 6029 ‘cfv 6030 (class class class)co 6795 Fincfn 8112 supcsup 8505 ℂcc 10139 ℝcr 10140 0cc0 10141 +∞cpnf 10276 ℝ^*cxr 10278 < clt 10279 [,)cico 12381 [,]cicc 12382 Σcsu 14623 Σ^{^}csumge0 41093

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4905 ax-sep 4916 ax-nul 4924 ax-pow 4975 ax-pr 5035 ax-un 7099 ax-inf2 8705 ax-cnex 10197 ax-resscn 10198 ax-1cn 10199 ax-icn 10200 ax-addcl 10201 ax-addrcl 10202 ax-mulcl 10203 ax-mulrcl 10204 ax-mulcom 10205 ax-addass 10206 ax-mulass 10207 ax-distr 10208 ax-i2m1 10209 ax-1ne0 10210 ax-1rid 10211 ax-rnegex 10212 ax-rrecex 10213 ax-cnre 10214 ax-pre-lttri 10215 ax-pre-lttrn 10216 ax-pre-ltadd 10217 ax-pre-mulgt0 10218 ax-pre-sup 10219

This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-fal 1637 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-tp 4322 df-op 4324 df-uni 4576 df-int 4613 df-iun 4657 df-br 4788 df-opab 4848 df-mpt 4865 df-tr 4888 df-id 5158 df-eprel 5163 df-po 5171 df-so 5172 df-fr 5209 df-se 5210 df-we 5211 df-xp 5256 df-rel 5257 df-cnv 5258 df-co 5259 df-dm 5260 df-rn 5261 df-res 5262 df-ima 5263 df-pred 5822 df-ord 5868 df-on 5869 df-lim 5870 df-suc 5871 df-iota 5993 df-fun 6032 df-fn 6033 df-f 6034 df-f1 6035 df-fo 6036 df-f1o 6037 df-fv 6038 df-isom 6039 df-riota 6756 df-ov 6798 df-oprab 6799 df-mpt2 6800 df-om 7216 df-1st 7318 df-2nd 7319 df-wrecs 7562 df-recs 7624 df-rdg 7662 df-1o 7716 df-oadd 7720 df-er 7899 df-en 8113 df-dom 8114 df-sdom 8115 df-fin 8116 df-sup 8507 df-oi 8574 df-card 8968 df-pnf 10281 df-mnf 10282 df-xr 10283 df-ltxr 10284 df-le 10285 df-sub 10473 df-neg 10474 df-div 10890 df-nn 11226 df-2 11284 df-3 11285 df-n0 11499 df-z 11584 df-uz 11893 df-rp 12035 df-ico 12385 df-icc 12386 df-fz 12533 df-fzo 12673 df-seq 13008 df-exp 13067 df-hash 13321 df-cj 14046 df-re 14047 df-im 14048 df-sqrt 14182 df-abs 14183 df-clim 14426 df-sum 14624 df-sumge0 41094

This theorem is referenced by: sge0resrnlem 41134 sge0fodjrnlem 41147 sge0xp 41160 meadjiunlem 41196 isomenndlem 41261 ovnsubaddlem1 41301

W3C validator