Theorem gsumle

Description: A finite sum in an ordered monoid is monotonic. This proof would be much easier in an ordered group, where an inverse element would be available. (Contributed by Thierry Arnoux, 13-Mar-2018)

	Ref	Expression
Hypotheses	gsumle.b	$$⊢B={\mathrm{Base}}_M$$
	gsumle.l	$$⊢\underset{\dot{}}{\le }={\le }_M$$
	gsumle.m	$$⊢\phi \to M\in \mathrm{oMnd}$$
	gsumle.n	$$⊢\phi \to M\in \mathrm{CMnd}$$
	gsumle.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	gsumle.f	$$⊢\phi \to F:A⟶B$$
	gsumle.g	$$⊢\phi \to G:A⟶B$$
	gsumle.c	$$⊢\phi \to F{\underset{\dot{}}{\le }}_{f}G$$
Assertion	gsumle	$$⊢\phi \to \left({\sum }_M,F\right)\underset{\dot{}}{\le }\left({\sum }_M,G\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsumle.b	$$⊢B={\mathrm{Base}}_M$$
2		gsumle.l	$$⊢\underset{\dot{}}{\le }={\le }_M$$
3		gsumle.m	$$⊢\phi \to M\in \mathrm{oMnd}$$
4		gsumle.n	$$⊢\phi \to M\in \mathrm{CMnd}$$
5		gsumle.a	$$⊢\phi \to A\in \mathrm{Fin}$$
6		gsumle.f	$$⊢\phi \to F:A⟶B$$
7		gsumle.g	$$⊢\phi \to G:A⟶B$$
8		gsumle.c	$$⊢\phi \to F{\underset{\dot{}}{\le }}_{f}G$$
9		ssid	$$⊢A\subseteq A$$
10		sseq1	$$⊢a=\varnothing \to \left(a\subseteq A\leftrightarrow \varnothing \subseteq A\right)$$
11	10	anbi2d	$$⊢a=\varnothing \to \left(\left(\phi \wedge a\subseteq A\right)\leftrightarrow \left(\phi \wedge \varnothing \subseteq A\right)\right)$$
12		reseq2	$$⊢a=\varnothing \to {F\upharpoonright }_a={F\upharpoonright }_{\varnothing }$$
13	12	oveq2d	$$⊢a=\varnothing \to {\sum }_M\left({F\upharpoonright }_a\right)={\sum }_M\left({F\upharpoonright }_{\varnothing }\right)$$
14		reseq2	$$⊢a=\varnothing \to {G\upharpoonright }_a={G\upharpoonright }_{\varnothing }$$
15	14	oveq2d	$$⊢a=\varnothing \to {\sum }_M\left({G\upharpoonright }_a\right)={\sum }_M\left({G\upharpoonright }_{\varnothing }\right)$$
16	13 15	breq12d	$$⊢a=\varnothing \to \left(\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_a\right)\right)\leftrightarrow \left({\sum }_M,\left({F\upharpoonright }_{\varnothing }\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_{\varnothing }\right)\right)\right)$$
17	11 16	imbi12d	$$⊢a=\varnothing \to \left(\left(\left(\phi \wedge a\subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_a\right)\right)\right)\leftrightarrow \left(\left(\phi \wedge \varnothing \subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_{\varnothing }\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_{\varnothing }\right)\right)\right)\right)$$
18		sseq1	$$⊢a=e\to \left(a\subseteq A\leftrightarrow e\subseteq A\right)$$
19	18	anbi2d	$$⊢a=e\to \left(\left(\phi \wedge a\subseteq A\right)\leftrightarrow \left(\phi \wedge e\subseteq A\right)\right)$$
20		reseq2	$$⊢a=e\to {F\upharpoonright }_a={F\upharpoonright }_e$$
21	20	oveq2d	$$⊢a=e\to {\sum }_M\left({F\upharpoonright }_a\right)={\sum }_M\left({F\upharpoonright }_e\right)$$
22		reseq2	$$⊢a=e\to {G\upharpoonright }_a={G\upharpoonright }_e$$
23	22	oveq2d	$$⊢a=e\to {\sum }_M\left({G\upharpoonright }_a\right)={\sum }_M\left({G\upharpoonright }_e\right)$$
24	21 23	breq12d	$$⊢a=e\to \left(\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_a\right)\right)\leftrightarrow \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)$$
25	19 24	imbi12d	$$⊢a=e\to \left(\left(\left(\phi \wedge a\subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_a\right)\right)\right)\leftrightarrow \left(\left(\phi \wedge e\subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\right)$$
26		sseq1	$$⊢a=e\cup \left\{y\right\}\to \left(a\subseteq A\leftrightarrow e\cup \left\{y\right\}\subseteq A\right)$$
27	26	anbi2d	$$⊢a=e\cup \left\{y\right\}\to \left(\left(\phi \wedge a\subseteq A\right)\leftrightarrow \left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\right)$$
28		reseq2	$$⊢a=e\cup \left\{y\right\}\to {F\upharpoonright }_a={F\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}$$
29	28	oveq2d	$$⊢a=e\cup \left\{y\right\}\to {\sum }_M\left({F\upharpoonright }_a\right)={\sum }_M\left({F\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)$$
30		reseq2	$$⊢a=e\cup \left\{y\right\}\to {G\upharpoonright }_a={G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}$$
31	30	oveq2d	$$⊢a=e\cup \left\{y\right\}\to {\sum }_M\left({G\upharpoonright }_a\right)={\sum }_M\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)$$
32	29 31	breq12d	$$⊢a=e\cup \left\{y\right\}\to \left(\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_a\right)\right)\leftrightarrow \left({\sum }_M,\left({F\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\right)\right)$$
33	27 32	imbi12d	$$⊢a=e\cup \left\{y\right\}\to \left(\left(\left(\phi \wedge a\subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_a\right)\right)\right)\leftrightarrow \left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\right)\right)\right)$$
34		sseq1	$$⊢a=A\to \left(a\subseteq A\leftrightarrow A\subseteq A\right)$$
35	34	anbi2d	$$⊢a=A\to \left(\left(\phi \wedge a\subseteq A\right)\leftrightarrow \left(\phi \wedge A\subseteq A\right)\right)$$
36		reseq2	$$⊢a=A\to {F\upharpoonright }_a={F\upharpoonright }_A$$
37	36	oveq2d	$$⊢a=A\to {\sum }_M\left({F\upharpoonright }_a\right)={\sum }_M\left({F\upharpoonright }_A\right)$$
38		reseq2	$$⊢a=A\to {G\upharpoonright }_a={G\upharpoonright }_A$$
39	38	oveq2d	$$⊢a=A\to {\sum }_M\left({G\upharpoonright }_a\right)={\sum }_M\left({G\upharpoonright }_A\right)$$
40	37 39	breq12d	$$⊢a=A\to \left(\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_a\right)\right)\leftrightarrow \left({\sum }_M,\left({F\upharpoonright }_A\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_A\right)\right)\right)$$
41	35 40	imbi12d	$$⊢a=A\to \left(\left(\left(\phi \wedge a\subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_a\right)\right)\right)\leftrightarrow \left(\left(\phi \wedge A\subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_A\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_A\right)\right)\right)\right)$$
42		omndtos	$$⊢M\in \mathrm{oMnd}\to M\in \mathrm{Toset}$$
43		tospos	$$⊢M\in \mathrm{Toset}\to M\in \mathrm{Poset}$$
44	3 42 43	3syl	$$⊢\phi \to M\in \mathrm{Poset}$$
45		res0	$$⊢{F\upharpoonright }_{\varnothing }=\varnothing$$
46	45	oveq2i	$$⊢{\sum }_M\left({F\upharpoonright }_{\varnothing }\right)={\sum }_M\varnothing$$
47		eqid	$$⊢0_M=0_M$$
48	47	gsum0	$$⊢{\sum }_M\varnothing =0_M$$
49	46 48	eqtri	$$⊢{\sum }_M\left({F\upharpoonright }_{\varnothing }\right)=0_M$$
50		omndmnd	$$⊢M\in \mathrm{oMnd}\to M\in \mathrm{Mnd}$$
51	1 47	mndidcl	$$⊢M\in \mathrm{Mnd}\to 0_M\in B$$
52	3 50 51	3syl	$$⊢\phi \to 0_M\in B$$
53	49 52	eqeltrid	$$⊢\phi \to {\sum }_M\left({F\upharpoonright }_{\varnothing }\right)\in B$$
54	1 2	posref	$$⊢\left(M\in \mathrm{Poset}\wedge {\sum }_M\left({F\upharpoonright }_{\varnothing }\right)\in B\right)\to \left({\sum }_M,\left({F\upharpoonright }_{\varnothing }\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({F\upharpoonright }_{\varnothing }\right)\right)$$
55	44 53 54	syl2anc	$$⊢\phi \to \left({\sum }_M,\left({F\upharpoonright }_{\varnothing }\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({F\upharpoonright }_{\varnothing }\right)\right)$$
56		res0	$$⊢{G\upharpoonright }_{\varnothing }=\varnothing$$
57	45 56	eqtr4i	$$⊢{F\upharpoonright }_{\varnothing }={G\upharpoonright }_{\varnothing }$$
58	57	oveq2i	$$⊢{\sum }_M\left({F\upharpoonright }_{\varnothing }\right)={\sum }_M\left({G\upharpoonright }_{\varnothing }\right)$$
59	55 58	breqtrdi	$$⊢\phi \to \left({\sum }_M,\left({F\upharpoonright }_{\varnothing }\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_{\varnothing }\right)\right)$$
60	59	adantr	$$⊢\left(\phi \wedge \varnothing \subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_{\varnothing }\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_{\varnothing }\right)\right)$$
61		ssun1	$$⊢e\subseteq e\cup \left\{y\right\}$$
62		sstr2	$$⊢e\subseteq e\cup \left\{y\right\}\to \left(e\cup \left\{y\right\}\subseteq A\to e\subseteq A\right)$$
63	61 62	ax-mp	$$⊢e\cup \left\{y\right\}\subseteq A\to e\subseteq A$$
64	63	anim2i	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to \left(\phi \wedge e\subseteq A\right)$$
65	64	imim1i	$$⊢\left(\left(\phi \wedge e\subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to \left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)$$
66		simplr	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg y\in e\right)\wedge \left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to \left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)$$
67		simpllr	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg y\in e\right)\wedge \left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to \neg y\in e$$
68		simpr	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg y\in e\right)\wedge \left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)$$
69		eqid	$$⊢{+}_M={+}_M$$
70	3	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to M\in \mathrm{oMnd}$$
71	7	ad2antrr	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to G:A⟶B$$
72		simplr	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to e\cup \left\{y\right\}\subseteq A$$
73		ssun2	$$⊢\left\{y\right\}\subseteq e\cup \left\{y\right\}$$
74		vex	$$⊢y\in \mathrm{V}$$
75	74	snss	$$⊢y\in \left(e\cup \left\{y\right\}\right)\leftrightarrow \left\{y\right\}\subseteq e\cup \left\{y\right\}$$
76	73 75	mpbir	$$⊢y\in \left(e\cup \left\{y\right\}\right)$$
77	76	a1i	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to y\in \left(e\cup \left\{y\right\}\right)$$
78	72 77	sseldd	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to y\in A$$
79	71 78	ffvelcdmd	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to G\left(y\right)\in B$$
80	79	adantr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to G\left(y\right)\in B$$
81	4	ad2antrr	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to M\in \mathrm{CMnd}$$
82		vex	$$⊢e\in \mathrm{V}$$
83	82	a1i	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to e\in \mathrm{V}$$
84	6	ad2antrr	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to F:A⟶B$$
85	61 72	sstrid	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to e\subseteq A$$
86	84 85	fssresd	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to \left({F\upharpoonright }_e\right):e⟶B$$
87	5	ad2antrr	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to A\in \mathrm{Fin}$$
88		fvexd	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to 0_M\in \mathrm{V}$$
89	84 87 88	fdmfifsupp	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {finSupp}_{0_M}\left(F\right)$$
90	89 88	fsuppres	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {finSupp}_{0_M}\left(\left({F\upharpoonright }_e\right)\right)$$
91	1 47 81 83 86 90	gsumcl	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {\sum }_M\left({F\upharpoonright }_e\right)\in B$$
92	91	adantr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to {\sum }_M\left({F\upharpoonright }_e\right)\in B$$
93	84 78	ffvelcdmd	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to F\left(y\right)\in B$$
94	93	adantr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to F\left(y\right)\in B$$
95	71 85	fssresd	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to \left({G\upharpoonright }_e\right):e⟶B$$
96		ssfi	$$⊢\left(A\in \mathrm{Fin}\wedge e\subseteq A\right)\to e\in \mathrm{Fin}$$
97	87 85 96	syl2anc	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to e\in \mathrm{Fin}$$
98	95 97 88	fdmfifsupp	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {finSupp}_{0_M}\left(\left({G\upharpoonright }_e\right)\right)$$
99	1 47 81 83 95 98	gsumcl	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {\sum }_M\left({G\upharpoonright }_e\right)\in B$$
100	99	adantr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to {\sum }_M\left({G\upharpoonright }_e\right)\in B$$
101		simpr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)$$
102		simpll	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to \phi$$
103	8	ad2antrr	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to F{\underset{\dot{}}{\le }}_{f}G$$
104	6	ffnd	$$⊢\phi \to FFnA$$
105	7	ffnd	$$⊢\phi \to GFnA$$
106		inidm	$$⊢A\cap A=A$$
107		eqidd	$$⊢\left(\phi \wedge y\in A\right)\to F\left(y\right)=F\left(y\right)$$
108		eqidd	$$⊢\left(\phi \wedge y\in A\right)\to G\left(y\right)=G\left(y\right)$$
109	104 105 5 5 106 107 108	ofrval	$$⊢\left(\phi \wedge F{\underset{\dot{}}{\le }}_{f}G\wedge y\in A\right)\to F\left(y\right)\underset{\dot{}}{\le }G\left(y\right)$$
110	102 103 78 109	syl3anc	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to F\left(y\right)\underset{\dot{}}{\le }G\left(y\right)$$
111	110	adantr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to F\left(y\right)\underset{\dot{}}{\le }G\left(y\right)$$
112	81	adantr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to M\in \mathrm{CMnd}$$
113	1 2 69 70 80 92 94 100 101 111 112	omndadd2d	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to \left(\left({\sum }_M,\left({F\upharpoonright }_e\right)\right){+}_{M}F\left(y\right)\right)\underset{\dot{}}{\le }\left(\left({\sum }_M,\left({G\upharpoonright }_e\right)\right){+}_{M}G\left(y\right)\right)$$
114	97	adantr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to e\in \mathrm{Fin}$$
115	6	ad2antrr	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge z\in e\right)\to F:A⟶B$$
116		simplr	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge z\in e\right)\to e\cup \left\{y\right\}\subseteq A$$
117		elun1	$$⊢z\in e\to z\in \left(e\cup \left\{y\right\}\right)$$
118	117	adantl	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge z\in e\right)\to z\in \left(e\cup \left\{y\right\}\right)$$
119	116 118	sseldd	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge z\in e\right)\to z\in A$$
120	115 119	ffvelcdmd	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge z\in e\right)\to F\left(z\right)\in B$$
121	120	ex	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to \left(z\in e\to F\left(z\right)\in B\right)$$
122	121	ad2antrr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to \left(z\in e\to F\left(z\right)\in B\right)$$
123	122	imp	$$⊢\left(\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\wedge z\in e\right)\to F\left(z\right)\in B$$
124	74	a1i	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to y\in \mathrm{V}$$
125		simplr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to \neg y\in e$$
126		fveq2	$$⊢z=y\to F\left(z\right)=F\left(y\right)$$
127	1 69 112 114 123 124 125 94 126	gsumunsn	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to \underset{z\in e\cup \left\{y\right\}}{{\sum }_M}F\left(z\right)=\left(\underset{z\in e}{{\sum }_M},F\left(z\right)\right){+}_{M}F\left(y\right)$$
128	84 72	feqresmpt	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {F\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}=\left(z\in \left(e\cup \left\{y\right\}\right)⟼F\left(z\right)\right)$$
129	128	oveq2d	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {\sum }_M\left({F\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)=\underset{z\in e\cup \left\{y\right\}}{{\sum }_M}F\left(z\right)$$
130	84 85	feqresmpt	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {F\upharpoonright }_e=\left(z\in e⟼F\left(z\right)\right)$$
131	130	oveq2d	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {\sum }_M\left({F\upharpoonright }_e\right)=\underset{z\in e}{{\sum }_M}F\left(z\right)$$
132	131	oveq1d	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to \left({\sum }_M,\left({F\upharpoonright }_e\right)\right){+}_{M}F\left(y\right)=\left(\underset{z\in e}{{\sum }_M},F\left(z\right)\right){+}_{M}F\left(y\right)$$
133	129 132	eqeq12d	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to \left({\sum }_M\left({F\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)=\left({\sum }_M,\left({F\upharpoonright }_e\right)\right){+}_{M}F\left(y\right)\leftrightarrow \underset{z\in e\cup \left\{y\right\}}{{\sum }_M}F\left(z\right)=\left(\underset{z\in e}{{\sum }_M},F\left(z\right)\right){+}_{M}F\left(y\right)\right)$$
134	133	adantr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to \left({\sum }_M\left({F\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)=\left({\sum }_M,\left({F\upharpoonright }_e\right)\right){+}_{M}F\left(y\right)\leftrightarrow \underset{z\in e\cup \left\{y\right\}}{{\sum }_M}F\left(z\right)=\left(\underset{z\in e}{{\sum }_M},F\left(z\right)\right){+}_{M}F\left(y\right)\right)$$
135	127 134	mpbird	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to {\sum }_M\left({F\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)=\left({\sum }_M,\left({F\upharpoonright }_e\right)\right){+}_{M}F\left(y\right)$$
136	7	adantr	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to G:A⟶B$$
137	136	ad2antrr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge z\in e\right)\to G:A⟶B$$
138	119	adantlr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge z\in e\right)\to z\in A$$
139	137 138	ffvelcdmd	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge z\in e\right)\to G\left(z\right)\in B$$
140	74	a1i	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to y\in \mathrm{V}$$
141		simpr	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to \neg y\in e$$
142		fveq2	$$⊢z=y\to G\left(z\right)=G\left(y\right)$$
143	1 69 81 97 139 140 141 79 142	gsumunsn	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to \underset{z\in e\cup \left\{y\right\}}{{\sum }_M}G\left(z\right)=\left(\underset{z\in e}{{\sum }_M},G\left(z\right)\right){+}_{M}G\left(y\right)$$
144		simpr	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to e\cup \left\{y\right\}\subseteq A$$
145	136 144	feqresmpt	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to {G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}=\left(z\in \left(e\cup \left\{y\right\}\right)⟼G\left(z\right)\right)$$
146	145	oveq2d	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to {\sum }_M\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)=\underset{z\in e\cup \left\{y\right\}}{{\sum }_M}G\left(z\right)$$
147		resabs1	$$⊢e\subseteq e\cup \left\{y\right\}\to {\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_e={G\upharpoonright }_e$$
148	61 147	mp1i	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to {\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_e={G\upharpoonright }_e$$
149	63	adantl	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to e\subseteq A$$
150	136 149	feqresmpt	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to {G\upharpoonright }_e=\left(z\in e⟼G\left(z\right)\right)$$
151	148 150	eqtrd	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to {\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_e=\left(z\in e⟼G\left(z\right)\right)$$
152	151	oveq2d	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to {\sum }_M\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_e\right)=\underset{z\in e}{{\sum }_M}G\left(z\right)$$
153		resabs1	$$⊢\left\{y\right\}\subseteq e\cup \left\{y\right\}\to {\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_{\left\{y\right\}}={G\upharpoonright }_{\left\{y\right\}}$$
154	73 153	mp1i	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to {\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_{\left\{y\right\}}={G\upharpoonright }_{\left\{y\right\}}$$
155	73 144	sstrid	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to \left\{y\right\}\subseteq A$$
156	136 155	feqresmpt	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to {G\upharpoonright }_{\left\{y\right\}}=\left(z\in \left\{y\right\}⟼G\left(z\right)\right)$$
157	154 156	eqtrd	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to {\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_{\left\{y\right\}}=\left(z\in \left\{y\right\}⟼G\left(z\right)\right)$$
158	157	oveq2d	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to {\sum }_M\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_{\left\{y\right\}}\right)=\underset{z\in \left\{y\right\}}{{\sum }_M}G\left(z\right)$$
159	3 50	syl	$$⊢\phi \to M\in \mathrm{Mnd}$$
160	159	adantr	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to M\in \mathrm{Mnd}$$
161	74	a1i	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to y\in \mathrm{V}$$
162	76	a1i	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to y\in \left(e\cup \left\{y\right\}\right)$$
163	144 162	sseldd	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to y\in A$$
164	136 163	ffvelcdmd	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to G\left(y\right)\in B$$
165	142	adantl	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge z=y\right)\to G\left(z\right)=G\left(y\right)$$
166	1 160 161 164 165	gsumsnd	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to \underset{z\in \left\{y\right\}}{{\sum }_M}G\left(z\right)=G\left(y\right)$$
167	158 166	eqtrd	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to {\sum }_M\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_{\left\{y\right\}}\right)=G\left(y\right)$$
168	152 167	oveq12d	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to \left({\sum }_M,\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_e\right)\right){+}_M\left({\sum }_M,\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_{\left\{y\right\}}\right)\right)=\left(\underset{z\in e}{{\sum }_M},G\left(z\right)\right){+}_{M}G\left(y\right)$$
169	146 168	eqeq12d	$$⊢\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to \left({\sum }_M\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)=\left({\sum }_M,\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_e\right)\right){+}_M\left({\sum }_M,\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_{\left\{y\right\}}\right)\right)\leftrightarrow \underset{z\in e\cup \left\{y\right\}}{{\sum }_M}G\left(z\right)=\left(\underset{z\in e}{{\sum }_M},G\left(z\right)\right){+}_{M}G\left(y\right)\right)$$
170	169	adantr	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to \left({\sum }_M\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)=\left({\sum }_M,\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_e\right)\right){+}_M\left({\sum }_M,\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_{\left\{y\right\}}\right)\right)\leftrightarrow \underset{z\in e\cup \left\{y\right\}}{{\sum }_M}G\left(z\right)=\left(\underset{z\in e}{{\sum }_M},G\left(z\right)\right){+}_{M}G\left(y\right)\right)$$
171	143 170	mpbird	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {\sum }_M\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)=\left({\sum }_M,\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_e\right)\right){+}_M\left({\sum }_M,\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_{\left\{y\right\}}\right)\right)$$
172	61 147	ax-mp	$$⊢{\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_e={G\upharpoonright }_e$$
173	172	oveq2i	$$⊢{\sum }_M\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_e\right)={\sum }_M\left({G\upharpoonright }_e\right)$$
174	73 153	ax-mp	$$⊢{\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_{\left\{y\right\}}={G\upharpoonright }_{\left\{y\right\}}$$
175	174	oveq2i	$$⊢{\sum }_M\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_{\left\{y\right\}}\right)={\sum }_M\left({G\upharpoonright }_{\left\{y\right\}}\right)$$
176	173 175	oveq12i	$$⊢\left({\sum }_M,\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_e\right)\right){+}_M\left({\sum }_M,\left({\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\upharpoonright }_{\left\{y\right\}}\right)\right)=\left({\sum }_M,\left({G\upharpoonright }_e\right)\right){+}_M\left({\sum }_M,\left({G\upharpoonright }_{\left\{y\right\}}\right)\right)$$
177	171 176	eqtrdi	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {\sum }_M\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)=\left({\sum }_M,\left({G\upharpoonright }_e\right)\right){+}_M\left({\sum }_M,\left({G\upharpoonright }_{\left\{y\right\}}\right)\right)$$
178	73 72	sstrid	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to \left\{y\right\}\subseteq A$$
179	71 178	feqresmpt	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {G\upharpoonright }_{\left\{y\right\}}=\left(x\in \left\{y\right\}⟼G\left(x\right)\right)$$
180	179	oveq2d	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {\sum }_M\left({G\upharpoonright }_{\left\{y\right\}}\right)=\underset{x\in \left\{y\right\}}{{\sum }_M}G\left(x\right)$$
181		cmnmnd	$$⊢M\in \mathrm{CMnd}\to M\in \mathrm{Mnd}$$
182	81 181	syl	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to M\in \mathrm{Mnd}$$
183		fveq2	$$⊢x=y\to G\left(x\right)=G\left(y\right)$$
184	1 183	gsumsn	$$⊢\left(M\in \mathrm{Mnd}\wedge y\in \mathrm{V}\wedge G\left(y\right)\in B\right)\to \underset{x\in \left\{y\right\}}{{\sum }_M}G\left(x\right)=G\left(y\right)$$
185	182 140 79 184	syl3anc	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to \underset{x\in \left\{y\right\}}{{\sum }_M}G\left(x\right)=G\left(y\right)$$
186	180 185	eqtrd	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {\sum }_M\left({G\upharpoonright }_{\left\{y\right\}}\right)=G\left(y\right)$$
187	186	oveq2d	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to \left({\sum }_M,\left({G\upharpoonright }_e\right)\right){+}_M\left({\sum }_M,\left({G\upharpoonright }_{\left\{y\right\}}\right)\right)=\left({\sum }_M,\left({G\upharpoonright }_e\right)\right){+}_{M}G\left(y\right)$$
188	177 187	eqtrd	$$⊢\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\to {\sum }_M\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)=\left({\sum }_M,\left({G\upharpoonright }_e\right)\right){+}_{M}G\left(y\right)$$
189	188	adantr	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to {\sum }_M\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)=\left({\sum }_M,\left({G\upharpoonright }_e\right)\right){+}_{M}G\left(y\right)$$
190	113 135 189	3brtr4d	$$⊢\left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\wedge \neg y\in e\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to \left({\sum }_M,\left({F\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\right)$$
191	66 67 68 190	syl21anc	$$⊢\left(\left(\left(e\in \mathrm{Fin}\wedge \neg y\in e\right)\wedge \left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\right)\wedge \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to \left({\sum }_M,\left({F\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\right)$$
192	191	exp31	$$⊢\left(e\in \mathrm{Fin}\wedge \neg y\in e\right)\to \left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to \left(\left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\to \left({\sum }_M,\left({F\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\right)\right)\right)$$
193	192	a2d	$$⊢\left(e\in \mathrm{Fin}\wedge \neg y\in e\right)\to \left(\left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to \left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\right)\right)\right)$$
194	65 193	syl5	$$⊢\left(e\in \mathrm{Fin}\wedge \neg y\in e\right)\to \left(\left(\left(\phi \wedge e\subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_e\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_e\right)\right)\right)\to \left(\left(\phi \wedge e\cup \left\{y\right\}\subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_{\left(e\cup \left\{y\right\}\right)}\right)\right)\right)\right)$$
195	17 25 33 41 60 194	findcard2s	$$⊢A\in \mathrm{Fin}\to \left(\left(\phi \wedge A\subseteq A\right)\to \left({\sum }_M,\left({F\upharpoonright }_A\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_A\right)\right)\right)$$
196	195	imp	$$⊢\left(A\in \mathrm{Fin}\wedge \left(\phi \wedge A\subseteq A\right)\right)\to \left({\sum }_M,\left({F\upharpoonright }_A\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_A\right)\right)$$
197	9 196	mpanr2	$$⊢\left(A\in \mathrm{Fin}\wedge \phi \right)\to \left({\sum }_M,\left({F\upharpoonright }_A\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_A\right)\right)$$
198	5 197	mpancom	$$⊢\phi \to \left({\sum }_M,\left({F\upharpoonright }_A\right)\right)\underset{\dot{}}{\le }\left({\sum }_M,\left({G\upharpoonright }_A\right)\right)$$
199		fnresdm	$$⊢FFnA\to {F\upharpoonright }_A=F$$
200	104 199	syl	$$⊢\phi \to {F\upharpoonright }_A=F$$
201	200	oveq2d	$$⊢\phi \to {\sum }_M\left({F\upharpoonright }_A\right)={\sum }_{M}F$$
202		fnresdm	$$⊢GFnA\to {G\upharpoonright }_A=G$$
203	105 202	syl	$$⊢\phi \to {G\upharpoonright }_A=G$$
204	203	oveq2d	$$⊢\phi \to {\sum }_M\left({G\upharpoonright }_A\right)={\sum }_{M}G$$
205	198 201 204	3brtr3d	$$⊢\phi \to \left({\sum }_M,F\right)\underset{\dot{}}{\le }\left({\sum }_M,G\right)$$