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 43432

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 6614	. . . . . . 7 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–onto→𝐴)
4	2, 3	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐶–onto→𝐴)
5		fornex 7667	. . . . . 6 ⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V))
6	1, 4, 5	sylc 65	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ V)
7	6	adantr 484	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V)
8		sge0f1o.1	. . . . . 6 ⊢ Ⅎ𝑘𝜑
9		sge0f1o.7	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
10		eqid 2758	. . . . . 6 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵)
11	8, 9, 10	fmptdf 6878	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞))
12	11	adantr 484	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞))
13		pnfex 10745	. . . . . . . 8 ⊢ +∞ ∈ V
14		eqid 2758	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝐶 ↦ 𝐷) = (𝑛 ∈ 𝐶 ↦ 𝐷)
15	14	elrnmpt 5802	. . . . . . . 8 ⊢ (+∞ ∈ V → (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷))
16	13, 15	ax-mp 5	. . . . . . 7 ⊢ (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷)
17	16	biimpi 219	. . . . . 6 ⊢ (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) → ∃𝑛 ∈ 𝐶 +∞ = 𝐷)
18	17	adantl 485	. . . . 5 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ∃𝑛 ∈ 𝐶 +∞ = 𝐷)
19		sge0f1o.2	. . . . . . 7 ⊢ Ⅎ𝑛𝜑
20		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑛+∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)
21		simp3 1135	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = 𝐷)
22		f1of 6607	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴)
23	2, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:𝐶⟶𝐴)
24	23	ffvelrnda 6848	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴)
25		sge0f1o.6	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)
26		nfcv 2919	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝐹‘𝑛)
27		nfv 1915	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝐹‘𝑛) = 𝐺
28	26	nfcsb1 3830	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵
29		nfcv 2919	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝐷
30	28, 29	nfeq 2932	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷
31	27, 30	nfim 1897	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
32		eqeq1 2762	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 = 𝐺 ↔ (𝐹‘𝑛) = 𝐺))
33		csbeq1a 3821	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
34	33	eqeq1d 2760	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 = 𝐷 ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷))
35	32, 34	imbi12d 348	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → ((𝑘 = 𝐺 → 𝐵 = 𝐷) ↔ ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)))
36		sge0f1o.3	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)
37	26, 31, 35, 36	vtoclgf 3485	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷))
38	24, 25, 37	sylc 65	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
39	38	eqcomd 2764	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
40	39	3adant3 1129	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
41	21, 40	eqtrd 2793	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
42		simpl 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝜑)
43	42, 24	jca 515	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴))
44		nfv 1915	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝐹‘𝑛) ∈ 𝐴
45	8, 44	nfan 1900	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴)
46	28	nfel1 2935	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)
47	45, 46	nfim 1897	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))
48		eleq1 2839	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 ∈ 𝐴 ↔ (𝐹‘𝑛) ∈ 𝐴))
49	48	anbi2d 631	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴)))
50	33	eleq1d 2836	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 ∈ (0[,]+∞) ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)))
51	49, 50	imbi12d 348	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐹‘𝑛) → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))))
52	26, 47, 51, 9	vtoclgf 3485	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)))
53	24, 43, 52	sylc 65	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))
54	28, 10, 33	elrnmpt1sf 42231	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑛) ∈ 𝐴 ∧ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
55	24, 53, 54	syl2anc 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
56	55	3adant3 1129	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
57	41, 56	eqeltrd 2852	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
58	57	3exp 1116	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝐶 → (+∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))))
59	19, 20, 58	rexlimd 3241	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))
60	59	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (∃𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))
61	18, 60	mpd 15	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
62	7, 12, 61	sge0pnfval 43423	. . 3 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = +∞)
63	1	adantr 484	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉)
64	39, 53	eqeltrd 2852	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,]+∞))
65	19, 64, 14	fmptdf 6878	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞))
66	65	adantr 484	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞))
67		simpr 488	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
68	63, 66, 67	sge0pnfval 43423	. . 3 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = +∞)
69	62, 68	eqtr4d 2796	. 2 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
70		sumex 15105	. . . . . . 7 ⊢ Σ𝑘 ∈ 𝑦 𝐵 ∈ V
71	70	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 ∈ V)
72		cnvimass 5926	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ 𝑦) ⊆ dom 𝐹
73	72, 23	fssdm 6520	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ⊆ 𝐶)
74		fex 6986	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐶⟶𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐹 ∈ V)
75	23, 1, 74	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ V)
76		cnvexg 7640	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ V → ^◡𝐹 ∈ V)
77	75, 76	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ^◡𝐹 ∈ V)
78		imaexg 7631	. . . . . . . . . . . . 13 ⊢ (^◡𝐹 ∈ V → (^◡𝐹 “ 𝑦) ∈ V)
79	77, 78	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ∈ V)
80		elpwg 4500	. . . . . . . . . . . 12 ⊢ ((^◡𝐹 “ 𝑦) ∈ V → ((^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (^◡𝐹 “ 𝑦) ⊆ 𝐶))
81	79, 80	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (^◡𝐹 “ 𝑦) ⊆ 𝐶))
82	73, 81	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
83	82	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
84		f1ocnv 6619	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → ^◡𝐹:𝐴–1-1-onto→𝐶)
85	2, 84	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ^◡𝐹:𝐴–1-1-onto→𝐶)
86		f1ofun 6609	. . . . . . . . . . . 12 ⊢ (^◡𝐹:𝐴–1-1-onto→𝐶 → Fun ^◡𝐹)
87	85, 86	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → Fun ^◡𝐹)
88	87	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Fun ^◡𝐹)
89		elinel2 4103	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
90	89	adantl 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin)
91		imafi 8756	. . . . . . . . . 10 ⊢ ((Fun ^◡𝐹 ∧ 𝑦 ∈ Fin) → (^◡𝐹 “ 𝑦) ∈ Fin)
92	88, 90, 91	syl2anc 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ Fin)
93	83, 92	elind 4101	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
94	93	adantlr 714	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
95		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑘 ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
96	8, 95	nfan 1900	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
97		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑘 𝑦 ∈ (𝒫 𝐴 ∩ Fin)
98	96, 97	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
99		nfcv 2919	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛+∞
100		nfmpt1 5134	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(𝑛 ∈ 𝐶 ↦ 𝐷)
101	100	nfrn 5798	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛ran (𝑛 ∈ 𝐶 ↦ 𝐷)
102	99, 101	nfel 2933	. . . . . . . . . . 11 ⊢ Ⅎ𝑛+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
103	102	nfn 1858	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
104	19, 103	nfan 1900	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
105		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑛 𝑦 ∈ (𝒫 𝐴 ∩ Fin)
106	104, 105	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
107	92	adantlr 714	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ Fin)
108		f1of1 6606	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–1-1→𝐴)
109	2, 108	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐶–1-1→𝐴)
110	109	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐶–1-1→𝐴)
111	81	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (^◡𝐹 “ 𝑦) ⊆ 𝐶))
112	83, 111	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ⊆ 𝐶)
113		f1ores 6621	. . . . . . . . . . 11 ⊢ ((𝐹:𝐶–1-1→𝐴 ∧ (^◡𝐹 “ 𝑦) ⊆ 𝐶) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)))
114	110, 112, 113	syl2anc 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)))
115	4	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐶–onto→𝐴)
116		elpwinss 42101	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴)
117	116	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ⊆ 𝐴)
118		foimacnv 6624	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝐹 “ (^◡𝐹 “ 𝑦)) = 𝑦)
119	115, 117, 118	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ (^◡𝐹 “ 𝑦)) = 𝑦)
120	119	f1oeq3d 6604	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)) ↔ (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦))
121	114, 120	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦)
122	121	adantlr 714	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦)
123	79	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → (^◡𝐹 “ 𝑦) ∈ V)
124		simpll 766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → 𝜑)
125	93	adantr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
126		simpr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → 𝑛 ∈ (^◡𝐹 “ 𝑦))
127	124, 125, 126	jca31 518	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)))
128		eleq1 2839	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↔ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)))
129	128	anbi2d 631	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ (𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))))
130		eleq2 2840	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑛 ∈ 𝑥 ↔ 𝑛 ∈ (^◡𝐹 “ 𝑦)))
131	129, 130	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) ↔ ((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦))))
132		reseq2 5823	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝐹 ↾ 𝑥) = (𝐹 ↾ (^◡𝐹 “ 𝑦)))
133	132	fveq1d 6665	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((𝐹 ↾ 𝑥)‘𝑛) = ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛))
134	133	eqeq1d 2760	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝐹 ↾ 𝑥)‘𝑛) = 𝐺 ↔ ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺))
135	131, 134	imbi12d 348	. . . . . . . . . . 11 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺) ↔ (((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)))
136		fvres 6682	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑥 → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛))
137	136	adantl 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛))
138		simpll 766	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝜑)
139		elpwinss 42101	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ⊆ 𝐶)
140	139	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ⊆ 𝐶)
141	140	sselda 3894	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝑛 ∈ 𝐶)
142	138, 141, 25	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → (𝐹‘𝑛) = 𝐺)
143	137, 142	eqtrd 2793	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺)
144	135, 143	vtoclg 3487	. . . . . . . . . 10 ⊢ ((^◡𝐹 “ 𝑦) ∈ V → (((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺))
145	123, 127, 144	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)
146	145	adantllr 718	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)
147	79	ad3antrrr 729	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ V)
148		simpll 766	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)))
149	82	ad3antrrr 729	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
150	107	adantr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ Fin)
151	149, 150	elind 4101	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
152		simpr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑦)
153	119	eqcomd 2764	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 = (𝐹 “ (^◡𝐹 “ 𝑦)))
154	153	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑦 = (𝐹 “ (^◡𝐹 “ 𝑦)))
155	152, 154	eleqtrd 2854	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))
156	155	adantllr 718	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))
157	148, 151, 156	jca31 518	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))))
158	128	anbi2d 631	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))))
159		imaeq2 5902	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝐹 “ 𝑥) = (𝐹 “ (^◡𝐹 “ 𝑦)))
160	159	eleq2d 2837	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑘 ∈ (𝐹 “ 𝑥) ↔ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))))
161	158, 160	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) ↔ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))))
162	161	imbi1d 345	. . . . . . . . . 10 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ) ↔ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ)))
163		rge0ssre 12901	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ ℝ
164		ax-resscn 10645	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
165	163, 164	sstri 3903	. . . . . . . . . . . 12 ⊢ (0[,)+∞) ⊆ ℂ
166		simplll 774	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝜑)
167		simpllr 775	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
168		fimass 6545	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐶⟶𝐴 → (𝐹 “ 𝑥) ⊆ 𝐴)
169	23, 168	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 “ 𝑥) ⊆ 𝐴)
170	169	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → (𝐹 “ 𝑥) ⊆ 𝐴)
171		simpr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ (𝐹 “ 𝑥))
172	170, 171	sseldd 3895	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴)
173	172	adantllr 718	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴)
174		foelrni 6720	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
175	4, 174	sylan 583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
176	175	adantlr 714	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
177		nfv 1915	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛 𝑘 ∈ 𝐴
178	104, 177	nfan 1900	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴)
179		nfv 1915	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛 𝐵 ∈ (0[,)+∞)
180		csbid 3820	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ⦋𝑘 / 𝑘⦌𝐵 = 𝐵
181	180	eqcomi 2767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 = ⦋𝑘 / 𝑘⦌𝐵
182	181	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = ⦋𝑘 / 𝑘⦌𝐵)
183		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑛) = 𝑘 → (𝐹‘𝑛) = 𝑘)
184	183	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑛) = 𝑘 → 𝑘 = (𝐹‘𝑛))
185	184	csbeq1d 3811	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑛) = 𝑘 → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
186	185	3ad2ant3 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
187	38	idi 1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
188	187	3adant3 1129	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
189	182, 186, 188	3eqtrd 2797	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷)
190	189	3adant1r 1174	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷)
191		0xr 10739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ∈ ℝ^*
192	191	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 0 ∈ ℝ^*)
193		pnfxr 10746	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ +∞ ∈ ℝ^*
194	193	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ℝ^*)
195	64	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈ (0[,]+∞))
196		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬ 𝐷 ∈ (0[,)+∞))
197	192, 194, 195, 196	eliccnelico 42577	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 = +∞)
198	197	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ = 𝐷)
199		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝑛 ∈ 𝐶)
200	64	idi 1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,]+∞))
201	14	elrnmpt1 5804	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ 𝐶 ∧ 𝐷 ∈ (0[,]+∞)) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
202	199, 200, 201	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
203	202	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
204	198, 203	eqeltrd 2852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
205	204	adantllr 718	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
206		simpllr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
207	205, 206	condan 817	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,)+∞))
208	207	3adant3 1129	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐷 ∈ (0[,)+∞))
209	190, 208	eqeltrd 2852	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 ∈ (0[,)+∞))
210	209	3exp 1116	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞))))
211	210	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞))))
212	178, 179, 211	rexlimd 3241	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞)))
213	176, 212	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))
214	166, 167, 173, 213	syl21anc 836	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ (0[,)+∞))
215	165, 214	sseldi 3892	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ)
216	215	idi 1	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ)
217	162, 216	vtoclg 3487	. . . . . . . . 9 ⊢ ((^◡𝐹 “ 𝑦) ∈ V → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ))
218	147, 157, 217	sylc 65	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℂ)
219	98, 106, 36, 107, 122, 146, 218	fsumf1of 42627	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷)
220		sumeq1 15106	. . . . . . . 8 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷)
221	220	rspceeqv 3558	. . . . . . 7 ⊢ (((^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin) ∧ Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
222	94, 219, 221	syl2anc 587	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
223	71, 222	rnmptssrn 42223	. . . . 5 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) ⊆ ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷))
224		sumex 15105	. . . . . . 7 ⊢ Σ𝑛 ∈ 𝑥 𝐷 ∈ V
225	224	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 ∈ V)
226	6, 169	ssexd 5198	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 “ 𝑥) ∈ V)
227		elpwg 4500	. . . . . . . . . . . 12 ⊢ ((𝐹 “ 𝑥) ∈ V → ((𝐹 “ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐹 “ 𝑥) ⊆ 𝐴))
228	226, 227	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹 “ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐹 “ 𝑥) ⊆ 𝐴))
229	169, 228	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 “ 𝑥) ∈ 𝒫 𝐴)
230	229	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ 𝒫 𝐴)
231	23	ffund 6507	. . . . . . . . . . 11 ⊢ (𝜑 → Fun 𝐹)
232	231	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Fun 𝐹)
233		elinel2 4103	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ∈ Fin)
234	233	adantl 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ∈ Fin)
235		imafi 8756	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ Fin) → (𝐹 “ 𝑥) ∈ Fin)
236	232, 234, 235	syl2anc 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ Fin)
237	230, 236	elind 4101	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin))
238	237	adantlr 714	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin))
239		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑥 ∈ (𝒫 𝐶 ∩ Fin)
240	96, 239	nfan 1900	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin))
241		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝑥 ∈ (𝒫 𝐶 ∩ Fin)
242	104, 241	nfan 1900	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin))
243	233	adantl 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ∈ Fin)
244	109	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝐹:𝐶–1-1→𝐴)
245		f1ores 6621	. . . . . . . . . . 11 ⊢ ((𝐹:𝐶–1-1→𝐴 ∧ 𝑥 ⊆ 𝐶) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
246	244, 140, 245	syl2anc 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
247	246	adantlr 714	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
248	143	adantllr 718	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺)
249	240, 242, 36, 243, 247, 248, 215	fsumf1of 42627	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
250	249	eqcomd 2764	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵)
251		sumeq1 15106	. . . . . . . 8 ⊢ (𝑦 = (𝐹 “ 𝑥) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵)
252	251	rspceeqv 3558	. . . . . . 7 ⊢ (((𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵)
253	238, 250, 252	syl2anc 587	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵)
254	225, 253	rnmptssrn 42223	. . . . 5 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷) ⊆ ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵))
255	223, 254	eqssd 3911	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) = ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷))
256	255	supeq1d 8956	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ^, < ) = sup(ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ^, < ))
257	6	adantr 484	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V)
258	96, 257, 213	sge0revalmpt 43428	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ^*, < ))
259	1	adantr 484	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉)
260	104, 259, 207	sge0revalmpt 43428	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = sup(ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ^*, < ))
261	256, 258, 260	3eqtr4d 2803	. 2 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
262	69, 261	pm2.61dan 812	1 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 = wceq 1538 Ⅎwnf 1785 ∈ wcel 2111 ∃wrex 3071 Vcvv 3409 ⦋csb 3807 ∩ cin 3859 ⊆ wss 3860 𝒫 cpw 4497 ↦ cmpt 5116 ^◡ccnv 5527 ran crn 5529 ↾ cres 5530 “ cima 5531 Fun wfun 6334 ⟶wf 6336 –1-1→wf1 6337 –onto→wfo 6338 –1-1-onto→wf1o 6339 ‘cfv 6340 (class class class)co 7156 Fincfn 8540 supcsup 8950 ℂcc 10586 ℝcr 10587 0cc0 10588 +∞cpnf 10723 ℝ^*cxr 10725 < clt 10726 [,)cico 12794 [,]cicc 12795 Σcsu 15103 Σ^{^}csumge0 43412

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5160 ax-sep 5173 ax-nul 5180 ax-pow 5238 ax-pr 5302 ax-un 7465 ax-inf2 9150 ax-cnex 10644 ax-resscn 10645 ax-1cn 10646 ax-icn 10647 ax-addcl 10648 ax-addrcl 10649 ax-mulcl 10650 ax-mulrcl 10651 ax-mulcom 10652 ax-addass 10653 ax-mulass 10654 ax-distr 10655 ax-i2m1 10656 ax-1ne0 10657 ax-1rid 10658 ax-rnegex 10659 ax-rrecex 10660 ax-cnre 10661 ax-pre-lttri 10662 ax-pre-lttrn 10663 ax-pre-ltadd 10664 ax-pre-mulgt0 10665 ax-pre-sup 10666

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-pss 3879 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4802 df-int 4842 df-iun 4888 df-br 5037 df-opab 5099 df-mpt 5117 df-tr 5143 df-id 5434 df-eprel 5439 df-po 5447 df-so 5448 df-fr 5487 df-se 5488 df-we 5489 df-xp 5534 df-rel 5535 df-cnv 5536 df-co 5537 df-dm 5538 df-rn 5539 df-res 5540 df-ima 5541 df-pred 6131 df-ord 6177 df-on 6178 df-lim 6179 df-suc 6180 df-iota 6299 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-isom 6349 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7586 df-1st 7699 df-2nd 7700 df-wrecs 7963 df-recs 8024 df-rdg 8062 df-1o 8118 df-er 8305 df-en 8541 df-dom 8542 df-sdom 8543 df-fin 8544 df-sup 8952 df-oi 9020 df-card 9414 df-pnf 10728 df-mnf 10729 df-xr 10730 df-ltxr 10731 df-le 10732 df-sub 10923 df-neg 10924 df-div 11349 df-nn 11688 df-2 11750 df-3 11751 df-n0 11948 df-z 12034 df-uz 12296 df-rp 12444 df-ico 12798 df-icc 12799 df-fz 12953 df-fzo 13096 df-seq 13432 df-exp 13493 df-hash 13754 df-cj 14519 df-re 14520 df-im 14521 df-sqrt 14655 df-abs 14656 df-clim 14906 df-sum 15104 df-sumge0 43413

This theorem is referenced by: sge0resrnlem 43453 sge0fodjrnlem 43466 sge0xp 43479 meadjiunlem 43515 isomenndlem 43580 ovnsubaddlem1 43620

W3C validator