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 45560

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 6840	. . . . . . 7 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–onto→𝐴)
4	2, 3	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐶–onto→𝐴)
5		focdmex 7946	. . . . . 6 ⊢ (𝐶 ∈ 𝑉 → (𝐹:𝐶–onto→𝐴 → 𝐴 ∈ V))
6	1, 4, 5	sylc 65	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ V)
7	6	adantr 480	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V)
8		sge0f1o.1	. . . . . 6 ⊢ Ⅎ𝑘𝜑
9		sge0f1o.7	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))
10		eqid 2731	. . . . . 6 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵)
11	8, 9, 10	fmptdf 7118	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞))
12	11	adantr 480	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞))
13		pnfex 11274	. . . . . . . 8 ⊢ +∞ ∈ V
14		eqid 2731	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝐶 ↦ 𝐷) = (𝑛 ∈ 𝐶 ↦ 𝐷)
15	14	elrnmpt 5955	. . . . . . . 8 ⊢ (+∞ ∈ V → (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷))
16	13, 15	ax-mp 5	. . . . . . 7 ⊢ (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷)
17	16	biimpi 215	. . . . . 6 ⊢ (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) → ∃𝑛 ∈ 𝐶 +∞ = 𝐷)
18	17	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ∃𝑛 ∈ 𝐶 +∞ = 𝐷)
19		sge0f1o.2	. . . . . . 7 ⊢ Ⅎ𝑛𝜑
20		nfv 1916	. . . . . . 7 ⊢ Ⅎ𝑛+∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)
21		simp3 1137	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = 𝐷)
22		f1of 6833	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴)
23	2, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:𝐶⟶𝐴)
24	23	ffvelcdmda 7086	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴)
25		sge0f1o.6	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)
26		nfcv 2902	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝐹‘𝑛)
27		nfv 1916	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝐹‘𝑛) = 𝐺
28	26	nfcsb1 3917	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵
29		nfcv 2902	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘𝐷
30	28, 29	nfeq 2915	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷
31	27, 30	nfim 1898	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
32		eqeq1 2735	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 = 𝐺 ↔ (𝐹‘𝑛) = 𝐺))
33		csbeq1a 3907	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
34	33	eqeq1d 2733	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 = 𝐷 ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷))
35	32, 34	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → ((𝑘 = 𝐺 → 𝐵 = 𝐷) ↔ ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)))
36		sge0f1o.3	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)
37	26, 31, 35, 36	vtoclgf 3557	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷))
38	24, 25, 37	sylc 65	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
39	38	eqcomd 2737	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
40	39	3adant3 1131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
41	21, 40	eqtrd 2771	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
42		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝜑)
43	42, 24	jca 511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴))
44		nfv 1916	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝐹‘𝑛) ∈ 𝐴
45	8, 44	nfan 1901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴)
46	28	nfel1 2918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)
47	45, 46	nfim 1898	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))
48		eleq1 2820	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 ∈ 𝐴 ↔ (𝐹‘𝑛) ∈ 𝐴))
49	48	anbi2d 628	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴)))
50	33	eleq1d 2817	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 ∈ (0[,]+∞) ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)))
51	49, 50	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐹‘𝑛) → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))))
52	26, 47, 51, 9	vtoclgf 3557	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)))
53	24, 43, 52	sylc 65	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))
54	28, 10, 33	elrnmpt1sf 44350	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑛) ∈ 𝐴 ∧ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
55	24, 53, 54	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
56	55	3adant3 1131	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
57	41, 56	eqeltrd 2832	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
58	57	3exp 1118	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝐶 → (+∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))))
59	19, 20, 58	rexlimd 3262	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))
60	59	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (∃𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))
61	18, 60	mpd 15	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
62	7, 12, 61	sge0pnfval 45551	. . 3 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = +∞)
63	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉)
64	39, 53	eqeltrd 2832	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,]+∞))
65	19, 64, 14	fmptdf 7118	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞))
66	65	adantr 480	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞))
67		simpr 484	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
68	63, 66, 67	sge0pnfval 45551	. . 3 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = +∞)
69	62, 68	eqtr4d 2774	. 2 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
70		sumex 15641	. . . . . . 7 ⊢ Σ𝑘 ∈ 𝑦 𝐵 ∈ V
71	70	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 ∈ V)
72		cnvimass 6080	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ 𝑦) ⊆ dom 𝐹
73	72, 23	fssdm 6737	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ⊆ 𝐶)
74	23, 1	fexd 7231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ V)
75		cnvexg 7919	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ V → ^◡𝐹 ∈ V)
76	74, 75	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ^◡𝐹 ∈ V)
77		imaexg 7910	. . . . . . . . . . . . 13 ⊢ (^◡𝐹 ∈ V → (^◡𝐹 “ 𝑦) ∈ V)
78	76, 77	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ∈ V)
79		elpwg 4605	. . . . . . . . . . . 12 ⊢ ((^◡𝐹 “ 𝑦) ∈ V → ((^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (^◡𝐹 “ 𝑦) ⊆ 𝐶))
80	78, 79	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (^◡𝐹 “ 𝑦) ⊆ 𝐶))
81	73, 80	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
82	81	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
83		f1ocnv 6845	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → ^◡𝐹:𝐴–1-1-onto→𝐶)
84	2, 83	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ^◡𝐹:𝐴–1-1-onto→𝐶)
85		f1ofun 6835	. . . . . . . . . . . 12 ⊢ (^◡𝐹:𝐴–1-1-onto→𝐶 → Fun ^◡𝐹)
86	84, 85	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → Fun ^◡𝐹)
87	86	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Fun ^◡𝐹)
88		elinel2 4196	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
89	88	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin)
90		imafi 9181	. . . . . . . . . 10 ⊢ ((Fun ^◡𝐹 ∧ 𝑦 ∈ Fin) → (^◡𝐹 “ 𝑦) ∈ Fin)
91	87, 89, 90	syl2anc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ Fin)
92	82, 91	elind 4194	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
93	92	adantlr 712	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
94		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑘 ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
95	8, 94	nfan 1901	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
96		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑘 𝑦 ∈ (𝒫 𝐴 ∩ Fin)
97	95, 96	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
98		nfcv 2902	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛+∞
99		nfmpt1 5256	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(𝑛 ∈ 𝐶 ↦ 𝐷)
100	99	nfrn 5951	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛ran (𝑛 ∈ 𝐶 ↦ 𝐷)
101	98, 100	nfel 2916	. . . . . . . . . . 11 ⊢ Ⅎ𝑛+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
102	101	nfn 1859	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
103	19, 102	nfan 1901	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
104		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑛 𝑦 ∈ (𝒫 𝐴 ∩ Fin)
105	103, 104	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
106	91	adantlr 712	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ Fin)
107		f1of1 6832	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–1-1→𝐴)
108	2, 107	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐶–1-1→𝐴)
109	108	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐶–1-1→𝐴)
110	80	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶 ↔ (^◡𝐹 “ 𝑦) ⊆ 𝐶))
111	82, 110	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ⊆ 𝐶)
112		f1ores 6847	. . . . . . . . . . 11 ⊢ ((𝐹:𝐶–1-1→𝐴 ∧ (^◡𝐹 “ 𝑦) ⊆ 𝐶) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)))
113	109, 111, 112	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)))
114	4	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐶–onto→𝐴)
115		elpwinss 44201	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴)
116	115	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ⊆ 𝐴)
117		foimacnv 6850	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝐹 “ (^◡𝐹 “ 𝑦)) = 𝑦)
118	114, 116, 117	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ (^◡𝐹 “ 𝑦)) = 𝑦)
119	118	f1oeq3d 6830	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)) ↔ (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦))
120	113, 119	mpbid 231	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦)
121	120	adantlr 712	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦)
122	78	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → (^◡𝐹 “ 𝑦) ∈ V)
123		simpll 764	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → 𝜑)
124	92	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
125		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → 𝑛 ∈ (^◡𝐹 “ 𝑦))
126	123, 124, 125	jca31 514	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)))
127		eleq1 2820	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↔ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)))
128	127	anbi2d 628	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ (𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))))
129		eleq2 2821	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑛 ∈ 𝑥 ↔ 𝑛 ∈ (^◡𝐹 “ 𝑦)))
130	128, 129	anbi12d 630	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) ↔ ((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦))))
131		reseq2 5976	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝐹 ↾ 𝑥) = (𝐹 ↾ (^◡𝐹 “ 𝑦)))
132	131	fveq1d 6893	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((𝐹 ↾ 𝑥)‘𝑛) = ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛))
133	132	eqeq1d 2733	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝐹 ↾ 𝑥)‘𝑛) = 𝐺 ↔ ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺))
134	130, 133	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺) ↔ (((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)))
135		fvres 6910	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑥 → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛))
136	135	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛))
137		simpll 764	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝜑)
138		elpwinss 44201	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ⊆ 𝐶)
139	138	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ⊆ 𝐶)
140	139	sselda 3982	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝑛 ∈ 𝐶)
141	137, 140, 25	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → (𝐹‘𝑛) = 𝐺)
142	136, 141	eqtrd 2771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺)
143	134, 142	vtoclg 3542	. . . . . . . . . 10 ⊢ ((^◡𝐹 “ 𝑦) ∈ V → (((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺))
144	122, 126, 143	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)
145	144	adantllr 716	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)
146	78	ad3antrrr 727	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ V)
147		simpll 764	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)))
148	81	ad3antrrr 727	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
149	106	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ Fin)
150	148, 149	elind 4194	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
151		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑦)
152	118	eqcomd 2737	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 = (𝐹 “ (^◡𝐹 “ 𝑦)))
153	152	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑦 = (𝐹 “ (^◡𝐹 “ 𝑦)))
154	151, 153	eleqtrd 2834	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))
155	154	adantllr 716	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))
156	147, 150, 155	jca31 514	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))))
157	127	anbi2d 628	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))))
158		imaeq2 6055	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝐹 “ 𝑥) = (𝐹 “ (^◡𝐹 “ 𝑦)))
159	158	eleq2d 2818	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑘 ∈ (𝐹 “ 𝑥) ↔ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))))
160	157, 159	anbi12d 630	. . . . . . . . . . 11 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) ↔ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))))
161	160	imbi1d 341	. . . . . . . . . 10 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ) ↔ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ)))
162		rge0ssre 13440	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ ℝ
163		ax-resscn 11173	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
164	162, 163	sstri 3991	. . . . . . . . . . . 12 ⊢ (0[,)+∞) ⊆ ℂ
165		simplll 772	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝜑)
166		simpllr 773	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
167		fimass 6738	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐶⟶𝐴 → (𝐹 “ 𝑥) ⊆ 𝐴)
168	23, 167	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 “ 𝑥) ⊆ 𝐴)
169	168	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → (𝐹 “ 𝑥) ⊆ 𝐴)
170		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ (𝐹 “ 𝑥))
171	169, 170	sseldd 3983	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴)
172	171	adantllr 716	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴)
173		foelcdmi 6953	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
174	4, 173	sylan 579	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
175	174	adantlr 712	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
176		nfv 1916	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛 𝑘 ∈ 𝐴
177	103, 176	nfan 1901	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴)
178		nfv 1916	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛 𝐵 ∈ (0[,)+∞)
179		csbid 3906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ⦋𝑘 / 𝑘⦌𝐵 = 𝐵
180	179	eqcomi 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 = ⦋𝑘 / 𝑘⦌𝐵
181	180	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = ⦋𝑘 / 𝑘⦌𝐵)
182		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑛) = 𝑘 → (𝐹‘𝑛) = 𝑘)
183	182	eqcomd 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑛) = 𝑘 → 𝑘 = (𝐹‘𝑛))
184	183	csbeq1d 3897	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑛) = 𝑘 → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
185	184	3ad2ant3 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
186	38	idi 1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
187	186	3adant3 1131	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
188	181, 185, 187	3eqtrd 2775	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷)
189	188	3adant1r 1176	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷)
190		0xr 11268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ∈ ℝ^*
191	190	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 0 ∈ ℝ^*)
192		pnfxr 11275	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ +∞ ∈ ℝ^*
193	192	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ℝ^*)
194	64	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈ (0[,]+∞))
195		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬ 𝐷 ∈ (0[,)+∞))
196	191, 193, 194, 195	eliccnelico 44704	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 = +∞)
197	196	eqcomd 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ = 𝐷)
198		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝑛 ∈ 𝐶)
199	64	idi 1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,]+∞))
200	14	elrnmpt1 5957	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ 𝐶 ∧ 𝐷 ∈ (0[,]+∞)) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
201	198, 199, 200	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
202	201	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
203	197, 202	eqeltrd 2832	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
204	203	adantllr 716	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
205		simpllr 773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
206	204, 205	condan 815	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,)+∞))
207	206	3adant3 1131	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐷 ∈ (0[,)+∞))
208	189, 207	eqeltrd 2832	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 ∈ (0[,)+∞))
209	208	3exp 1118	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞))))
210	209	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞))))
211	177, 178, 210	rexlimd 3262	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞)))
212	175, 211	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))
213	165, 166, 172, 212	syl21anc 835	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ (0[,)+∞))
214	164, 213	sselid 3980	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ)
215	214	idi 1	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ)
216	161, 215	vtoclg 3542	. . . . . . . . 9 ⊢ ((^◡𝐹 “ 𝑦) ∈ V → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ))
217	146, 156, 216	sylc 65	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℂ)
218	97, 105, 36, 106, 121, 145, 217	fsumf1of 44752	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷)
219		sumeq1 15642	. . . . . . . 8 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷)
220	219	rspceeqv 3633	. . . . . . 7 ⊢ (((^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin) ∧ Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
221	93, 218, 220	syl2anc 583	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
222	71, 221	rnmptssrn 44343	. . . . 5 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) ⊆ ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷))
223		sumex 15641	. . . . . . 7 ⊢ Σ𝑛 ∈ 𝑥 𝐷 ∈ V
224	223	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 ∈ V)
225	6, 168	ssexd 5324	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 “ 𝑥) ∈ V)
226		elpwg 4605	. . . . . . . . . . . 12 ⊢ ((𝐹 “ 𝑥) ∈ V → ((𝐹 “ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐹 “ 𝑥) ⊆ 𝐴))
227	225, 226	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹 “ 𝑥) ∈ 𝒫 𝐴 ↔ (𝐹 “ 𝑥) ⊆ 𝐴))
228	168, 227	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 “ 𝑥) ∈ 𝒫 𝐴)
229	228	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ 𝒫 𝐴)
230	23	ffund 6721	. . . . . . . . . . 11 ⊢ (𝜑 → Fun 𝐹)
231	230	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Fun 𝐹)
232		elinel2 4196	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ∈ Fin)
233	232	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ∈ Fin)
234		imafi 9181	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ Fin) → (𝐹 “ 𝑥) ∈ Fin)
235	231, 233, 234	syl2anc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ Fin)
236	229, 235	elind 4194	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin))
237	236	adantlr 712	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin))
238		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑥 ∈ (𝒫 𝐶 ∩ Fin)
239	95, 238	nfan 1901	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin))
240		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝑥 ∈ (𝒫 𝐶 ∩ Fin)
241	103, 240	nfan 1901	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin))
242	232	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ∈ Fin)
243	108	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝐹:𝐶–1-1→𝐴)
244		f1ores 6847	. . . . . . . . . . 11 ⊢ ((𝐹:𝐶–1-1→𝐴 ∧ 𝑥 ⊆ 𝐶) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
245	243, 139, 244	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
246	245	adantlr 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
247	142	adantllr 716	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺)
248	239, 241, 36, 242, 246, 247, 214	fsumf1of 44752	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
249	248	eqcomd 2737	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵)
250		sumeq1 15642	. . . . . . . 8 ⊢ (𝑦 = (𝐹 “ 𝑥) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵)
251	250	rspceeqv 3633	. . . . . . 7 ⊢ (((𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵)
252	237, 249, 251	syl2anc 583	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵)
253	224, 252	rnmptssrn 44343	. . . . 5 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷) ⊆ ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵))
254	222, 253	eqssd 3999	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) = ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷))
255	254	supeq1d 9447	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ^, < ) = sup(ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ^, < ))
256	6	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V)
257	95, 256, 212	sge0revalmpt 45556	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ^*, < ))
258	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉)
259	103, 258, 206	sge0revalmpt 45556	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = sup(ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ^*, < ))
260	255, 257, 259	3eqtr4d 2781	. 2 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
261	69, 260	pm2.61dan 810	1 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1086 = wceq 1540 Ⅎwnf 1784 ∈ wcel 2105 ∃wrex 3069 Vcvv 3473 ⦋csb 3893 ∩ cin 3947 ⊆ wss 3948 𝒫 cpw 4602 ↦ cmpt 5231 ^◡ccnv 5675 ran crn 5677 ↾ cres 5678 “ cima 5679 Fun wfun 6537 ⟶wf 6539 –1-1→wf1 6540 –onto→wfo 6541 –1-1-onto→wf1o 6542 ‘cfv 6543 (class class class)co 7412 Fincfn 8945 supcsup 9441 ℂcc 11114 ℝcr 11115 0cc0 11116 +∞cpnf 11252 ℝ^*cxr 11254 < clt 11255 [,)cico 13333 [,]cicc 13334 Σcsu 15639 Σ^{^}csumge0 45540

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-inf2 9642 ax-cnex 11172 ax-resscn 11173 ax-1cn 11174 ax-icn 11175 ax-addcl 11176 ax-addrcl 11177 ax-mulcl 11178 ax-mulrcl 11179 ax-mulcom 11180 ax-addass 11181 ax-mulass 11182 ax-distr 11183 ax-i2m1 11184 ax-1ne0 11185 ax-1rid 11186 ax-rnegex 11187 ax-rrecex 11188 ax-cnre 11189 ax-pre-lttri 11190 ax-pre-lttrn 11191 ax-pre-ltadd 11192 ax-pre-mulgt0 11193 ax-pre-sup 11194

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7860 df-1st 7979 df-2nd 7980 df-frecs 8272 df-wrecs 8303 df-recs 8377 df-rdg 8416 df-1o 8472 df-er 8709 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-sup 9443 df-oi 9511 df-card 9940 df-pnf 11257 df-mnf 11258 df-xr 11259 df-ltxr 11260 df-le 11261 df-sub 11453 df-neg 11454 df-div 11879 df-nn 12220 df-2 12282 df-3 12283 df-n0 12480 df-z 12566 df-uz 12830 df-rp 12982 df-ico 13337 df-icc 13338 df-fz 13492 df-fzo 13635 df-seq 13974 df-exp 14035 df-hash 14298 df-cj 15053 df-re 15054 df-im 15055 df-sqrt 15189 df-abs 15190 df-clim 15439 df-sum 15640 df-sumge0 45541

This theorem is referenced by: sge0resrnlem 45581 sge0fodjrnlem 45594 sge0xp 45607 meadjiunlem 45643 isomenndlem 45708 ovnsubaddlem1 45748

W3C validator