Theorem tsmsxplem1 24109

Description: Lemma for tsmsxp 24111. (Contributed by Mario Carneiro, 21-Sep-2015.)

Hypotheses

Ref	Expression
tsmsxp.b	⊢ 𝐵 = (Base‘𝐺)
tsmsxp.g	⊢ (𝜑 → 𝐺 ∈ CMnd)
tsmsxp.2	⊢ (𝜑 → 𝐺 ∈ TopGrp)
tsmsxp.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
tsmsxp.c	⊢ (𝜑 → 𝐶 ∈ 𝑊)
tsmsxp.f	⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵)
tsmsxp.h	⊢ (𝜑 → 𝐻:𝐴⟶𝐵)
tsmsxp.1	⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))
tsmsxp.j	⊢ 𝐽 = (TopOpen‘𝐺)
tsmsxp.z	⊢ 0 = (0g‘𝐺)
tsmsxp.p	⊢ + = (+g‘𝐺)
tsmsxp.m	⊢ − = (-g‘𝐺)
tsmsxp.l	⊢ (𝜑 → 𝐿 ∈ 𝐽)
tsmsxp.3	⊢ (𝜑 → 0 ∈ 𝐿)
tsmsxp.k	⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐴 ∩ Fin))
tsmsxp.ks	⊢ (𝜑 → dom 𝐷 ⊆ 𝐾)
tsmsxp.d	⊢ (𝜑 → 𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))

Assertion

Ref	Expression
tsmsxplem1	⊢ (𝜑 → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))

Distinct variable groups:   0 ,𝑘   𝑗,𝑘,𝑛,𝑥,𝐺   𝐵,𝑘   𝐷,𝑗,𝑘,𝑛,𝑥   𝑗,𝐿,𝑛,𝑥   𝐴,𝑗,𝑘,𝑛   𝑗,𝐾,𝑘,𝑛,𝑥   𝑗,𝐻,𝑘,𝑛,𝑥   − ,𝑗,𝑛,𝑥   𝐶,𝑗,𝑘,𝑛   𝑗,𝐹,𝑘,𝑛,𝑥   𝜑,𝑗,𝑘,𝑛

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)   𝐵(𝑥,𝑗,𝑛)   𝐶(𝑥)   + (𝑥,𝑗,𝑘,𝑛)   𝐽(𝑥,𝑗,𝑘,𝑛)   𝐿(𝑘)   − (𝑘)   𝑉(𝑥,𝑗,𝑘,𝑛)   𝑊(𝑥,𝑗,𝑘,𝑛)   0 (𝑥,𝑗,𝑛)

Proof of Theorem tsmsxplem1

Dummy variables 𝑔 𝑦 𝑧 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tsmsxp.k	. . . 4 ⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐴 ∩ Fin))
2	1	elin2d 4159	. . 3 ⊢ (𝜑 → 𝐾 ∈ Fin)
3		elfpw 9266	. . . . . . . 8 ⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐾 ⊆ 𝐴 ∧ 𝐾 ∈ Fin))
4	3	simplbi 496	. . . . . . 7 ⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ⊆ 𝐴)
5	1, 4	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐾 ⊆ 𝐴)
6	5	sselda 3935	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → 𝑗 ∈ 𝐴)
7		tsmsxp.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐺)
8		tsmsxp.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘𝐺)
9		eqid 2737	. . . . . 6 ⊢ (𝒫 𝐶 ∩ Fin) = (𝒫 𝐶 ∩ Fin)
10		tsmsxp.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ CMnd)
11	10	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ CMnd)
12		tsmsxp.2	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ TopGrp)
13		tgptps 24036	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
14	12, 13	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ TopSp)
15	14	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ TopSp)
16		tsmsxp.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑊)
17	16	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊)
18		tsmsxp.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵)
19		fovcdm 7538	. . . . . . . . 9 ⊢ ((𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
20	18, 19	syl3an1 1164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
21	20	3expa 1119	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
22	21	fmpttd 7069	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)):𝐶⟶𝐵)
23		tsmsxp.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ (𝐺 tsums (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘))))
24		df-ima 5645	. . . . . . . 8 ⊢ ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) = ran ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿)
25	8, 7	tgptopon 24038	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝐵))
26	12, 25	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵))
27		tsmsxp.l	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ 𝐽)
28		toponss 22883	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐿 ∈ 𝐽) → 𝐿 ⊆ 𝐵)
29	26, 27, 28	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ⊆ 𝐵)
30	29	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐿 ⊆ 𝐵)
31	30	resmptd 6007	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) = (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
32	31	rneqd 5895	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ran ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ↾ 𝐿) = ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
33	24, 32	eqtrid 2784	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) = ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
34		tsmsxp.h	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻:𝐴⟶𝐵)
35	34	ffvelcdmda 7038	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ 𝐵)
36		tsmsxp.p	. . . . . . . . . . . . 13 ⊢ + = (+g‘𝐺)
37		eqid 2737	. . . . . . . . . . . . 13 ⊢ (invg‘𝐺) = (invg‘𝐺)
38		tsmsxp.m	. . . . . . . . . . . . 13 ⊢ − = (-g‘𝐺)
39	7, 36, 37, 38	grpsubval 18927	. . . . . . . . . . . 12 ⊢ (((𝐻‘𝑗) ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔)))
40	35, 39	sylan 581	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔)))
41	40	mpteq2dva 5193	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) = (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔))))
42		tgpgrp 24034	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
43	12, 42	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ∈ Grp)
44	43	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ Grp)
45	7, 37	grpinvcl 18929	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵) → ((invg‘𝐺)‘𝑔) ∈ 𝐵)
46	44, 45	sylan 581	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((invg‘𝐺)‘𝑔) ∈ 𝐵)
47	7, 37	grpinvf 18928	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ Grp → (invg‘𝐺):𝐵⟶𝐵)
48	44, 47	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺):𝐵⟶𝐵)
49	48	feqmptd 6910	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺) = (𝑔 ∈ 𝐵 ↦ ((invg‘𝐺)‘𝑔)))
50		eqidd 2738	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)))
51		oveq2 7376	. . . . . . . . . . 11 ⊢ (𝑦 = ((invg‘𝐺)‘𝑔) → ((𝐻‘𝑗) + 𝑦) = ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔)))
52	46, 49, 50, 51	fmptco 7084	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) = (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) + ((invg‘𝐺)‘𝑔))))
53	41, 52	eqtr4d 2775	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) = ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)))
54	12	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐺 ∈ TopGrp)
55	8, 37	grpinvhmeo 24042	. . . . . . . . . . 11 ⊢ (𝐺 ∈ TopGrp → (invg‘𝐺) ∈ (𝐽Homeo𝐽))
56	54, 55	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (invg‘𝐺) ∈ (𝐽Homeo𝐽))
57		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) = (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦))
58	57, 7, 36, 8	tgplacthmeo 24059	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ TopGrp ∧ (𝐻‘𝑗) ∈ 𝐵) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
59	54, 35, 58	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽))
60		hmeoco 23728	. . . . . . . . . 10 ⊢ (((invg‘𝐺) ∈ (𝐽Homeo𝐽) ∧ (𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∈ (𝐽Homeo𝐽)) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽))
61	56, 59, 60	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑦 ∈ 𝐵 ↦ ((𝐻‘𝑗) + 𝑦)) ∘ (invg‘𝐺)) ∈ (𝐽Homeo𝐽))
62	53, 61	eqeltrd 2837	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ (𝐽Homeo𝐽))
63	27	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐿 ∈ 𝐽)
64		hmeoima 23721	. . . . . . . 8 ⊢ (((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ (𝐽Homeo𝐽) ∧ 𝐿 ∈ 𝐽) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) ∈ 𝐽)
65	62, 63, 64	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝑔 ∈ 𝐵 ↦ ((𝐻‘𝑗) − 𝑔)) “ 𝐿) ∈ 𝐽)
66	33, 65	eqeltrrd 2838	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ∈ 𝐽)
67		tsmsxp.z	. . . . . . . . 9 ⊢ 0 = (0g‘𝐺)
68	7, 67, 38	grpsubid1 18967	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝐻‘𝑗) ∈ 𝐵) → ((𝐻‘𝑗) − 0 ) = (𝐻‘𝑗))
69	44, 35, 68	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐻‘𝑗) − 0 ) = (𝐻‘𝑗))
70		tsmsxp.3	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ 𝐿)
71	70	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 0 ∈ 𝐿)
72		ovex 7401	. . . . . . . 8 ⊢ ((𝐻‘𝑗) − 0 ) ∈ V
73		eqid 2737	. . . . . . . . 9 ⊢ (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) = (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))
74		oveq2 7376	. . . . . . . . 9 ⊢ (𝑔 = 0 → ((𝐻‘𝑗) − 𝑔) = ((𝐻‘𝑗) − 0 ))
75	73, 74	elrnmpt1s 5916	. . . . . . . 8 ⊢ (( 0 ∈ 𝐿 ∧ ((𝐻‘𝑗) − 0 ) ∈ V) → ((𝐻‘𝑗) − 0 ) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
76	71, 72, 75	sylancl 587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ((𝐻‘𝑗) − 0 ) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
77	69, 76	eqeltrrd 2838	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐻‘𝑗) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))
78	7, 8, 9, 11, 15, 17, 22, 23, 66, 77	tsmsi 24090	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
79	6, 78	syldan 592	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
80	79	ralrimiva 3130	. . 3 ⊢ (𝜑 → ∀𝑗 ∈ 𝐾 ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
81		sseq1 3961	. . . . . 6 ⊢ (𝑦 = (𝑓‘𝑗) → (𝑦 ⊆ 𝑧 ↔ (𝑓‘𝑗) ⊆ 𝑧))
82	81	imbi1d 341	. . . . 5 ⊢ (𝑦 = (𝑓‘𝑗) → ((𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ ((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
83	82	ralbidv 3161	. . . 4 ⊢ (𝑦 = (𝑓‘𝑗) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
84	83	ac6sfi 9196	. . 3 ⊢ ((𝐾 ∈ Fin ∧ ∀𝑗 ∈ 𝐾 ∃𝑦 ∈ (𝒫 𝐶 ∩ Fin)∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))) → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
85	2, 80, 84	syl2anc 585	. 2 ⊢ (𝜑 → ∃𝑓(𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)))))
86		frn 6677	. . . . . . . . 9 ⊢ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
87	86	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ (𝒫 𝐶 ∩ Fin))
88		inss1 4191	. . . . . . . 8 ⊢ (𝒫 𝐶 ∩ Fin) ⊆ 𝒫 𝐶
89	87, 88	sstrdi 3948	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ 𝒫 𝐶)
90		sspwuni 5057	. . . . . . 7 ⊢ (ran 𝑓 ⊆ 𝒫 𝐶 ↔ ∪ ran 𝑓 ⊆ 𝐶)
91	89, 90	sylib 218	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ∪ ran 𝑓 ⊆ 𝐶)
92		tsmsxp.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin))
93		elfpw 9266	. . . . . . . . . 10 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) ↔ (𝐷 ⊆ (𝐴 × 𝐶) ∧ 𝐷 ∈ Fin))
94	93	simplbi 496	. . . . . . . . 9 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ⊆ (𝐴 × 𝐶))
95		rnss 5896	. . . . . . . . 9 ⊢ (𝐷 ⊆ (𝐴 × 𝐶) → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
96	92, 94, 95	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ran 𝐷 ⊆ ran (𝐴 × 𝐶))
97		rnxpss 6138	. . . . . . . 8 ⊢ ran (𝐴 × 𝐶) ⊆ 𝐶
98	96, 97	sstrdi 3948	. . . . . . 7 ⊢ (𝜑 → ran 𝐷 ⊆ 𝐶)
99	98	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ⊆ 𝐶)
100	91, 99	unssd 4146	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
101	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐾 ∈ Fin)
102		ffn 6670	. . . . . . . . . 10 ⊢ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) → 𝑓 Fn 𝐾)
103	102	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓 Fn 𝐾)
104		dffn4 6760	. . . . . . . . 9 ⊢ (𝑓 Fn 𝐾 ↔ 𝑓:𝐾–onto→ran 𝑓)
105	103, 104	sylib 218	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑓:𝐾–onto→ran 𝑓)
106		fofi 9225	. . . . . . . 8 ⊢ ((𝐾 ∈ Fin ∧ 𝑓:𝐾–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
107	101, 105, 106	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ∈ Fin)
108		inss2 4192	. . . . . . . 8 ⊢ (𝒫 𝐶 ∩ Fin) ⊆ Fin
109	87, 108	sstrdi 3948	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝑓 ⊆ Fin)
110		unifi 9256	. . . . . . 7 ⊢ ((ran 𝑓 ∈ Fin ∧ ran 𝑓 ⊆ Fin) → ∪ ran 𝑓 ∈ Fin)
111	107, 109, 110	syl2anc 585	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ∪ ran 𝑓 ∈ Fin)
112		elinel2 4156	. . . . . . . 8 ⊢ (𝐷 ∈ (𝒫 (𝐴 × 𝐶) ∩ Fin) → 𝐷 ∈ Fin)
113		rnfi 9252	. . . . . . . 8 ⊢ (𝐷 ∈ Fin → ran 𝐷 ∈ Fin)
114	92, 112, 113	3syl 18	. . . . . . 7 ⊢ (𝜑 → ran 𝐷 ∈ Fin)
115	114	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ran 𝐷 ∈ Fin)
116		unfi 9107	. . . . . 6 ⊢ ((∪ ran 𝑓 ∈ Fin ∧ ran 𝐷 ∈ Fin) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
117	111, 115, 116	syl2anc 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
118		elfpw 9266	. . . . 5 ⊢ ((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ↔ ((∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶 ∧ (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin))
119	100, 117, 118	sylanbrc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
120	119	adantrr 718	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
121		ssun2 4133	. . . 4 ⊢ ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
122	121	a1i 11	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷))
123	119	adantlr 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin))
124		fvssunirn 6873	. . . . . . . . . . . . . 14 ⊢ (𝑓‘𝑗) ⊆ ∪ ran 𝑓
125		ssun1 4132	. . . . . . . . . . . . . 14 ⊢ ∪ ran 𝑓 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
126	124, 125	sstri 3945	. . . . . . . . . . . . 13 ⊢ (𝑓‘𝑗) ⊆ (∪ ran 𝑓 ∪ ran 𝐷)
127		id 22	. . . . . . . . . . . . 13 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → 𝑧 = (∪ ran 𝑓 ∪ ran 𝐷))
128	126, 127	sseqtrrid 3979	. . . . . . . . . . . 12 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝑓‘𝑗) ⊆ 𝑧)
129		pm5.5 361	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑗) ⊆ 𝑧 → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
130	128, 129	syl 17	. . . . . . . . . . 11 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
131		reseq2 5941	. . . . . . . . . . . . 13 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧) = ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷)))
132	131	oveq2d 7384	. . . . . . . . . . . 12 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) = (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))))
133	132	eleq1d 2822	. . . . . . . . . . 11 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → ((𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
134	130, 133	bitrd 279	. . . . . . . . . 10 ⊢ (𝑧 = (∪ ran 𝑓 ∪ ran 𝐷) → (((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) ↔ (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
135	134	rspcv 3574	. . . . . . . . 9 ⊢ ((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
136	123, 135	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
137	10	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ CMnd)
138		cmnmnd 19738	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
139	137, 138	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐺 ∈ Mnd)
140		simplr 769	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗 ∈ 𝐾)
141	117	adantlr 716	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin)
142	100	adantlr 716	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶)
143	142	sselda 3935	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → 𝑘 ∈ 𝐶)
144	18	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
145	144, 6	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → (𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴))
146	19	3expa 1119	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:(𝐴 × 𝐶)⟶𝐵 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
147	145, 146	sylan 581	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
148	147	adantlr 716	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ 𝐶) → (𝑗𝐹𝑘) ∈ 𝐵)
149	143, 148	syldan 592	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ 𝐵)
150	149	fmpttd 7069	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)):(∪ ran 𝑓 ∪ ran 𝐷)⟶𝐵)
151		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))
152		ovexd 7403	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑗𝐹𝑘) ∈ V)
153	67	fvexi 6856	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
154	153	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 0 ∈ V)
155	151, 141, 152, 154	fsuppmptdm 9291	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)) finSupp 0 )
156	7, 67, 137, 141, 150, 155	gsumcl 19856	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
157		velsn 4598	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑗} ↔ 𝑦 = 𝑗)
158		ovres 7534	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ {𝑗} ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
159	157, 158	sylanbr 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑦𝐹𝑘))
160		oveq1 7375	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑗 → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
161	160	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦𝐹𝑘) = (𝑗𝐹𝑘))
162	159, 161	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = 𝑗 ∧ 𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷)) → (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘) = (𝑗𝐹𝑘))
163	162	mpteq2dva 5193	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑗 → (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
164	163	oveq2d 7384	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑗 → (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
165	7, 164	gsumsn 19895	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Mnd ∧ 𝑗 ∈ 𝐾 ∧ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
166	139, 140, 156, 165	syl3anc 1374	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
167		snfi 8992	. . . . . . . . . . . . 13 ⊢ {𝑗} ∈ Fin
168	167	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ∈ Fin)
169	18	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐹:(𝐴 × 𝐶)⟶𝐵)
170	6	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝑗 ∈ 𝐴)
171	170	snssd 4767	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → {𝑗} ⊆ 𝐴)
172		xpss12 5647	. . . . . . . . . . . . . 14 ⊢ (({𝑗} ⊆ 𝐴 ∧ (∪ ran 𝑓 ∪ ran 𝐷) ⊆ 𝐶) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
173	171, 142, 172	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ⊆ (𝐴 × 𝐶))
174	169, 173	fssresd 6709	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))):({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))⟶𝐵)
175		xpfi 9232	. . . . . . . . . . . . . 14 ⊢ (({𝑗} ∈ Fin ∧ (∪ ran 𝑓 ∪ ran 𝐷) ∈ Fin) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
176	167, 141, 175	sylancr 588	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) ∈ Fin)
177	174, 176, 154	fdmfifsupp 9290	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))) finSupp 0 )
178	7, 67, 137, 168, 141, 174, 177	gsumxp 19917	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝑦 ∈ {𝑗} ↦ (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑦(𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))𝑘))))))
179	142	resmptd 6007	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷)) = (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘)))
180	179	oveq2d 7384	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝑘 ∈ (∪ ran 𝑓 ∪ ran 𝐷) ↦ (𝑗𝐹𝑘))))
181	166, 178, 180	3eqtr4rd 2783	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))))
182	181	eleq1d 2822	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))
183		ovex 7401	. . . . . . . . . . 11 ⊢ ((𝐻‘𝑗) − 𝑔) ∈ V
184	73, 183	elrnmpti 5919	. . . . . . . . . 10 ⊢ ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) ↔ ∃𝑔 ∈ 𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔))
185		isabl 19725	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
186	43, 10, 185	sylanbrc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ Abel)
187	186	ad3antrrr 731	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝐺 ∈ Abel)
188	6, 35	syldan 592	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾) → (𝐻‘𝑗) ∈ 𝐵)
189	188	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → (𝐻‘𝑗) ∈ 𝐵)
190	29	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → 𝐿 ⊆ 𝐵)
191	190	sselda 3935	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ 𝐵)
192	7, 38, 187, 189, 191	ablnncan 19761	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) = 𝑔)
193		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → 𝑔 ∈ 𝐿)
194	192, 193	eqeltrd 2837	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) ∈ 𝐿)
195		oveq2 7376	. . . . . . . . . . . . 13 ⊢ ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) = ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)))
196	195	eleq1d 2822	. . . . . . . . . . . 12 ⊢ ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → (((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻‘𝑗) − ((𝐻‘𝑗) − 𝑔)) ∈ 𝐿))
197	194, 196	syl5ibrcom 247	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑔 ∈ 𝐿) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
198	197	rexlimdva 3139	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∃𝑔 ∈ 𝐿 (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = ((𝐻‘𝑗) − 𝑔) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
199	184, 198	biimtrid 242	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
200	182, 199	sylbid 240	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → ((𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ (∪ ran 𝑓 ∪ ran 𝐷))) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔)) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
201	136, 200	syld 47	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐾) ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
202	201	an32s 653	. . . . . 6 ⊢ (((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) ∧ 𝑗 ∈ 𝐾) → (∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
203	202	ralimdva 3150	. . . . 5 ⊢ ((𝜑 ∧ 𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin)) → (∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))) → ∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
204	203	impr 454	. . . 4 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
205		fveq2 6842	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝐻‘𝑗) = (𝐻‘𝑥))
206		sneq 4592	. . . . . . . . . 10 ⊢ (𝑗 = 𝑥 → {𝑗} = {𝑥})
207	206	xpeq1d 5661	. . . . . . . . 9 ⊢ (𝑗 = 𝑥 → ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)) = ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))
208	207	reseq2d 5946	. . . . . . . 8 ⊢ (𝑗 = 𝑥 → (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))) = (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))
209	208	oveq2d 7384	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷)))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))))
210	205, 209	oveq12d 7386	. . . . . 6 ⊢ (𝑗 = 𝑥 → ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) = ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))))
211	210	eleq1d 2822	. . . . 5 ⊢ (𝑗 = 𝑥 → (((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
212	211	cbvralvw 3216	. . . 4 ⊢ (∀𝑗 ∈ 𝐾 ((𝐻‘𝑗) − (𝐺 Σg (𝐹 ↾ ({𝑗} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿 ↔ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
213	204, 212	sylib 218	. . 3 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)
214		sseq2 3962	. . . . 5 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (ran 𝐷 ⊆ 𝑛 ↔ ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷)))
215		xpeq2 5653	. . . . . . . . . 10 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → ({𝑥} × 𝑛) = ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))
216	215	reseq2d 5946	. . . . . . . . 9 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐹 ↾ ({𝑥} × 𝑛)) = (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))
217	216	oveq2d 7384	. . . . . . . 8 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛))) = (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷)))))
218	217	oveq2d 7384	. . . . . . 7 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) = ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))))
219	218	eleq1d 2822	. . . . . 6 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
220	219	ralbidv 3161	. . . . 5 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → (∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿 ↔ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿))
221	214, 220	anbi12d 633	. . . 4 ⊢ (𝑛 = (∪ ran 𝑓 ∪ ran 𝐷) → ((ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿) ↔ (ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)))
222	221	rspcev 3578	. . 3 ⊢ (((∪ ran 𝑓 ∪ ran 𝐷) ∈ (𝒫 𝐶 ∩ Fin) ∧ (ran 𝐷 ⊆ (∪ ran 𝑓 ∪ ran 𝐷) ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × (∪ ran 𝑓 ∪ ran 𝐷))))) ∈ 𝐿)) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
223	120, 122, 213, 222	syl12anc 837	. 2 ⊢ ((𝜑 ∧ (𝑓:𝐾⟶(𝒫 𝐶 ∩ Fin) ∧ ∀𝑗 ∈ 𝐾 ∀𝑧 ∈ (𝒫 𝐶 ∩ Fin)((𝑓‘𝑗) ⊆ 𝑧 → (𝐺 Σg ((𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)) ↾ 𝑧)) ∈ ran (𝑔 ∈ 𝐿 ↦ ((𝐻‘𝑗) − 𝑔))))) → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))
224	85, 223	exlimddv 1937	1 ⊢ (𝜑 → ∃𝑛 ∈ (𝒫 𝐶 ∩ Fin)(ran 𝐷 ⊆ 𝑛 ∧ ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑛)))) ∈ 𝐿))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  Vcvv 3442   ∪ cun 3901   ∩ cin 3902   ⊆ wss 3903  𝒫 cpw 4556  {csn 4582  ∪ cuni 4865   ↦ cmpt 5181   × cxp 5630  dom cdm 5632  ran crn 5633   ↾ cres 5634   “ cima 5635   ∘ ccom 5636   Fn wfn 6495  ⟶wf 6496  –onto→wfo 6498  ‘cfv 6500  (class class class)co 7368  Fincfn 8895  Basecbs 17148  +_gcplusg 17189  TopOpenctopn 17353  0_gc0g 17371   Σ_g cgsu 17372  Mndcmnd 18671  Grpcgrp 18875  inv_gcminusg 18876  -_gcsg 18877  CMndccmn 19721  Abelcabl 19722  TopOnctopon 22866  TopSpctps 22888  Homeochmeo 23709  TopGrpctgp 24027   tsums ctsu 24082

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-iin 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-of 7632  df-om 7819  df-1st 7943  df-2nd 7944  df-supp 8113  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-2o 8408  df-er 8645  df-map 8777  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9277  df-oi 9427  df-card 9863  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-2 12220  df-n0 12414  df-z 12501  df-uz 12764  df-fz 13436  df-fzo 13583  df-seq 13937  df-hash 14266  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17149  df-ress 17170  df-plusg 17202  df-0g 17373  df-gsum 17374  df-topgen 17375  df-mre 17517  df-mrc 17518  df-acs 17520  df-plusf 18576  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-submnd 18721  df-grp 18878  df-minusg 18879  df-sbg 18880  df-mulg 19010  df-cntz 19258  df-cmn 19723  df-abl 19724  df-fbas 21318  df-fg 21319  df-top 22850  df-topon 22867  df-topsp 22889  df-bases 22902  df-ntr 22976  df-nei 23054  df-cn 23183  df-cnp 23184  df-tx 23518  df-hmeo 23711  df-fil 23802  df-fm 23894  df-flim 23895  df-flf 23896  df-tmd 24028  df-tgp 24029  df-tsms 24083

This theorem is referenced by:  tsmsxp  24111