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 46363

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 6771	. . . . . . 7 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–onto→𝐴)
4	2, 3	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐶–onto→𝐴)
5		focdmex 7891	. . . . . 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	8, 9	fmptd2f 45213	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞))
11	10	adantr 480	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞))
12		sge0f1o.2	. . . . . 6 ⊢ Ⅎ𝑛𝜑
13		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑛+∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)
14		simp3 1138	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = 𝐷)
15		f1of 6764	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴)
16	2, 15	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:𝐶⟶𝐴)
17	16	ffvelcdmda 7018	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴)
18		sge0f1o.6	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)
19		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝐹‘𝑛) = 𝐺
20		nfcsb1v 3875	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵
21	20	nfeq1 2907	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷
22	19, 21	nfim 1896	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
23		eqeq1 2733	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 = 𝐺 ↔ (𝐹‘𝑛) = 𝐺))
24		csbeq1a 3865	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
25	24	eqeq1d 2731	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 = 𝐷 ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷))
26	23, 25	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐹‘𝑛) → ((𝑘 = 𝐺 → 𝐵 = 𝐷) ↔ ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)))
27		sge0f1o.3	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)
28	22, 26, 27	vtoclg1f 3525	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝐹‘𝑛) = 𝐺 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷))
29	17, 18, 28	sylc 65	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
30	29	eqcomd 2735	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
31	30	3adant3 1132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → 𝐷 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
32	14, 31	eqtrd 2764	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
33		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝜑)
34	33, 17	jca 511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴))
35		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘(𝐹‘𝑛) ∈ 𝐴
36	8, 35	nfan 1899	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘(𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴)
37	20	nfel1 2908	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)
38	36, 37	nfim 1896	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))
39		eleq1 2816	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝐹‘𝑛) → (𝑘 ∈ 𝐴 ↔ (𝐹‘𝑛) ∈ 𝐴))
40	39	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐹‘𝑛) → ((𝜑 ∧ 𝑘 ∈ 𝐴) ↔ (𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴)))
41	24	eleq1d 2813	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 ∈ (0[,]+∞) ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)))
42	40, 41	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐹‘𝑛) → (((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))))
43	38, 42, 9	vtoclg1f 3525	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → ((𝜑 ∧ (𝐹‘𝑛) ∈ 𝐴) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)))
44	17, 34, 43	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞))
45		eqid 2729	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵)
46	20, 45, 24	elrnmpt1sf 45167	. . . . . . . . . 10 ⊢ (((𝐹‘𝑛) ∈ 𝐴 ∧ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ (0[,]+∞)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
47	17, 44, 46	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
48	47	3adant3 1132	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
49	32, 48	eqeltrd 2828	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
50	49	3exp 1119	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ 𝐶 → (+∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))))
51	12, 13, 50	rexlimd 3236	. . . . 5 ⊢ (𝜑 → (∃𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵)))
52		pnfex 11168	. . . . . . 7 ⊢ +∞ ∈ V
53		eqid 2729	. . . . . . . 8 ⊢ (𝑛 ∈ 𝐶 ↦ 𝐷) = (𝑛 ∈ 𝐶 ↦ 𝐷)
54	53	elrnmpt 5900	. . . . . . 7 ⊢ (+∞ ∈ V → (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷))
55	52, 54	ax-mp 5	. . . . . 6 ⊢ (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) ↔ ∃𝑛 ∈ 𝐶 +∞ = 𝐷)
56	55	biimpi 216	. . . . 5 ⊢ (+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷) → ∃𝑛 ∈ 𝐶 +∞ = 𝐷)
57	51, 56	impel 505	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑘 ∈ 𝐴 ↦ 𝐵))
58	7, 11, 57	sge0pnfval 46354	. . 3 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = +∞)
59	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉)
60	30, 44	eqeltrd 2828	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,]+∞))
61	12, 60	fmptd2f 45213	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞))
62	61	adantr 480	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 ↦ 𝐷):𝐶⟶(0[,]+∞))
63		simpr 484	. . . 4 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
64	59, 62, 63	sge0pnfval 46354	. . 3 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = +∞)
65	58, 64	eqtr4d 2767	. 2 ⊢ ((𝜑 ∧ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
66		sumex 15595	. . . . . . 7 ⊢ Σ𝑘 ∈ 𝑦 𝐵 ∈ V
67	66	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 ∈ V)
68		cnvimass 6033	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ 𝑦) ⊆ dom 𝐹
69	68, 16	fssdm 6671	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ⊆ 𝐶)
70	1, 69	sselpwd 5267	. . . . . . . . . 10 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
71	70	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
72		f1ocnv 6776	. . . . . . . . . . . 12 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → ^◡𝐹:𝐴–1-1-onto→𝐶)
73	2, 72	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐹:𝐴–1-1-onto→𝐶)
74		f1ofun 6766	. . . . . . . . . . 11 ⊢ (^◡𝐹:𝐴–1-1-onto→𝐶 → Fun ^◡𝐹)
75	73, 74	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → Fun ^◡𝐹)
76		elinel2 4153	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
77		imafi 9204	. . . . . . . . . 10 ⊢ ((Fun ^◡𝐹 ∧ 𝑦 ∈ Fin) → (^◡𝐹 “ 𝑦) ∈ Fin)
78	75, 76, 77	syl2an 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ Fin)
79	71, 78	elind 4151	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
80	79	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
81		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑘 ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
82	8, 81	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
83		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑘 𝑦 ∈ (𝒫 𝐴 ∩ Fin)
84	82, 83	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
85		nfmpt1 5191	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(𝑛 ∈ 𝐶 ↦ 𝐷)
86	85	nfrn 5894	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛ran (𝑛 ∈ 𝐶 ↦ 𝐷)
87	86	nfel2 2910	. . . . . . . . . . 11 ⊢ Ⅎ𝑛+∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
88	87	nfn 1857	. . . . . . . . . 10 ⊢ Ⅎ𝑛 ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)
89	12, 88	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
90		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑛 𝑦 ∈ (𝒫 𝐴 ∩ Fin)
91	89, 90	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
92	78	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ∈ Fin)
93		f1of1 6763	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶–1-1→𝐴)
94	2, 93	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐶–1-1→𝐴)
95	94	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐶–1-1→𝐴)
96	69	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (^◡𝐹 “ 𝑦) ⊆ 𝐶)
97		f1ores 6778	. . . . . . . . . . 11 ⊢ ((𝐹:𝐶–1-1→𝐴 ∧ (^◡𝐹 “ 𝑦) ⊆ 𝐶) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)))
98	95, 96, 97	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)))
99		elpwinss 45027	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴)
100		foimacnv 6781	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝐹 “ (^◡𝐹 “ 𝑦)) = 𝑦)
101	4, 99, 100	syl2an 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ (^◡𝐹 “ 𝑦)) = 𝑦)
102	101	f1oeq3d 6761	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→(𝐹 “ (^◡𝐹 “ 𝑦)) ↔ (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦))
103	98, 102	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦)
104	103	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ (^◡𝐹 “ 𝑦)):(^◡𝐹 “ 𝑦)–1-1-onto→𝑦)
105	16, 1	fexd 7163	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ V)
106		cnvexg 7857	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ V → ^◡𝐹 ∈ V)
107	105, 106	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ^◡𝐹 ∈ V)
108	107	imaexd 7849	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝐹 “ 𝑦) ∈ V)
109	108	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → (^◡𝐹 “ 𝑦) ∈ V)
110		simpll 766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → 𝜑)
111	79	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
112		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → 𝑛 ∈ (^◡𝐹 “ 𝑦))
113	110, 111, 112	jca31 514	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)))
114		eleq1 2816	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↔ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)))
115	114	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ (𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))))
116		eleq2w2 2725	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑛 ∈ 𝑥 ↔ 𝑛 ∈ (^◡𝐹 “ 𝑦)))
117	115, 116	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) ↔ ((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦))))
118		reseq2 5925	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝐹 ↾ 𝑥) = (𝐹 ↾ (^◡𝐹 “ 𝑦)))
119	118	fveq1d 6824	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((𝐹 ↾ 𝑥)‘𝑛) = ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛))
120	119	eqeq1d 2731	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝐹 ↾ 𝑥)‘𝑛) = 𝐺 ↔ ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺))
121	117, 120	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺) ↔ (((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)))
122		fvres 6841	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑥 → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛))
123	122	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = (𝐹‘𝑛))
124		simpll 766	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝜑)
125		elpwinss 45027	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ⊆ 𝐶)
126	125	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ⊆ 𝐶)
127	126	sselda 3935	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → 𝑛 ∈ 𝐶)
128	124, 127, 18	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → (𝐹‘𝑛) = 𝐺)
129	123, 128	eqtrd 2764	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺)
130	121, 129	vtoclg 3509	. . . . . . . . . 10 ⊢ ((^◡𝐹 “ 𝑦) ∈ V → (((𝜑 ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺))
131	109, 113, 130	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)
132	131	adantllr 719	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑛 ∈ (^◡𝐹 “ 𝑦)) → ((𝐹 ↾ (^◡𝐹 “ 𝑦))‘𝑛) = 𝐺)
133	108	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ V)
134		simpll 766	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)))
135	70	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ 𝒫 𝐶)
136	92	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ Fin)
137	135, 136	elind 4151	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))
138		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑦)
139	101	eqcomd 2735	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 = (𝐹 “ (^◡𝐹 “ 𝑦)))
140	139	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑦 = (𝐹 “ (^◡𝐹 “ 𝑦)))
141	138, 140	eleqtrd 2830	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))
142	141	adantllr 719	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))
143	134, 137, 142	jca31 514	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))))
144	114	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ↔ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin))))
145		imaeq2 6007	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝐹 “ 𝑥) = (𝐹 “ (^◡𝐹 “ 𝑦)))
146	145	eleq2d 2814	. . . . . . . . . . . 12 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (𝑘 ∈ (𝐹 “ 𝑥) ↔ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))))
147	144, 146	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) ↔ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦)))))
148	147	imbi1d 341	. . . . . . . . . 10 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → (((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ) ↔ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ)))
149		rge0ssre 13359	. . . . . . . . . . . 12 ⊢ (0[,)+∞) ⊆ ℝ
150		ax-resscn 11066	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℂ
151	149, 150	sstri 3945	. . . . . . . . . . 11 ⊢ (0[,)+∞) ⊆ ℂ
152		simplll 774	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝜑)
153		simpllr 775	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
154	16	fimassd 6673	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 “ 𝑥) ⊆ 𝐴)
155	154	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → (𝐹 “ 𝑥) ⊆ 𝐴)
156		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ (𝐹 “ 𝑥))
157	155, 156	sseldd 3936	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴)
158	157	adantllr 719	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝑘 ∈ 𝐴)
159		foelcdmi 6884	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐶–onto→𝐴 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
160	4, 159	sylan 580	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
161	160	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → ∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘)
162		nfv 1914	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛 𝑘 ∈ 𝐴
163	89, 162	nfan 1899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴)
164		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛 𝐵 ∈ (0[,)+∞)
165		csbid 3864	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⦋𝑘 / 𝑘⦌𝐵 = 𝐵
166	165	eqcomi 2738	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐵 = ⦋𝑘 / 𝑘⦌𝐵
167	166	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = ⦋𝑘 / 𝑘⦌𝐵)
168		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑛) = 𝑘 → (𝐹‘𝑛) = 𝑘)
169	168	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑛) = 𝑘 → 𝑘 = (𝐹‘𝑛))
170	169	csbeq1d 3855	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑛) = 𝑘 → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
171	170	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋𝑘 / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
172	29	3adant3 1132	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐷)
173	167, 171, 172	3eqtrd 2768	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷)
174	173	3adant1r 1178	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 = 𝐷)
175		0xr 11162	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ ℝ^*
176	175	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 0 ∈ ℝ^*)
177		pnfxr 11169	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ +∞ ∈ ℝ^*
178	177	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ℝ^*)
179	60	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈ (0[,]+∞))
180		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬ 𝐷 ∈ (0[,)+∞))
181	176, 178, 179, 180	eliccnelico 45510	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 = +∞)
182	181	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ = 𝐷)
183		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝑛 ∈ 𝐶)
184	53, 183, 60	elrnmpt1d 5906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
185	184	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → 𝐷 ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
186	182, 185	eqeltrd 2828	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
187	186	adantllr 719	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
188		simpllr 775	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) ∧ ¬ 𝐷 ∈ (0[,)+∞)) → ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷))
189	187, 188	condan 817	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ (0[,)+∞))
190	189	3adant3 1132	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐷 ∈ (0[,)+∞))
191	174, 190	eqeltrd 2828	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑛 ∈ 𝐶 ∧ (𝐹‘𝑛) = 𝑘) → 𝐵 ∈ (0[,)+∞))
192	191	3exp 1119	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞))))
193	192	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (𝑛 ∈ 𝐶 → ((𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞))))
194	163, 164, 193	rexlimd 3236	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → (∃𝑛 ∈ 𝐶 (𝐹‘𝑛) = 𝑘 → 𝐵 ∈ (0[,)+∞)))
195	161, 194	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))
196	152, 153, 158, 195	syl21anc 837	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ (0[,)+∞))
197	151, 196	sselid 3933	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ 𝑥)) → 𝐵 ∈ ℂ)
198	148, 197	vtoclg 3509	. . . . . . . . 9 ⊢ ((^◡𝐹 “ 𝑦) ∈ V → ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ (^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (𝐹 “ (^◡𝐹 “ 𝑦))) → 𝐵 ∈ ℂ))
199	133, 143, 198	sylc 65	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℂ)
200	84, 91, 27, 92, 104, 132, 199	fsumf1of 45555	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷)
201		sumeq1 15596	. . . . . . . 8 ⊢ (𝑥 = (^◡𝐹 “ 𝑦) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷)
202	201	rspceeqv 3600	. . . . . . 7 ⊢ (((^◡𝐹 “ 𝑦) ∈ (𝒫 𝐶 ∩ Fin) ∧ Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ (^◡𝐹 “ 𝑦)𝐷) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
203	80, 200, 202	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∃𝑥 ∈ (𝒫 𝐶 ∩ Fin)Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
204	67, 203	rnmptssrn 45160	. . . . 5 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) ⊆ ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷))
205		sumex 15595	. . . . . . 7 ⊢ Σ𝑛 ∈ 𝑥 𝐷 ∈ V
206	205	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 ∈ V)
207	6, 154	sselpwd 5267	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 “ 𝑥) ∈ 𝒫 𝐴)
208	207	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ 𝒫 𝐴)
209	16	ffund 6656	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝐹)
210		elinel2 4153	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝒫 𝐶 ∩ Fin) → 𝑥 ∈ Fin)
211		imafi 9204	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ Fin) → (𝐹 “ 𝑥) ∈ Fin)
212	209, 210, 211	syl2an 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ Fin)
213	208, 212	elind 4151	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin))
214	213	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin))
215		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑥 ∈ (𝒫 𝐶 ∩ Fin)
216	82, 215	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin))
217		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑛 𝑥 ∈ (𝒫 𝐶 ∩ Fin)
218	89, 217	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑛((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin))
219	210	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → 𝑥 ∈ Fin)
220		f1ores 6778	. . . . . . . . . . 11 ⊢ ((𝐹:𝐶–1-1→𝐴 ∧ 𝑥 ⊆ 𝐶) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
221	94, 125, 220	syl2an 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
222	221	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–1-1-onto→(𝐹 “ 𝑥))
223	129	adantllr 719	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) ∧ 𝑛 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑛) = 𝐺)
224	216, 218, 27, 219, 222, 223, 197	fsumf1of 45555	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵 = Σ𝑛 ∈ 𝑥 𝐷)
225	224	eqcomd 2735	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵)
226		sumeq1 15596	. . . . . . . 8 ⊢ (𝑦 = (𝐹 “ 𝑥) → Σ𝑘 ∈ 𝑦 𝐵 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵)
227	226	rspceeqv 3600	. . . . . . 7 ⊢ (((𝐹 “ 𝑥) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ (𝐹 “ 𝑥)𝐵) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵)
228	214, 225, 227	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) ∧ 𝑥 ∈ (𝒫 𝐶 ∩ Fin)) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑛 ∈ 𝑥 𝐷 = Σ𝑘 ∈ 𝑦 𝐵)
229	206, 228	rnmptssrn 45160	. . . . 5 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷) ⊆ ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵))
230	204, 229	eqssd 3953	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵) = ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷))
231	230	supeq1d 9336	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ^, < ) = sup(ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ^, < ))
232	6	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐴 ∈ V)
233	82, 232, 195	sge0revalmpt 46359	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ^*, < ))
234	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → 𝐶 ∈ 𝑉)
235	89, 234, 189	sge0revalmpt 46359	. . 3 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)) = sup(ran (𝑥 ∈ (𝒫 𝐶 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 𝐷), ℝ^*, < ))
236	231, 233, 235	3eqtr4d 2774	. 2 ⊢ ((𝜑 ∧ ¬ +∞ ∈ ran (𝑛 ∈ 𝐶 ↦ 𝐷)) → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
237	65, 236	pm2.61dan 812	1 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^{^}‘(𝑛 ∈ 𝐶 ↦ 𝐷)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 Ⅎwnf 1783 ∈ wcel 2109 ∃wrex 3053 Vcvv 3436 ⦋csb 3851 ∩ cin 3902 ⊆ wss 3903 𝒫 cpw 4551 ↦ cmpt 5173 ^◡ccnv 5618 ran crn 5620 ↾ cres 5621 “ cima 5622 Fun wfun 6476 ⟶wf 6478 –1-1→wf1 6479 –onto→wfo 6480 –1-1-onto→wf1o 6481 ‘cfv 6482 (class class class)co 7349 Fincfn 8872 supcsup 9330 ℂcc 11007 ℝcr 11008 0cc0 11009 +∞cpnf 11146 ℝ^*cxr 11148 < clt 11149 [,)cico 13250 [,]cicc 13251 Σcsu 15593 Σ^{^}csumge0 46343

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-inf2 9537 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-isom 6491 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-er 8625 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-sup 9332 df-oi 9402 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-n0 12385 df-z 12472 df-uz 12736 df-rp 12894 df-ico 13254 df-icc 13255 df-fz 13411 df-fzo 13558 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-clim 15395 df-sum 15594 df-sumge0 46344

This theorem is referenced by: sge0resrnlem 46384 sge0fodjrnlem 46397 sge0xp 46410 meadjiunlem 46446 isomenndlem 46511 ovnsubaddlem1 46551

W3C validator