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 42657

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 6617	. . . . . . 7 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–onto→𝐴)
4	2, 3	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐶–onto→𝐴)
5		fornex 7651	. . . . . 6 ⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V))
6	1, 4, 5	sylc 65	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ V)
7	6	adantr 483	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V)
8		sge0f1o.1	. . . . . 6 ⊢ Ⅎ𝑘𝜑
9		sge0f1o.7	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
10		eqid 2821	. . . . . 6 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵)
11	8, 9, 10	fmptdf 6876	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞))
12	11	adantr 483	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞))
13		pnfex 10688	. . . . . . . 8 ⊢ +∞ ∈ V
14		eqid 2821	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝐶 ↦ 𝐷) = (𝑛 ∈ 𝐶 ↦ 𝐷)
15	14	elrnmpt 5823	. . . . . . . 8 ⊢ (+∞ ∈ V → (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷))
16	13, 15	ax-mp 5	. . . . . . 7 ⊢ (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷)
17	16	biimpi 218	. . . . . 6 ⊢ (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) → ∃𝑛 ∈ 𝐶 +∞ = 𝐷)
18	17	adantl 484	. . . . 5 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ∃𝑛 ∈ 𝐶 +∞ = 𝐷)
19		sge0f1o.2	. . . . . . 7 ⊢ Ⅎ𝑛𝜑
20		nfv 1911	. . . . . . 7 ⊢ Ⅎ𝑛+∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)
21		simp3 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = 𝐷)
22		f1of 6610	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴)
23	2, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:𝐶⟶𝐴)
24	23	ffvelrnda 6846	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴)
25		sge0f1o.6	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)
26		nfcv 2977	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝐹‘𝑛)
27		nfv 1911	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝐹‘𝑛) = 𝐺
28	26	nfcsb1 3906	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵
29		nfcv 2977	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝐷
30	28, 29	nfeq 2991	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷
31	27, 30	nfim 1893	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
32		eqeq1 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 = 𝐺 ↔ (𝐹‘𝑛) = 𝐺))
33		csbeq1a 3897	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
34	33	eqeq1d 2823	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 = 𝐷 ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷))
35	32, 34	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → ((𝑘 = 𝐺 → 𝐵 = 𝐷) ↔ ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)))
36		sge0f1o.3	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)
37	26, 31, 35, 36	vtoclgf 3566	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷))
38	24, 25, 37	sylc 65	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
39	38	eqcomd 2827	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
40	39	3adant3 1128	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
41	21, 40	eqtrd 2856	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
42		simpl 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝜑)
43	42, 24	jca 514	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴))
44		nfv 1911	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝐹‘𝑛) ∈ 𝐴
45	8, 44	nfan 1896	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴)
46	28	nfel1 2994	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)
47	45, 46	nfim 1893	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))
48		eleq1 2900	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 ∈ 𝐴 ↔ (𝐹‘𝑛) ∈ 𝐴))
49	48	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴)))
50	33	eleq1d 2897	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 ∈ (0[,]+∞) ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)))
51	49, 50	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐹‘𝑛) → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))))
52	26, 47, 51, 9	vtoclgf 3566	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)))
53	24, 43, 52	sylc 65	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))
54	28, 10, 33	elrnmpt1sf 41442	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑛) ∈ 𝐴 ∧ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
55	24, 53, 54	syl2anc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
56	55	3adant3 1128	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
57	41, 56	eqeltrd 2913	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
58	57	3exp 1115	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝐶 → (+∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))))
59	19, 20, 58	rexlimd 3317	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))
60	59	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (∃𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))
61	18, 60	mpd 15	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
62	7, 12, 61	sge0pnfval 42648	. . 3 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = +∞)
63	1	adantr 483	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉)
64	39, 53	eqeltrd 2913	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,]+∞))
65	19, 64, 14	fmptdf 6876	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞))
66	65	adantr 483	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞))
67		simpr 487	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
68	63, 66, 67	sge0pnfval 42648	. . 3 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = +∞)
69	62, 68	eqtr4d 2859	. 2 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
70		sumex 15038	. . . . . . 7 ⊢ Σ𝑘 ∈ 𝑦 𝐵 ∈ V
71	70	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 ∈ V)
72		cnvimass 5944	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ 𝑦) ⊆ dom 𝐹
73	72, 23	fssdm 6525	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ⊆ 𝐶)
74		fex 6983	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐶⟶𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐹 ∈ V)
75	23, 1, 74	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ V)
76		cnvexg 7623	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ V → ^◡𝐹 ∈ V)
77	75, 76	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ^◡𝐹 ∈ V)
78		imaexg 7614	. . . . . . . . . . . . 13 ⊢ (^◡𝐹 ∈ V → (^◡𝐹 “ 𝑦) ∈ V)
79	77, 78	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ∈ V)
80		elpwg 4545	. . . . . . . . . . . 12 ⊢ ((^◡𝐹 “ 𝑦) ∈ V → ((^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (^◡𝐹 “ 𝑦) ⊆ 𝐶))
81	79, 80	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (^◡𝐹 “ 𝑦) ⊆ 𝐶))
82	73, 81	mpbird 259	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
83	82	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
84		f1ocnv 6622	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → ^◡𝐹:𝐴–1-1-onto→𝐶)
85	2, 84	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ^◡𝐹:𝐴–1-1-onto→𝐶)
86		f1ofun 6612	. . . . . . . . . . . 12 ⊢ (^◡𝐹:𝐴–1-1-onto→𝐶 → Fun ^◡𝐹)
87	85, 86	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → Fun ^◡𝐹)
88	87	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Fun ^◡𝐹)
89		elinel2 4173	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
90	89	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin)
91		imafi 8811	. . . . . . . . . 10 ⊢ ((Fun ^◡𝐹 ∧ 𝑦 ∈ Fin) → (^◡𝐹 “ 𝑦) ∈ Fin)
92	88, 90, 91	syl2anc 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ Fin)
93	83, 92	elind 4171	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
94	93	adantlr 713	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
95		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑘 ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
96	8, 95	nfan 1896	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
97		nfv 1911	. . . . . . . . 9 ⊢ Ⅎ𝑘 𝑦 ∈ (𝒫 𝐴 ∩ Fin)
98	96, 97	nfan 1896	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
99		nfcv 2977	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛+∞
100		nfmpt1 5157	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(𝑛 ∈ 𝐶 ↦ 𝐷)
101	100	nfrn 5819	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛ran (𝑛 ∈ 𝐶 ↦ 𝐷)
102	99, 101	nfel 2992	. . . . . . . . . . 11 ⊢ Ⅎ𝑛+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
103	102	nfn 1853	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
104	19, 103	nfan 1896	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
105		nfv 1911	. . . . . . . . 9 ⊢ Ⅎ𝑛 𝑦 ∈ (𝒫 𝐴 ∩ Fin)
106	104, 105	nfan 1896	. . . . . . . 8 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
107	92	adantlr 713	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ Fin)
108		f1of1 6609	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–1-1→𝐴)
109	2, 108	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐶–1-1→𝐴)
110	109	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐶–1-1→𝐴)
111	81	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (^◡𝐹 “ 𝑦) ⊆ 𝐶))
112	83, 111	mpbid 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ⊆ 𝐶)
113		f1ores 6624	. . . . . . . . . . 11 ⊢ ((𝐹:𝐶–1-1→𝐴 ∧ (^◡𝐹 “ 𝑦) ⊆ 𝐶) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)))
114	110, 112, 113	syl2anc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)))
115	4	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐶–onto→𝐴)
116		elpwinss 41304	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴)
117	116	adantl 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ⊆ 𝐴)
118		foimacnv 6627	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝐹 “ (^◡𝐹 “ 𝑦)) = 𝑦)
119	115, 117, 118	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ (^◡𝐹 “ 𝑦)) = 𝑦)
120	119	f1oeq3d 6607	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)) ↔ (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦))
121	114, 120	mpbid 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦)
122	121	adantlr 713	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦)
123	79	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → (^◡𝐹 “ 𝑦) ∈ V)
124		simpll 765	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → 𝜑)
125	93	adantr 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
126		simpr 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → 𝑛 ∈ (^◡𝐹 “ 𝑦))
127	124, 125, 126	jca31 517	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)))
128		eleq1 2900	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↔ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)))
129	128	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ (𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))))
130		eleq2 2901	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑛 ∈ 𝑥 ↔ 𝑛 ∈ (^◡𝐹 “ 𝑦)))
131	129, 130	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) ↔ ((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦))))
132		reseq2 5843	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝐹 ↾ 𝑥) = (𝐹 ↾ (^◡𝐹 “ 𝑦)))
133	132	fveq1d 6667	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((𝐹 ↾ 𝑥)‘𝑛) = ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛))
134	133	eqeq1d 2823	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝐹 ↾ 𝑥)‘𝑛) = 𝐺 ↔ ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺))
135	131, 134	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺) ↔ (((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)))
136		fvres 6684	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑥 → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛))
137	136	adantl 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛))
138		simpll 765	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝜑)
139		elpwinss 41304	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ⊆ 𝐶)
140	139	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ⊆ 𝐶)
141	140	sselda 3967	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝑛 ∈ 𝐶)
142	138, 141, 25	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → (𝐹‘𝑛) = 𝐺)
143	137, 142	eqtrd 2856	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺)
144	135, 143	vtoclg 3568	. . . . . . . . . 10 ⊢ ((^◡𝐹 “ 𝑦) ∈ V → (((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺))
145	123, 127, 144	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)
146	145	adantllr 717	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)
147	79	ad3antrrr 728	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ V)
148		simpll 765	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)))
149	82	ad3antrrr 728	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
150	107	adantr 483	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ Fin)
151	149, 150	elind 4171	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
152		simpr 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑦)
153	119	eqcomd 2827	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 = (𝐹 “ (^◡𝐹 “ 𝑦)))
154	153	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑦 = (𝐹 “ (^◡𝐹 “ 𝑦)))
155	152, 154	eleqtrd 2915	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))
156	155	adantllr 717	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))
157	148, 151, 156	jca31 517	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))))
158	128	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))))
159		imaeq2 5920	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝐹 “ 𝑥) = (𝐹 “ (^◡𝐹 “ 𝑦)))
160	159	eleq2d 2898	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑘 ∈ (𝐹 “ 𝑥) ↔ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))))
161	158, 160	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) ↔ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))))
162	161	imbi1d 344	. . . . . . . . . 10 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ) ↔ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ)))
163		rge0ssre 12838	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ ℝ
164		ax-resscn 10588	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
165	163, 164	sstri 3976	. . . . . . . . . . . 12 ⊢ (0[,)+∞) ⊆ ℂ
166		simplll 773	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝜑)
167		simpllr 774	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
168		fimass 6550	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐶⟶𝐴 → (𝐹 “ 𝑥) ⊆ 𝐴)
169	23, 168	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 “ 𝑥) ⊆ 𝐴)
170	169	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → (𝐹 “ 𝑥) ⊆ 𝐴)
171		simpr 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ (𝐹 “ 𝑥))
172	170, 171	sseldd 3968	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴)
173	172	adantllr 717	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴)
174		foelrni 6722	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
175	4, 174	sylan 582	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
176	175	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
177		nfv 1911	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛 𝑘 ∈ 𝐴
178	104, 177	nfan 1896	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴)
179		nfv 1911	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛 𝐵 ∈ (0[,)+∞)
180		csbid 3896	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ⦋𝑘 / 𝑘⦌𝐵 = 𝐵
181	180	eqcomi 2830	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 = ⦋𝑘 / 𝑘⦌𝐵
182	181	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = ⦋𝑘 / 𝑘⦌𝐵)
183		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑛) = 𝑘 → (𝐹‘𝑛) = 𝑘)
184	183	eqcomd 2827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑛) = 𝑘 → 𝑘 = (𝐹‘𝑛))
185	184	csbeq1d 3887	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑛) = 𝑘 → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
186	185	3ad2ant3 1131	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
187	38	idi 1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
188	187	3adant3 1128	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
189	182, 186, 188	3eqtrd 2860	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷)
190	189	3adant1r 1173	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷)
191		0xr 10682	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ∈ ℝ^*
192	191	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 0 ∈ ℝ^*)
193		pnfxr 10689	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ +∞ ∈ ℝ^*
194	193	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ℝ^*)
195	64	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈ (0[,]+∞))
196		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬ 𝐷 ∈ (0[,)+∞))
197	192, 194, 195, 196	eliccnelico 41797	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 = +∞)
198	197	eqcomd 2827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ = 𝐷)
199		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝑛 ∈ 𝐶)
200	64	idi 1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,]+∞))
201	14	elrnmpt1 5825	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ 𝐶 ∧ 𝐷 ∈ (0[,]+∞)) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
202	199, 200, 201	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
203	202	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
204	198, 203	eqeltrd 2913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
205	204	adantllr 717	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
206		simpllr 774	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
207	205, 206	condan 816	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,)+∞))
208	207	3adant3 1128	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐷 ∈ (0[,)+∞))
209	190, 208	eqeltrd 2913	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 ∈ (0[,)+∞))
210	209	3exp 1115	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞))))
211	210	adantr 483	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞))))
212	178, 179, 211	rexlimd 3317	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞)))
213	176, 212	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))
214	166, 167, 173, 213	syl21anc 835	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ (0[,)+∞))
215	165, 214	sseldi 3965	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ)
216	215	idi 1	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ)
217	162, 216	vtoclg 3568	. . . . . . . . 9 ⊢ ((^◡𝐹 “ 𝑦) ∈ V → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ))
218	147, 157, 217	sylc 65	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℂ)
219	98, 106, 36, 107, 122, 146, 218	fsumf1of 41847	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷)
220		sumeq1 15039	. . . . . . . 8 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷)
221	220	rspceeqv 3638	. . . . . . 7 ⊢ (((^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin) ∧ Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
222	94, 219, 221	syl2anc 586	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
223	71, 222	rnmptssrn 41434	. . . . 5 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) ⊆ ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷))
224		sumex 15038	. . . . . . 7 ⊢ Σ𝑛 ∈ 𝑥 𝐷 ∈ V
225	224	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 ∈ V)
226	6, 169	ssexd 5221	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 “ 𝑥) ∈ V)
227		elpwg 4545	. . . . . . . . . . . 12 ⊢ ((𝐹 “ 𝑥) ∈ V → ((𝐹 “ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐹 “ 𝑥) ⊆ 𝐴))
228	226, 227	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹 “ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐹 “ 𝑥) ⊆ 𝐴))
229	169, 228	mpbird 259	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 “ 𝑥) ∈ 𝒫 𝐴)
230	229	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ 𝒫 𝐴)
231	23	ffund 6513	. . . . . . . . . . 11 ⊢ (𝜑 → Fun 𝐹)
232	231	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Fun 𝐹)
233		elinel2 4173	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ∈ Fin)
234	233	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ∈ Fin)
235		imafi 8811	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ Fin) → (𝐹 “ 𝑥) ∈ Fin)
236	232, 234, 235	syl2anc 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ Fin)
237	230, 236	elind 4171	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin))
238	237	adantlr 713	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin))
239		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑥 ∈ (𝒫 𝐶 ∩ Fin)
240	96, 239	nfan 1896	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin))
241		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝑥 ∈ (𝒫 𝐶 ∩ Fin)
242	104, 241	nfan 1896	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin))
243	233	adantl 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ∈ Fin)
244	109	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝐹:𝐶–1-1→𝐴)
245		f1ores 6624	. . . . . . . . . . 11 ⊢ ((𝐹:𝐶–1-1→𝐴 ∧ 𝑥 ⊆ 𝐶) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
246	244, 140, 245	syl2anc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
247	246	adantlr 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
248	143	adantllr 717	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺)
249	240, 242, 36, 243, 247, 248, 215	fsumf1of 41847	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
250	249	eqcomd 2827	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵)
251		sumeq1 15039	. . . . . . . 8 ⊢ (𝑦 = (𝐹 “ 𝑥) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵)
252	251	rspceeqv 3638	. . . . . . 7 ⊢ (((𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵)
253	238, 250, 252	syl2anc 586	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵)
254	225, 253	rnmptssrn 41434	. . . . 5 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷) ⊆ ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵))
255	223, 254	eqssd 3984	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) = ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷))
256	255	supeq1d 8904	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ^, < ) = sup(ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ^, < ))
257	6	adantr 483	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V)
258	96, 257, 213	sge0revalmpt 42653	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ^*, < ))
259	1	adantr 483	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉)
260	104, 259, 207	sge0revalmpt 42653	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = sup(ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ^*, < ))
261	256, 258, 260	3eqtr4d 2866	. 2 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
262	69, 261	pm2.61dan 811	1 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 Ⅎwnf 1780 ∈ wcel 2110 ∃wrex 3139 Vcvv 3495 ⦋csb 3883 ∩ cin 3935 ⊆ wss 3936 𝒫 cpw 4539 ↦ cmpt 5139 ^◡ccnv 5549 ran crn 5551 ↾ cres 5552 “ cima 5553 Fun wfun 6344 ⟶wf 6346 –1-1→wf1 6347 –onto→wfo 6348 –1-1-onto→wf1o 6349 ‘cfv 6350 (class class class)co 7150 Fincfn 8503 supcsup 8898 ℂcc 10529 ℝcr 10530 0cc0 10531 +∞cpnf 10666 ℝ^*cxr 10668 < clt 10669 [,)cico 12734 [,]cicc 12735 Σcsu 15036 Σ^{^}csumge0 42637

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-rep 5183 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 ax-un 7455 ax-inf2 9098 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-fal 1546 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3497 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4833 df-int 4870 df-iun 4914 df-br 5060 df-opab 5122 df-mpt 5140 df-tr 5166 df-id 5455 df-eprel 5460 df-po 5469 df-so 5470 df-fr 5509 df-se 5510 df-we 5511 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-pred 6143 df-ord 6189 df-on 6190 df-lim 6191 df-suc 6192 df-iota 6309 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-isom 6359 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-oadd 8100 df-er 8283 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-sup 8900 df-oi 8968 df-card 9362 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-3 11695 df-n0 11892 df-z 11976 df-uz 12238 df-rp 12384 df-ico 12738 df-icc 12739 df-fz 12887 df-fzo 13028 df-seq 13364 df-exp 13424 df-hash 13685 df-cj 14452 df-re 14453 df-im 14454 df-sqrt 14588 df-abs 14589 df-clim 14839 df-sum 15037 df-sumge0 42638

This theorem is referenced by: sge0resrnlem 42678 sge0fodjrnlem 42691 sge0xp 42704 meadjiunlem 42740 isomenndlem 42805 ovnsubaddlem1 42845

W3C validator