imasdsf1olem

Description: Lemma for imasdsf1o . (Contributed by Mario Carneiro, 21-Aug-2015) (Proof shortened by AV, 6-Oct-2020)

	Ref	Expression
Hypotheses	imasdsf1o.u	$⊢ φ \to U = F “_{𝑠} R$
	imasdsf1o.v	$⊢ φ \to V = {Base}_{R}$
	imasdsf1o.f	$⊢ φ \to F : V \underset{1-1 onto}{⟶} B$
	imasdsf1o.r	$⊢ φ \to R \in Z$
	imasdsf1o.e	$⊢ E = {dist (R) ↾}_{(V \times V)}$
	imasdsf1o.d	$⊢ D = dist (U)$
	imasdsf1o.m	$⊢ φ \to E \in ∞Met (V)$
	imasdsf1o.x	$⊢ φ \to X \in V$
	imasdsf1o.y	$⊢ φ \to Y \in V$
	imasdsf1o.w	$⊢ W = ℝ_{𝑠}^{} ↾_{𝑠} (ℝ^{} ∖ \{−∞\})$
	imasdsf1o.s	$⊢ S = \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = F (X) \land F (2^{nd} (h (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\}$
	imasdsf1o.t	$⊢ T = ⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{*}} (E \circ g))$
Assertion	imasdsf1olem	$⊢ φ \to F (X) D F (Y) = X E Y$

Proof

Step	Hyp	Ref	Expression
1		imasdsf1o.u	$⊢ φ \to U = F “_{𝑠} R$
2		imasdsf1o.v	$⊢ φ \to V = {Base}_{R}$
3		imasdsf1o.f	$⊢ φ \to F : V \underset{1-1 onto}{⟶} B$
4		imasdsf1o.r	$⊢ φ \to R \in Z$
5		imasdsf1o.e	$⊢ E = {dist (R) ↾}_{(V \times V)}$
6		imasdsf1o.d	$⊢ D = dist (U)$
7		imasdsf1o.m	$⊢ φ \to E \in ∞Met (V)$
8		imasdsf1o.x	$⊢ φ \to X \in V$
9		imasdsf1o.y	$⊢ φ \to Y \in V$
10		imasdsf1o.w	$⊢ W = ℝ_{𝑠}^{} ↾_{𝑠} (ℝ^{} ∖ \{−∞\})$
11		imasdsf1o.s	$⊢ S = \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = F (X) \land F (2^{nd} (h (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\}$
12		imasdsf1o.t	$⊢ T = ⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{*}} (E \circ g))$
13		f1ofo	$⊢ F : V \underset{1-1 onto}{⟶} B \to F : V \underset{onto}{⟶} B$
14	3 13	syl	$⊢ φ \to F : V \underset{onto}{⟶} B$
15		eqid	$⊢ dist (R) = dist (R)$
16		f1of	$⊢ F : V \underset{1-1 onto}{⟶} B \to F : V ⟶ B$
17	3 16	syl	$⊢ φ \to F : V ⟶ B$
18	17 8	ffvelrnd	$⊢ φ \to F (X) \in B$
19	17 9	ffvelrnd	$⊢ φ \to F (Y) \in B$
20	1 2 14 4 15 6 18 19 11 5	imasdsval2	$⊢ φ \to F (X) D F (Y) = sup (⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{} <)$
21	12	infeq1i	$⊢ sup (T ℝ^{} <) = sup (⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{*} <)$
22	20 21	eqtr4di	$⊢ φ \to F (X) D F (Y) = sup (T ℝ^{*} <)$
23		xrsbas	$⊢ ℝ^{} = {Base}_{ℝ_{𝑠}^{}}$
24		xrsadd	$⊢ +_{𝑒} = +_{ℝ_{𝑠}^{*}}$
25		xrsex	$⊢ ℝ_{𝑠}^{*} \in V$
26	25	a1i	$⊢ ((φ \land n \in ℕ) \land g \in S) \to ℝ_{𝑠}^{*} \in V$
27		fzfid	$⊢ ((φ \land n \in ℕ) \land g \in S) \to (1 \dots n) \in Fin$
28		difss	$⊢ ℝ^{} ∖ \{−∞\} \subseteq ℝ^{}$
29	28	a1i	$⊢ ((φ \land n \in ℕ) \land g \in S) \to ℝ^{} ∖ \{−∞\} \subseteq ℝ^{}$
30		xmetf	$⊢ E \in ∞Met (V) \to E : V \times V ⟶ ℝ^{*}$
31		ffn	$⊢ E : V \times V ⟶ ℝ^{*} \to E Fn (V \times V)$
32	7 30 31	3syl	$⊢ φ \to E Fn (V \times V)$
33		xmetcl	$⊢ (E \in ∞Met (V) \land f \in V \land g \in V) \to f E g \in ℝ^{*}$
34		xmetge0	$⊢ (E \in ∞Met (V) \land f \in V \land g \in V) \to 0 \leq f E g$
35		ge0nemnf	$⊢ (f E g \in ℝ^{*} \land 0 \leq f E g) \to f E g \neq −∞$
36	33 34 35	syl2anc	$⊢ (E \in ∞Met (V) \land f \in V \land g \in V) \to f E g \neq −∞$
37		eldifsn	$⊢ f E g \in (ℝ^{} ∖ \{−∞\}) \leftrightarrow (f E g \in ℝ^{} \land f E g \neq −∞)$
38	33 36 37	sylanbrc	$⊢ (E \in ∞Met (V) \land f \in V \land g \in V) \to f E g \in (ℝ^{*} ∖ \{−∞\})$
39	38	3expb	$⊢ (E \in ∞Met (V) \land (f \in V \land g \in V)) \to f E g \in (ℝ^{*} ∖ \{−∞\})$
40	7 39	sylan	$⊢ (φ \land (f \in V \land g \in V)) \to f E g \in (ℝ^{*} ∖ \{−∞\})$
41	40	ralrimivva	$⊢ φ \to \forall f \in V \forall g \in V f E g \in (ℝ^{*} ∖ \{−∞\})$
42		ffnov	$⊢ E : V \times V ⟶ ℝ^{} ∖ \{−∞\} \leftrightarrow (E Fn (V \times V) \land \forall f \in V \forall g \in V f E g \in (ℝ^{} ∖ \{−∞\}))$
43	32 41 42	sylanbrc	$⊢ φ \to E : V \times V ⟶ ℝ^{*} ∖ \{−∞\}$
44	43	ad2antrr	$⊢ ((φ \land n \in ℕ) \land g \in S) \to E : V \times V ⟶ ℝ^{*} ∖ \{−∞\}$
45	11	ssrab3	$⊢ S \subseteq {(V \times V)}^{(1 \dots n)}$
46	45	a1i	$⊢ (φ \land n \in ℕ) \to S \subseteq {(V \times V)}^{(1 \dots n)}$
47	46	sselda	$⊢ ((φ \land n \in ℕ) \land g \in S) \to g \in ({(V \times V)}^{(1 \dots n)})$
48		elmapi	$⊢ g \in ({(V \times V)}^{(1 \dots n)}) \to g : (1 \dots n) ⟶ V \times V$
49	47 48	syl	$⊢ ((φ \land n \in ℕ) \land g \in S) \to g : (1 \dots n) ⟶ V \times V$
50		fco	$⊢ (E : V \times V ⟶ ℝ^{} ∖ \{−∞\} \land g : (1 \dots n) ⟶ V \times V) \to (E \circ g) : (1 \dots n) ⟶ ℝ^{} ∖ \{−∞\}$
51	44 49 50	syl2anc	$⊢ ((φ \land n \in ℕ) \land g \in S) \to (E \circ g) : (1 \dots n) ⟶ ℝ^{*} ∖ \{−∞\}$
52		0re	$⊢ 0 \in ℝ$
53		rexr	$⊢ 0 \in ℝ \to 0 \in ℝ^{*}$
54		renemnf	$⊢ 0 \in ℝ \to 0 \neq −∞$
55		eldifsn	$⊢ 0 \in (ℝ^{} ∖ \{−∞\}) \leftrightarrow (0 \in ℝ^{} \land 0 \neq −∞)$
56	53 54 55	sylanbrc	$⊢ 0 \in ℝ \to 0 \in (ℝ^{*} ∖ \{−∞\})$
57	52 56	mp1i	$⊢ ((φ \land n \in ℕ) \land g \in S) \to 0 \in (ℝ^{*} ∖ \{−∞\})$
58		xaddid2	$⊢ x \in ℝ^{*} \to 0 +_{𝑒} x = x$
59		xaddid1	$⊢ x \in ℝ^{*} \to x +_{𝑒} 0 = x$
60	58 59	jca	$⊢ x \in ℝ^{*} \to (0 +_{𝑒} x = x \land x +_{𝑒} 0 = x)$
61	60	adantl	$⊢ (((φ \land n \in ℕ) \land g \in S) \land x \in ℝ^{*}) \to (0 +_{𝑒} x = x \land x +_{𝑒} 0 = x)$
62	23 24 10 26 27 29 51 57 61	gsumress	$⊢ ((φ \land n \in ℕ) \land g \in S) \to \sum_{ℝ_{𝑠}^{*}} (E \circ g) = \sum_{W} (E \circ g)$
63	10 23	ressbas2	$⊢ ℝ^{} ∖ \{−∞\} \subseteq ℝ^{} \to ℝ^{*} ∖ \{−∞\} = {Base}_{W}$
64	28 63	ax-mp	$⊢ ℝ^{*} ∖ \{−∞\} = {Base}_{W}$
65	10	xrs10	$⊢ 0 = 0_{W}$
66	10	xrs1cmn	$⊢ W \in CMnd$
67	66	a1i	$⊢ ((φ \land n \in ℕ) \land g \in S) \to W \in CMnd$
68		c0ex	$⊢ 0 \in V$
69	68	a1i	$⊢ ((φ \land n \in ℕ) \land g \in S) \to 0 \in V$
70	51 27 69	fdmfifsupp	$⊢ ((φ \land n \in ℕ) \land g \in S) \to {finSupp}_{0} ((E \circ g))$
71	64 65 67 27 51 70	gsumcl	$⊢ ((φ \land n \in ℕ) \land g \in S) \to \sum_{W} (E \circ g) \in (ℝ^{*} ∖ \{−∞\})$
72	62 71	eqeltrd	$⊢ ((φ \land n \in ℕ) \land g \in S) \to \sum_{ℝ_{𝑠}^{}} (E \circ g) \in (ℝ^{} ∖ \{−∞\})$
73	72	eldifad	$⊢ ((φ \land n \in ℕ) \land g \in S) \to \sum_{ℝ_{𝑠}^{}} (E \circ g) \in ℝ^{}$
74	73	fmpttd	$⊢ (φ \land n \in ℕ) \to (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) : S ⟶ ℝ^{}$
75	74	frnd	$⊢ (φ \land n \in ℕ) \to ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) \subseteq ℝ^{}$
76	75	ralrimiva	$⊢ φ \to \forall n \in ℕ ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) \subseteq ℝ^{}$
77		iunss	$⊢ ⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) \subseteq ℝ^{} \leftrightarrow \forall n \in ℕ ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) \subseteq ℝ^{}$
78	76 77	sylibr	$⊢ φ \to ⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) \subseteq ℝ^{}$
79	12 78	eqsstrid	$⊢ φ \to T \subseteq ℝ^{*}$
80		infxrcl	$⊢ T \subseteq ℝ^{} \to sup (T ℝ^{} <) \in ℝ^{*}$
81	79 80	syl	$⊢ φ \to sup (T ℝ^{} <) \in ℝ^{}$
82		xmetcl	$⊢ (E \in ∞Met (V) \land X \in V \land Y \in V) \to X E Y \in ℝ^{*}$
83	7 8 9 82	syl3anc	$⊢ φ \to X E Y \in ℝ^{*}$
84		1nn	$⊢ 1 \in ℕ$
85		1ex	$⊢ 1 \in V$
86		opex	$⊢ ⟨X, Y⟩ \in V$
87	85 86	f1osn	$⊢ \{⟨1, ⟨X, Y⟩⟩\} : \{1\} \underset{1-1 onto}{⟶} \{⟨X, Y⟩\}$
88		f1of	$⊢ \{⟨1, ⟨X, Y⟩⟩\} : \{1\} \underset{1-1 onto}{⟶} \{⟨X, Y⟩\} \to \{⟨1, ⟨X, Y⟩⟩\} : \{1\} ⟶ \{⟨X, Y⟩\}$
89	87 88	ax-mp	$⊢ \{⟨1, ⟨X, Y⟩⟩\} : \{1\} ⟶ \{⟨X, Y⟩\}$
90	8 9	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (V \times V)$
91	90	snssd	$⊢ φ \to \{⟨X, Y⟩\} \subseteq V \times V$
92		fss	$⊢ (\{⟨1, ⟨X, Y⟩⟩\} : \{1\} ⟶ \{⟨X, Y⟩\} \land \{⟨X, Y⟩\} \subseteq V \times V) \to \{⟨1, ⟨X, Y⟩⟩\} : \{1\} ⟶ V \times V$
93	89 91 92	sylancr	$⊢ φ \to \{⟨1, ⟨X, Y⟩⟩\} : \{1\} ⟶ V \times V$
94	7	elfvexd	$⊢ φ \to V \in V$
95	94 94	xpexd	$⊢ φ \to V \times V \in V$
96		snex	$⊢ \{1\} \in V$
97		elmapg	$⊢ (V \times V \in V \land \{1\} \in V) \to (\{⟨1, ⟨X, Y⟩⟩\} \in ({(V \times V)}^{\{1\}}) \leftrightarrow \{⟨1, ⟨X, Y⟩⟩\} : \{1\} ⟶ V \times V)$
98	95 96 97	sylancl	$⊢ φ \to (\{⟨1, ⟨X, Y⟩⟩\} \in ({(V \times V)}^{\{1\}}) \leftrightarrow \{⟨1, ⟨X, Y⟩⟩\} : \{1\} ⟶ V \times V)$
99	93 98	mpbird	$⊢ φ \to \{⟨1, ⟨X, Y⟩⟩\} \in ({(V \times V)}^{\{1\}})$
100		op1stg	$⊢ (X \in V \land Y \in V) \to 1^{st} (⟨X, Y⟩) = X$
101	8 9 100	syl2anc	$⊢ φ \to 1^{st} (⟨X, Y⟩) = X$
102	101	fveq2d	$⊢ φ \to F (1^{st} (⟨X, Y⟩)) = F (X)$
103		op2ndg	$⊢ (X \in V \land Y \in V) \to 2^{nd} (⟨X, Y⟩) = Y$
104	8 9 103	syl2anc	$⊢ φ \to 2^{nd} (⟨X, Y⟩) = Y$
105	104	fveq2d	$⊢ φ \to F (2^{nd} (⟨X, Y⟩)) = F (Y)$
106	102 105	jca	$⊢ φ \to (F (1^{st} (⟨X, Y⟩)) = F (X) \land F (2^{nd} (⟨X, Y⟩)) = F (Y))$
107	25	a1i	$⊢ φ \to ℝ_{𝑠}^{*} \in V$
108		snfi	$⊢ \{1\} \in Fin$
109	108	a1i	$⊢ φ \to \{1\} \in Fin$
110	28	a1i	$⊢ φ \to ℝ^{} ∖ \{−∞\} \subseteq ℝ^{}$
111		xmetge0	$⊢ (E \in ∞Met (V) \land X \in V \land Y \in V) \to 0 \leq X E Y$
112	7 8 9 111	syl3anc	$⊢ φ \to 0 \leq X E Y$
113		ge0nemnf	$⊢ (X E Y \in ℝ^{*} \land 0 \leq X E Y) \to X E Y \neq −∞$
114	83 112 113	syl2anc	$⊢ φ \to X E Y \neq −∞$
115		eldifsn	$⊢ X E Y \in (ℝ^{} ∖ \{−∞\}) \leftrightarrow (X E Y \in ℝ^{} \land X E Y \neq −∞)$
116	83 114 115	sylanbrc	$⊢ φ \to X E Y \in (ℝ^{*} ∖ \{−∞\})$
117		fconst6g	$⊢ X E Y \in (ℝ^{} ∖ \{−∞\}) \to (\{1\} \times \{X E Y\}) : \{1\} ⟶ ℝ^{} ∖ \{−∞\}$
118	116 117	syl	$⊢ φ \to (\{1\} \times \{X E Y\}) : \{1\} ⟶ ℝ^{*} ∖ \{−∞\}$
119		fcoconst	$⊢ (E Fn (V \times V) \land ⟨X, Y⟩ \in (V \times V)) \to E \circ (\{1\} \times \{⟨X, Y⟩\}) = \{1\} \times \{E (⟨X, Y⟩)\}$
120	32 90 119	syl2anc	$⊢ φ \to E \circ (\{1\} \times \{⟨X, Y⟩\}) = \{1\} \times \{E (⟨X, Y⟩)\}$
121	85 86	xpsn	$⊢ \{1\} \times \{⟨X, Y⟩\} = \{⟨1, ⟨X, Y⟩⟩\}$
122	121	coeq2i	$⊢ E \circ (\{1\} \times \{⟨X, Y⟩\}) = E \circ \{⟨1, ⟨X, Y⟩⟩\}$
123		df-ov	$⊢ X E Y = E (⟨X, Y⟩)$
124	123	eqcomi	$⊢ E (⟨X, Y⟩) = X E Y$
125	124	sneqi	$⊢ \{E (⟨X, Y⟩)\} = \{X E Y\}$
126	125	xpeq2i	$⊢ \{1\} \times \{E (⟨X, Y⟩)\} = \{1\} \times \{X E Y\}$
127	120 122 126	3eqtr3g	$⊢ φ \to E \circ \{⟨1, ⟨X, Y⟩⟩\} = \{1\} \times \{X E Y\}$
128	127	feq1d	$⊢ φ \to ((E \circ \{⟨1, ⟨X, Y⟩⟩\}) : \{1\} ⟶ ℝ^{} ∖ \{−∞\} \leftrightarrow (\{1\} \times \{X E Y\}) : \{1\} ⟶ ℝ^{} ∖ \{−∞\})$
129	118 128	mpbird	$⊢ φ \to (E \circ \{⟨1, ⟨X, Y⟩⟩\}) : \{1\} ⟶ ℝ^{*} ∖ \{−∞\}$
130	52 56	mp1i	$⊢ φ \to 0 \in (ℝ^{*} ∖ \{−∞\})$
131	60	adantl	$⊢ (φ \land x \in ℝ^{*}) \to (0 +_{𝑒} x = x \land x +_{𝑒} 0 = x)$
132	23 24 10 107 109 110 129 130 131	gsumress	$⊢ φ \to \sum_{ℝ_{𝑠}^{*}} (E \circ \{⟨1, ⟨X, Y⟩⟩\}) = \sum_{W} (E \circ \{⟨1, ⟨X, Y⟩⟩\})$
133		fconstmpt	$⊢ \{1\} \times \{X E Y\} = (j \in \{1\} ⟼ X E Y)$
134	127 133	eqtrdi	$⊢ φ \to E \circ \{⟨1, ⟨X, Y⟩⟩\} = (j \in \{1\} ⟼ X E Y)$
135	134	oveq2d	$⊢ φ \to \sum_{W} (E \circ \{⟨1, ⟨X, Y⟩⟩\}) = \underset{j \in \{1\}}{\sum_{W}} (X E Y)$
136		cmnmnd	$⊢ W \in CMnd \to W \in Mnd$
137	66 136	mp1i	$⊢ φ \to W \in Mnd$
138	84	a1i	$⊢ φ \to 1 \in ℕ$
139		eqidd	$⊢ j = 1 \to X E Y = X E Y$
140	64 139	gsumsn	$⊢ (W \in Mnd \land 1 \in ℕ \land X E Y \in (ℝ^{*} ∖ \{−∞\})) \to \underset{j \in \{1\}}{\sum_{W}} (X E Y) = X E Y$
141	137 138 116 140	syl3anc	$⊢ φ \to \underset{j \in \{1\}}{\sum_{W}} (X E Y) = X E Y$
142	132 135 141	3eqtrrd	$⊢ φ \to X E Y = \sum_{ℝ_{𝑠}^{*}} (E \circ \{⟨1, ⟨X, Y⟩⟩\})$
143		fveq1	$⊢ g = \{⟨1, ⟨X, Y⟩⟩\} \to g (1) = \{⟨1, ⟨X, Y⟩⟩\} (1)$
144	85 86	fvsn	$⊢ \{⟨1, ⟨X, Y⟩⟩\} (1) = ⟨X, Y⟩$
145	143 144	eqtrdi	$⊢ g = \{⟨1, ⟨X, Y⟩⟩\} \to g (1) = ⟨X, Y⟩$
146	145	fveq2d	$⊢ g = \{⟨1, ⟨X, Y⟩⟩\} \to 1^{st} (g (1)) = 1^{st} (⟨X, Y⟩)$
147	146	fveqeq2d	$⊢ g = \{⟨1, ⟨X, Y⟩⟩\} \to (F (1^{st} (g (1))) = F (X) \leftrightarrow F (1^{st} (⟨X, Y⟩)) = F (X))$
148	145	fveq2d	$⊢ g = \{⟨1, ⟨X, Y⟩⟩\} \to 2^{nd} (g (1)) = 2^{nd} (⟨X, Y⟩)$
149	148	fveqeq2d	$⊢ g = \{⟨1, ⟨X, Y⟩⟩\} \to (F (2^{nd} (g (1))) = F (Y) \leftrightarrow F (2^{nd} (⟨X, Y⟩)) = F (Y))$
150	147 149	anbi12d	$⊢ g = \{⟨1, ⟨X, Y⟩⟩\} \to ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (1))) = F (Y)) \leftrightarrow (F (1^{st} (⟨X, Y⟩)) = F (X) \land F (2^{nd} (⟨X, Y⟩)) = F (Y)))$
151		coeq2	$⊢ g = \{⟨1, ⟨X, Y⟩⟩\} \to E \circ g = E \circ \{⟨1, ⟨X, Y⟩⟩\}$
152	151	oveq2d	$⊢ g = \{⟨1, ⟨X, Y⟩⟩\} \to \sum_{ℝ_{𝑠}^{}} (E \circ g) = \sum_{ℝ_{𝑠}^{}} (E \circ \{⟨1, ⟨X, Y⟩⟩\})$
153	152	eqeq2d	$⊢ g = \{⟨1, ⟨X, Y⟩⟩\} \to (X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g) \leftrightarrow X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ \{⟨1, ⟨X, Y⟩⟩\}))$
154	150 153	anbi12d	$⊢ g = \{⟨1, ⟨X, Y⟩⟩\} \to (((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (1))) = F (Y)) \land X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g)) \leftrightarrow ((F (1^{st} (⟨X, Y⟩)) = F (X) \land F (2^{nd} (⟨X, Y⟩)) = F (Y)) \land X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ \{⟨1, ⟨X, Y⟩⟩\})))$
155	154	rspcev	$⊢ (\{⟨1, ⟨X, Y⟩⟩\} \in ({(V \times V)}^{\{1\}}) \land ((F (1^{st} (⟨X, Y⟩)) = F (X) \land F (2^{nd} (⟨X, Y⟩)) = F (Y)) \land X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ \{⟨1, ⟨X, Y⟩⟩\}))) \to \exists g \in ({(V \times V)}^{\{1\}}) ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (1))) = F (Y)) \land X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g))$
156	99 106 142 155	syl12anc	$⊢ φ \to \exists g \in ({(V \times V)}^{\{1\}}) ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (1))) = F (Y)) \land X E Y = \sum_{ℝ_{𝑠}^{*}} (E \circ g))$
157		ovex	$⊢ X E Y \in V$
158		eqid	$⊢ (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) = (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g))$
159	158	elrnmpt	$⊢ X E Y \in V \to (X E Y \in ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) \leftrightarrow \exists g \in S X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g))$
160	157 159	ax-mp	$⊢ X E Y \in ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) \leftrightarrow \exists g \in S X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g)$
161	11	rexeqi	$⊢ \exists g \in S X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g) \leftrightarrow \exists g \in \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = F (X) \land F (2^{nd} (h (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\} X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g)$
162		fveq1	$⊢ h = g \to h (1) = g (1)$
163	162	fveq2d	$⊢ h = g \to 1^{st} (h (1)) = 1^{st} (g (1))$
164	163	fveqeq2d	$⊢ h = g \to (F (1^{st} (h (1))) = F (X) \leftrightarrow F (1^{st} (g (1))) = F (X))$
165		fveq1	$⊢ h = g \to h (n) = g (n)$
166	165	fveq2d	$⊢ h = g \to 2^{nd} (h (n)) = 2^{nd} (g (n))$
167	166	fveqeq2d	$⊢ h = g \to (F (2^{nd} (h (n))) = F (Y) \leftrightarrow F (2^{nd} (g (n))) = F (Y))$
168		fveq1	$⊢ h = g \to h (i) = g (i)$
169	168	fveq2d	$⊢ h = g \to 2^{nd} (h (i)) = 2^{nd} (g (i))$
170	169	fveq2d	$⊢ h = g \to F (2^{nd} (h (i))) = F (2^{nd} (g (i)))$
171		fveq1	$⊢ h = g \to h (i + 1) = g (i + 1)$
172	171	fveq2d	$⊢ h = g \to 1^{st} (h (i + 1)) = 1^{st} (g (i + 1))$
173	172	fveq2d	$⊢ h = g \to F (1^{st} (h (i + 1))) = F (1^{st} (g (i + 1)))$
174	170 173	eqeq12d	$⊢ h = g \to (F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))) \leftrightarrow F (2^{nd} (g (i))) = F (1^{st} (g (i + 1))))$
175	174	ralbidv	$⊢ h = g \to (\forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))) \leftrightarrow \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1))))$
176	164 167 175	3anbi123d	$⊢ h = g \to ((F (1^{st} (h (1))) = F (X) \land F (2^{nd} (h (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1)))) \leftrightarrow (F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1)))))$
177	176	rexrab	$⊢ \exists g \in \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = F (X) \land F (2^{nd} (h (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\} X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g) \leftrightarrow \exists g \in ({(V \times V)}^{(1 \dots n)}) ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1)))) \land X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g))$
178	161 177	bitri	$⊢ \exists g \in S X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g) \leftrightarrow \exists g \in ({(V \times V)}^{(1 \dots n)}) ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1)))) \land X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g))$
179		oveq2	$⊢ n = 1 \to (1 \dots n) = (1 \dots 1)$
180		1z	$⊢ 1 \in ℤ$
181		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
182	180 181	ax-mp	$⊢ (1 \dots 1) = \{1\}$
183	179 182	eqtrdi	$⊢ n = 1 \to (1 \dots n) = \{1\}$
184	183	oveq2d	$⊢ n = 1 \to {(V \times V)}^{(1 \dots n)} = {(V \times V)}^{\{1\}}$
185		df-3an	$⊢ (F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1)))) \leftrightarrow ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y)) \land \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1))))$
186		ral0	$⊢ \forall i \in \emptyset F (2^{nd} (g (i))) = F (1^{st} (g (i + 1)))$
187		oveq1	$⊢ n = 1 \to n - 1 = 1 - 1$
188		1m1e0	$⊢ 1 - 1 = 0$
189	187 188	eqtrdi	$⊢ n = 1 \to n - 1 = 0$
190	189	oveq2d	$⊢ n = 1 \to (1 \dots n - 1) = (1 \dots 0)$
191		fz10	$⊢ (1 \dots 0) = \emptyset$
192	190 191	eqtrdi	$⊢ n = 1 \to (1 \dots n - 1) = \emptyset$
193	192	raleqdv	$⊢ n = 1 \to (\forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1))) \leftrightarrow \forall i \in \emptyset F (2^{nd} (g (i))) = F (1^{st} (g (i + 1))))$
194	186 193	mpbiri	$⊢ n = 1 \to \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1)))$
195	194	biantrud	$⊢ n = 1 \to ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y)) \leftrightarrow ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y)) \land \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1)))))$
196		2fveq3	$⊢ n = 1 \to 2^{nd} (g (n)) = 2^{nd} (g (1))$
197	196	fveqeq2d	$⊢ n = 1 \to (F (2^{nd} (g (n))) = F (Y) \leftrightarrow F (2^{nd} (g (1))) = F (Y))$
198	197	anbi2d	$⊢ n = 1 \to ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y)) \leftrightarrow (F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (1))) = F (Y)))$
199	195 198	bitr3d	$⊢ n = 1 \to (((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y)) \land \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1)))) \leftrightarrow (F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (1))) = F (Y)))$
200	185 199	syl5bb	$⊢ n = 1 \to ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1)))) \leftrightarrow (F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (1))) = F (Y)))$
201	200	anbi1d	$⊢ n = 1 \to (((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1)))) \land X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g)) \leftrightarrow ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (1))) = F (Y)) \land X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g)))$
202	184 201	rexeqbidv	$⊢ n = 1 \to (\exists g \in ({(V \times V)}^{(1 \dots n)}) ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1)))) \land X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g)) \leftrightarrow \exists g \in ({(V \times V)}^{\{1\}}) ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (1))) = F (Y)) \land X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g)))$
203	178 202	syl5bb	$⊢ n = 1 \to (\exists g \in S X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g) \leftrightarrow \exists g \in ({(V \times V)}^{\{1\}}) ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (1))) = F (Y)) \land X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g)))$
204	160 203	syl5bb	$⊢ n = 1 \to (X E Y \in ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) \leftrightarrow \exists g \in ({(V \times V)}^{\{1\}}) ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (1))) = F (Y)) \land X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g)))$
205	204	rspcev	$⊢ (1 \in ℕ \land \exists g \in ({(V \times V)}^{\{1\}}) ((F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (1))) = F (Y)) \land X E Y = \sum_{ℝ_{𝑠}^{}} (E \circ g))) \to \exists n \in ℕ X E Y \in ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g))$
206	84 156 205	sylancr	$⊢ φ \to \exists n \in ℕ X E Y \in ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{*}} (E \circ g))$
207		eliun	$⊢ X E Y \in ⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) \leftrightarrow \exists n \in ℕ X E Y \in ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g))$
208	206 207	sylibr	$⊢ φ \to X E Y \in ⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{*}} (E \circ g))$
209	208 12	eleqtrrdi	$⊢ φ \to X E Y \in T$
210		infxrlb	$⊢ (T \subseteq ℝ^{} \land X E Y \in T) \to sup (T ℝ^{} <) \leq X E Y$
211	79 209 210	syl2anc	$⊢ φ \to sup (T ℝ^{*} <) \leq X E Y$
212	12	eleq2i	$⊢ p \in T \leftrightarrow p \in ⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{*}} (E \circ g))$
213		eliun	$⊢ p \in ⋃_{n \in ℕ} ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) \leftrightarrow \exists n \in ℕ p \in ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g))$
214	212 213	bitri	$⊢ p \in T \leftrightarrow \exists n \in ℕ p \in ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{*}} (E \circ g))$
215	158	elrnmpt	$⊢ p \in V \to (p \in ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) \leftrightarrow \exists g \in S p = \sum_{ℝ_{𝑠}^{}} (E \circ g))$
216	215	elv	$⊢ p \in ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) \leftrightarrow \exists g \in S p = \sum_{ℝ_{𝑠}^{}} (E \circ g)$
217	176 11	elrab2	$⊢ g \in S \leftrightarrow (g \in ({(V \times V)}^{(1 \dots n)}) \land (F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1)))))$
218	217	simprbi	$⊢ g \in S \to (F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1))))$
219	218	adantl	$⊢ ((φ \land n \in ℕ) \land g \in S) \to (F (1^{st} (g (1))) = F (X) \land F (2^{nd} (g (n))) = F (Y) \land \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1))))$
220	219	simp2d	$⊢ ((φ \land n \in ℕ) \land g \in S) \to F (2^{nd} (g (n))) = F (Y)$
221	3	ad2antrr	$⊢ ((φ \land n \in ℕ) \land g \in S) \to F : V \underset{1-1 onto}{⟶} B$
222		f1of1	$⊢ F : V \underset{1-1 onto}{⟶} B \to F : V \underset{1-1}{⟶} B$
223	221 222	syl	$⊢ ((φ \land n \in ℕ) \land g \in S) \to F : V \underset{1-1}{⟶} B$
224		simplr	$⊢ ((φ \land n \in ℕ) \land g \in S) \to n \in ℕ$
225		elfz1end	$⊢ n \in ℕ \leftrightarrow n \in (1 \dots n)$
226	224 225	sylib	$⊢ ((φ \land n \in ℕ) \land g \in S) \to n \in (1 \dots n)$
227	49 226	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land g \in S) \to g (n) \in (V \times V)$
228		xp2nd	$⊢ g (n) \in (V \times V) \to 2^{nd} (g (n)) \in V$
229	227 228	syl	$⊢ ((φ \land n \in ℕ) \land g \in S) \to 2^{nd} (g (n)) \in V$
230	9	ad2antrr	$⊢ ((φ \land n \in ℕ) \land g \in S) \to Y \in V$
231		f1fveq	$⊢ (F : V \underset{1-1}{⟶} B \land (2^{nd} (g (n)) \in V \land Y \in V)) \to (F (2^{nd} (g (n))) = F (Y) \leftrightarrow 2^{nd} (g (n)) = Y)$
232	223 229 230 231	syl12anc	$⊢ ((φ \land n \in ℕ) \land g \in S) \to (F (2^{nd} (g (n))) = F (Y) \leftrightarrow 2^{nd} (g (n)) = Y)$
233	220 232	mpbid	$⊢ ((φ \land n \in ℕ) \land g \in S) \to 2^{nd} (g (n)) = Y$
234	233	oveq2d	$⊢ ((φ \land n \in ℕ) \land g \in S) \to X E 2^{nd} (g (n)) = X E Y$
235		eleq1	$⊢ m = 1 \to (m \in (1 \dots n) \leftrightarrow 1 \in (1 \dots n))$
236		2fveq3	$⊢ m = 1 \to 2^{nd} (g (m)) = 2^{nd} (g (1))$
237	236	oveq2d	$⊢ m = 1 \to X E 2^{nd} (g (m)) = X E 2^{nd} (g (1))$
238		oveq2	$⊢ m = 1 \to (1 \dots m) = (1 \dots 1)$
239	238 182	eqtrdi	$⊢ m = 1 \to (1 \dots m) = \{1\}$
240	239	reseq2d	$⊢ m = 1 \to {(E \circ g) ↾}_{(1 \dots m)} = {(E \circ g) ↾}_{\{1\}}$
241	240	oveq2d	$⊢ m = 1 \to \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)}) = \sum_{W} ({(E \circ g) ↾}_{\{1\}})$
242	237 241	breq12d	$⊢ m = 1 \to (X E 2^{nd} (g (m)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)}) \leftrightarrow X E 2^{nd} (g (1)) \leq \sum_{W} ({(E \circ g) ↾}_{\{1\}}))$
243	235 242	imbi12d	$⊢ m = 1 \to ((m \in (1 \dots n) \to X E 2^{nd} (g (m)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)})) \leftrightarrow (1 \in (1 \dots n) \to X E 2^{nd} (g (1)) \leq \sum_{W} ({(E \circ g) ↾}_{\{1\}})))$
244	243	imbi2d	$⊢ m = 1 \to ((((φ \land n \in ℕ) \land g \in S) \to (m \in (1 \dots n) \to X E 2^{nd} (g (m)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)}))) \leftrightarrow (((φ \land n \in ℕ) \land g \in S) \to (1 \in (1 \dots n) \to X E 2^{nd} (g (1)) \leq \sum_{W} ({(E \circ g) ↾}_{\{1\}}))))$
245		eleq1	$⊢ m = x \to (m \in (1 \dots n) \leftrightarrow x \in (1 \dots n))$
246		2fveq3	$⊢ m = x \to 2^{nd} (g (m)) = 2^{nd} (g (x))$
247	246	oveq2d	$⊢ m = x \to X E 2^{nd} (g (m)) = X E 2^{nd} (g (x))$
248		oveq2	$⊢ m = x \to (1 \dots m) = (1 \dots x)$
249	248	reseq2d	$⊢ m = x \to {(E \circ g) ↾}_{(1 \dots m)} = {(E \circ g) ↾}_{(1 \dots x)}$
250	249	oveq2d	$⊢ m = x \to \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)}) = \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)})$
251	247 250	breq12d	$⊢ m = x \to (X E 2^{nd} (g (m)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)}) \leftrightarrow X E 2^{nd} (g (x)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)}))$
252	245 251	imbi12d	$⊢ m = x \to ((m \in (1 \dots n) \to X E 2^{nd} (g (m)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)})) \leftrightarrow (x \in (1 \dots n) \to X E 2^{nd} (g (x)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)})))$
253	252	imbi2d	$⊢ m = x \to ((((φ \land n \in ℕ) \land g \in S) \to (m \in (1 \dots n) \to X E 2^{nd} (g (m)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)}))) \leftrightarrow (((φ \land n \in ℕ) \land g \in S) \to (x \in (1 \dots n) \to X E 2^{nd} (g (x)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)}))))$
254		eleq1	$⊢ m = x + 1 \to (m \in (1 \dots n) \leftrightarrow x + 1 \in (1 \dots n))$
255		2fveq3	$⊢ m = x + 1 \to 2^{nd} (g (m)) = 2^{nd} (g (x + 1))$
256	255	oveq2d	$⊢ m = x + 1 \to X E 2^{nd} (g (m)) = X E 2^{nd} (g (x + 1))$
257		oveq2	$⊢ m = x + 1 \to (1 \dots m) = (1 \dots x + 1)$
258	257	reseq2d	$⊢ m = x + 1 \to {(E \circ g) ↾}_{(1 \dots m)} = {(E \circ g) ↾}_{(1 \dots x + 1)}$
259	258	oveq2d	$⊢ m = x + 1 \to \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)}) = \sum_{W} ({(E \circ g) ↾}_{(1 \dots x + 1)})$
260	256 259	breq12d	$⊢ m = x + 1 \to (X E 2^{nd} (g (m)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)}) \leftrightarrow X E 2^{nd} (g (x + 1)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x + 1)}))$
261	254 260	imbi12d	$⊢ m = x + 1 \to ((m \in (1 \dots n) \to X E 2^{nd} (g (m)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)})) \leftrightarrow (x + 1 \in (1 \dots n) \to X E 2^{nd} (g (x + 1)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x + 1)})))$
262	261	imbi2d	$⊢ m = x + 1 \to ((((φ \land n \in ℕ) \land g \in S) \to (m \in (1 \dots n) \to X E 2^{nd} (g (m)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)}))) \leftrightarrow (((φ \land n \in ℕ) \land g \in S) \to (x + 1 \in (1 \dots n) \to X E 2^{nd} (g (x + 1)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x + 1)}))))$
263		eleq1	$⊢ m = n \to (m \in (1 \dots n) \leftrightarrow n \in (1 \dots n))$
264		2fveq3	$⊢ m = n \to 2^{nd} (g (m)) = 2^{nd} (g (n))$
265	264	oveq2d	$⊢ m = n \to X E 2^{nd} (g (m)) = X E 2^{nd} (g (n))$
266		oveq2	$⊢ m = n \to (1 \dots m) = (1 \dots n)$
267	266	reseq2d	$⊢ m = n \to {(E \circ g) ↾}_{(1 \dots m)} = {(E \circ g) ↾}_{(1 \dots n)}$
268	267	oveq2d	$⊢ m = n \to \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)}) = \sum_{W} ({(E \circ g) ↾}_{(1 \dots n)})$
269	265 268	breq12d	$⊢ m = n \to (X E 2^{nd} (g (m)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)}) \leftrightarrow X E 2^{nd} (g (n)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots n)}))$
270	263 269	imbi12d	$⊢ m = n \to ((m \in (1 \dots n) \to X E 2^{nd} (g (m)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)})) \leftrightarrow (n \in (1 \dots n) \to X E 2^{nd} (g (n)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots n)})))$
271	270	imbi2d	$⊢ m = n \to ((((φ \land n \in ℕ) \land g \in S) \to (m \in (1 \dots n) \to X E 2^{nd} (g (m)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots m)}))) \leftrightarrow (((φ \land n \in ℕ) \land g \in S) \to (n \in (1 \dots n) \to X E 2^{nd} (g (n)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots n)}))))$
272	7	ad2antrr	$⊢ ((φ \land n \in ℕ) \land g \in S) \to E \in ∞Met (V)$
273	8	ad2antrr	$⊢ ((φ \land n \in ℕ) \land g \in S) \to X \in V$
274		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
275	224 274	eleqtrdi	$⊢ ((φ \land n \in ℕ) \land g \in S) \to n \in ℤ_{\geq 1}$
276		eluzfz1	$⊢ n \in ℤ_{\geq 1} \to 1 \in (1 \dots n)$
277	275 276	syl	$⊢ ((φ \land n \in ℕ) \land g \in S) \to 1 \in (1 \dots n)$
278	49 277	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land g \in S) \to g (1) \in (V \times V)$
279		xp2nd	$⊢ g (1) \in (V \times V) \to 2^{nd} (g (1)) \in V$
280	278 279	syl	$⊢ ((φ \land n \in ℕ) \land g \in S) \to 2^{nd} (g (1)) \in V$
281		xmetcl	$⊢ (E \in ∞Met (V) \land X \in V \land 2^{nd} (g (1)) \in V) \to X E 2^{nd} (g (1)) \in ℝ^{*}$
282	272 273 280 281	syl3anc	$⊢ ((φ \land n \in ℕ) \land g \in S) \to X E 2^{nd} (g (1)) \in ℝ^{*}$
283	282	xrleidd	$⊢ ((φ \land n \in ℕ) \land g \in S) \to X E 2^{nd} (g (1)) \leq X E 2^{nd} (g (1))$
284	137	ad2antrr	$⊢ ((φ \land n \in ℕ) \land g \in S) \to W \in Mnd$
285	84	a1i	$⊢ ((φ \land n \in ℕ) \land g \in S) \to 1 \in ℕ$
286	44 278	ffvelrnd	$⊢ ((φ \land n \in ℕ) \land g \in S) \to E (g (1)) \in (ℝ^{*} ∖ \{−∞\})$
287		2fveq3	$⊢ j = 1 \to E (g (j)) = E (g (1))$
288	64 287	gsumsn	$⊢ (W \in Mnd \land 1 \in ℕ \land E (g (1)) \in (ℝ^{*} ∖ \{−∞\})) \to \underset{j \in \{1\}}{\sum_{W}} E (g (j)) = E (g (1))$
289	284 285 286 288	syl3anc	$⊢ ((φ \land n \in ℕ) \land g \in S) \to \underset{j \in \{1\}}{\sum_{W}} E (g (j)) = E (g (1))$
290	272 30	syl	$⊢ ((φ \land n \in ℕ) \land g \in S) \to E : V \times V ⟶ ℝ^{*}$
291		fcompt	$⊢ (E : V \times V ⟶ ℝ^{*} \land g : (1 \dots n) ⟶ V \times V) \to E \circ g = (j \in (1 \dots n) ⟼ E (g (j)))$
292	290 49 291	syl2anc	$⊢ ((φ \land n \in ℕ) \land g \in S) \to E \circ g = (j \in (1 \dots n) ⟼ E (g (j)))$
293	292	reseq1d	$⊢ ((φ \land n \in ℕ) \land g \in S) \to {(E \circ g) ↾}_{\{1\}} = {(j \in (1 \dots n) ⟼ E (g (j))) ↾}_{\{1\}}$
294	277	snssd	$⊢ ((φ \land n \in ℕ) \land g \in S) \to \{1\} \subseteq (1 \dots n)$
295	294	resmptd	$⊢ ((φ \land n \in ℕ) \land g \in S) \to {(j \in (1 \dots n) ⟼ E (g (j))) ↾}_{\{1\}} = (j \in \{1\} ⟼ E (g (j)))$
296	293 295	eqtrd	$⊢ ((φ \land n \in ℕ) \land g \in S) \to {(E \circ g) ↾}_{\{1\}} = (j \in \{1\} ⟼ E (g (j)))$
297	296	oveq2d	$⊢ ((φ \land n \in ℕ) \land g \in S) \to \sum_{W} ({(E \circ g) ↾}_{\{1\}}) = \underset{j \in \{1\}}{\sum_{W}} E (g (j))$
298		df-ov	$⊢ X E 2^{nd} (g (1)) = E (⟨X, 2^{nd} (g (1))⟩)$
299		1st2nd2	$⊢ g (1) \in (V \times V) \to g (1) = ⟨1^{st} (g (1)), 2^{nd} (g (1))⟩$
300	278 299	syl	$⊢ ((φ \land n \in ℕ) \land g \in S) \to g (1) = ⟨1^{st} (g (1)), 2^{nd} (g (1))⟩$
301	219	simp1d	$⊢ ((φ \land n \in ℕ) \land g \in S) \to F (1^{st} (g (1))) = F (X)$
302		xp1st	$⊢ g (1) \in (V \times V) \to 1^{st} (g (1)) \in V$
303	278 302	syl	$⊢ ((φ \land n \in ℕ) \land g \in S) \to 1^{st} (g (1)) \in V$
304		f1fveq	$⊢ (F : V \underset{1-1}{⟶} B \land (1^{st} (g (1)) \in V \land X \in V)) \to (F (1^{st} (g (1))) = F (X) \leftrightarrow 1^{st} (g (1)) = X)$
305	223 303 273 304	syl12anc	$⊢ ((φ \land n \in ℕ) \land g \in S) \to (F (1^{st} (g (1))) = F (X) \leftrightarrow 1^{st} (g (1)) = X)$
306	301 305	mpbid	$⊢ ((φ \land n \in ℕ) \land g \in S) \to 1^{st} (g (1)) = X$
307	306	opeq1d	$⊢ ((φ \land n \in ℕ) \land g \in S) \to ⟨1^{st} (g (1)), 2^{nd} (g (1))⟩ = ⟨X, 2^{nd} (g (1))⟩$
308	300 307	eqtr2d	$⊢ ((φ \land n \in ℕ) \land g \in S) \to ⟨X, 2^{nd} (g (1))⟩ = g (1)$
309	308	fveq2d	$⊢ ((φ \land n \in ℕ) \land g \in S) \to E (⟨X, 2^{nd} (g (1))⟩) = E (g (1))$
310	298 309	eqtrid	$⊢ ((φ \land n \in ℕ) \land g \in S) \to X E 2^{nd} (g (1)) = E (g (1))$
311	289 297 310	3eqtr4d	$⊢ ((φ \land n \in ℕ) \land g \in S) \to \sum_{W} ({(E \circ g) ↾}_{\{1\}}) = X E 2^{nd} (g (1))$
312	283 311	breqtrrd	$⊢ ((φ \land n \in ℕ) \land g \in S) \to X E 2^{nd} (g (1)) \leq \sum_{W} ({(E \circ g) ↾}_{\{1\}})$
313	312	a1d	$⊢ ((φ \land n \in ℕ) \land g \in S) \to (1 \in (1 \dots n) \to X E 2^{nd} (g (1)) \leq \sum_{W} ({(E \circ g) ↾}_{\{1\}}))$
314		simprl	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to x \in ℕ$
315	314 274	eleqtrdi	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to x \in ℤ_{\geq 1}$
316		simprr	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to x + 1 \in (1 \dots n)$
317		peano2fzr	$⊢ (x \in ℤ_{\geq 1} \land x + 1 \in (1 \dots n)) \to x \in (1 \dots n)$
318	315 316 317	syl2anc	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to x \in (1 \dots n)$
319	318	expr	$⊢ (((φ \land n \in ℕ) \land g \in S) \land x \in ℕ) \to (x + 1 \in (1 \dots n) \to x \in (1 \dots n))$
320	319	imim1d	$⊢ (((φ \land n \in ℕ) \land g \in S) \land x \in ℕ) \to ((x \in (1 \dots n) \to X E 2^{nd} (g (x)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)})) \to (x + 1 \in (1 \dots n) \to X E 2^{nd} (g (x)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)})))$
321	272	adantr	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to E \in ∞Met (V)$
322	273	adantr	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to X \in V$
323	49	adantr	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to g : (1 \dots n) ⟶ V \times V$
324	323 318	ffvelrnd	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to g (x) \in (V \times V)$
325		xp2nd	$⊢ g (x) \in (V \times V) \to 2^{nd} (g (x)) \in V$
326	324 325	syl	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to 2^{nd} (g (x)) \in V$
327		xmetcl	$⊢ (E \in ∞Met (V) \land X \in V \land 2^{nd} (g (x)) \in V) \to X E 2^{nd} (g (x)) \in ℝ^{*}$
328	321 322 326 327	syl3anc	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to X E 2^{nd} (g (x)) \in ℝ^{*}$
329	66	a1i	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to W \in CMnd$
330		fzfid	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (1 \dots x) \in Fin$
331	51	adantr	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (E \circ g) : (1 \dots n) ⟶ ℝ^{*} ∖ \{−∞\}$
332		fzsuc	$⊢ x \in ℤ_{\geq 1} \to (1 \dots x + 1) = (1 \dots x) \cup \{x + 1\}$
333	315 332	syl	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (1 \dots x + 1) = (1 \dots x) \cup \{x + 1\}$
334		elfzuz3	$⊢ x + 1 \in (1 \dots n) \to n \in ℤ_{\geq (x + 1)}$
335	334	ad2antll	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to n \in ℤ_{\geq (x + 1)}$
336		fzss2	$⊢ n \in ℤ_{\geq (x + 1)} \to (1 \dots x + 1) \subseteq (1 \dots n)$
337	335 336	syl	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (1 \dots x + 1) \subseteq (1 \dots n)$
338	333 337	eqsstrrd	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (1 \dots x) \cup \{x + 1\} \subseteq (1 \dots n)$
339	338	unssad	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (1 \dots x) \subseteq (1 \dots n)$
340	331 339	fssresd	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to ({(E \circ g) ↾}_{(1 \dots x)}) : (1 \dots x) ⟶ ℝ^{*} ∖ \{−∞\}$
341	68	a1i	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to 0 \in V$
342	340 330 341	fdmfifsupp	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to {finSupp}_{0} (({(E \circ g) ↾}_{(1 \dots x)}))$
343	64 65 329 330 340 342	gsumcl	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)}) \in (ℝ^{*} ∖ \{−∞\})$
344	343	eldifad	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)}) \in ℝ^{*}$
345	321 30	syl	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to E : V \times V ⟶ ℝ^{*}$
346	323 316	ffvelrnd	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to g (x + 1) \in (V \times V)$
347	345 346	ffvelrnd	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to E (g (x + 1)) \in ℝ^{*}$
348		xleadd1a	$⊢ ((X E 2^{nd} (g (x)) \in ℝ^{} \land \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)}) \in ℝ^{} \land E (g (x + 1)) \in ℝ^{*}) \land X E 2^{nd} (g (x)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)})) \to (X E 2^{nd} (g (x))) +_{𝑒} E (g (x + 1)) \leq (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1))$
349	348	ex	$⊢ (X E 2^{nd} (g (x)) \in ℝ^{} \land \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)}) \in ℝ^{} \land E (g (x + 1)) \in ℝ^{*}) \to (X E 2^{nd} (g (x)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)}) \to (X E 2^{nd} (g (x))) +_{𝑒} E (g (x + 1)) \leq (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1)))$
350	328 344 347 349	syl3anc	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (X E 2^{nd} (g (x)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)}) \to (X E 2^{nd} (g (x))) +_{𝑒} E (g (x + 1)) \leq (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1)))$
351		xp2nd	$⊢ g (x + 1) \in (V \times V) \to 2^{nd} (g (x + 1)) \in V$
352	346 351	syl	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to 2^{nd} (g (x + 1)) \in V$
353		xmettri	$⊢ (E \in ∞Met (V) \land (X \in V \land 2^{nd} (g (x + 1)) \in V \land 2^{nd} (g (x)) \in V)) \to X E 2^{nd} (g (x + 1)) \leq (X E 2^{nd} (g (x))) +_{𝑒} (2^{nd} (g (x)) E 2^{nd} (g (x + 1)))$
354	321 322 352 326 353	syl13anc	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to X E 2^{nd} (g (x + 1)) \leq (X E 2^{nd} (g (x))) +_{𝑒} (2^{nd} (g (x)) E 2^{nd} (g (x + 1)))$
355		1st2nd2	$⊢ g (x + 1) \in (V \times V) \to g (x + 1) = ⟨1^{st} (g (x + 1)), 2^{nd} (g (x + 1))⟩$
356	346 355	syl	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to g (x + 1) = ⟨1^{st} (g (x + 1)), 2^{nd} (g (x + 1))⟩$
357		2fveq3	$⊢ i = x \to 2^{nd} (g (i)) = 2^{nd} (g (x))$
358	357	fveq2d	$⊢ i = x \to F (2^{nd} (g (i))) = F (2^{nd} (g (x)))$
359		fvoveq1	$⊢ i = x \to g (i + 1) = g (x + 1)$
360	359	fveq2d	$⊢ i = x \to 1^{st} (g (i + 1)) = 1^{st} (g (x + 1))$
361	360	fveq2d	$⊢ i = x \to F (1^{st} (g (i + 1))) = F (1^{st} (g (x + 1)))$
362	358 361	eqeq12d	$⊢ i = x \to (F (2^{nd} (g (i))) = F (1^{st} (g (i + 1))) \leftrightarrow F (2^{nd} (g (x))) = F (1^{st} (g (x + 1))))$
363	219	simp3d	$⊢ ((φ \land n \in ℕ) \land g \in S) \to \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1)))$
364	363	adantr	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to \forall i \in (1 \dots n - 1) F (2^{nd} (g (i))) = F (1^{st} (g (i + 1)))$
365		nnz	$⊢ x \in ℕ \to x \in ℤ$
366	365	ad2antrl	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to x \in ℤ$
367		eluzp1m1	$⊢ (x \in ℤ \land n \in ℤ_{\geq (x + 1)}) \to n - 1 \in ℤ_{\geq x}$
368	366 335 367	syl2anc	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to n - 1 \in ℤ_{\geq x}$
369		elfzuzb	$⊢ x \in (1 \dots n - 1) \leftrightarrow (x \in ℤ_{\geq 1} \land n - 1 \in ℤ_{\geq x})$
370	315 368 369	sylanbrc	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to x \in (1 \dots n - 1)$
371	362 364 370	rspcdva	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to F (2^{nd} (g (x))) = F (1^{st} (g (x + 1)))$
372	223	adantr	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to F : V \underset{1-1}{⟶} B$
373		xp1st	$⊢ g (x + 1) \in (V \times V) \to 1^{st} (g (x + 1)) \in V$
374	346 373	syl	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to 1^{st} (g (x + 1)) \in V$
375		f1fveq	$⊢ (F : V \underset{1-1}{⟶} B \land (2^{nd} (g (x)) \in V \land 1^{st} (g (x + 1)) \in V)) \to (F (2^{nd} (g (x))) = F (1^{st} (g (x + 1))) \leftrightarrow 2^{nd} (g (x)) = 1^{st} (g (x + 1)))$
376	372 326 374 375	syl12anc	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (F (2^{nd} (g (x))) = F (1^{st} (g (x + 1))) \leftrightarrow 2^{nd} (g (x)) = 1^{st} (g (x + 1)))$
377	371 376	mpbid	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to 2^{nd} (g (x)) = 1^{st} (g (x + 1))$
378	377	opeq1d	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to ⟨2^{nd} (g (x)), 2^{nd} (g (x + 1))⟩ = ⟨1^{st} (g (x + 1)), 2^{nd} (g (x + 1))⟩$
379	356 378	eqtr4d	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to g (x + 1) = ⟨2^{nd} (g (x)), 2^{nd} (g (x + 1))⟩$
380	379	fveq2d	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to E (g (x + 1)) = E (⟨2^{nd} (g (x)), 2^{nd} (g (x + 1))⟩)$
381		df-ov	$⊢ 2^{nd} (g (x)) E 2^{nd} (g (x + 1)) = E (⟨2^{nd} (g (x)), 2^{nd} (g (x + 1))⟩)$
382	380 381	eqtr4di	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to E (g (x + 1)) = 2^{nd} (g (x)) E 2^{nd} (g (x + 1))$
383	382	oveq2d	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (X E 2^{nd} (g (x))) +_{𝑒} E (g (x + 1)) = (X E 2^{nd} (g (x))) +_{𝑒} (2^{nd} (g (x)) E 2^{nd} (g (x + 1)))$
384	354 383	breqtrrd	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to X E 2^{nd} (g (x + 1)) \leq (X E 2^{nd} (g (x))) +_{𝑒} E (g (x + 1))$
385		xmetcl	$⊢ (E \in ∞Met (V) \land X \in V \land 2^{nd} (g (x + 1)) \in V) \to X E 2^{nd} (g (x + 1)) \in ℝ^{*}$
386	321 322 352 385	syl3anc	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to X E 2^{nd} (g (x + 1)) \in ℝ^{*}$
387	328 347	xaddcld	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (X E 2^{nd} (g (x))) +_{𝑒} E (g (x + 1)) \in ℝ^{*}$
388	344 347	xaddcld	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1)) \in ℝ^{*}$
389		xrletr	$⊢ (X E 2^{nd} (g (x + 1)) \in ℝ^{} \land (X E 2^{nd} (g (x))) +_{𝑒} E (g (x + 1)) \in ℝ^{} \land (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1)) \in ℝ^{*}) \to ((X E 2^{nd} (g (x + 1)) \leq (X E 2^{nd} (g (x))) +_{𝑒} E (g (x + 1)) \land (X E 2^{nd} (g (x))) +_{𝑒} E (g (x + 1)) \leq (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1))) \to X E 2^{nd} (g (x + 1)) \leq (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1)))$
390	386 387 388 389	syl3anc	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to ((X E 2^{nd} (g (x + 1)) \leq (X E 2^{nd} (g (x))) +_{𝑒} E (g (x + 1)) \land (X E 2^{nd} (g (x))) +_{𝑒} E (g (x + 1)) \leq (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1))) \to X E 2^{nd} (g (x + 1)) \leq (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1)))$
391	384 390	mpand	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to ((X E 2^{nd} (g (x))) +_{𝑒} E (g (x + 1)) \leq (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1)) \to X E 2^{nd} (g (x + 1)) \leq (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1)))$
392	350 391	syld	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (X E 2^{nd} (g (x)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)}) \to X E 2^{nd} (g (x + 1)) \leq (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1)))$
393		xrex	$⊢ ℝ^{*} \in V$
394	393	difexi	$⊢ ℝ^{*} ∖ \{−∞\} \in V$
395	10 24	ressplusg	$⊢ ℝ^{*} ∖ \{−∞\} \in V \to +_{𝑒} = +_{W}$
396	394 395	ax-mp	$⊢ +_{𝑒} = +_{W}$
397	44	ad2antrr	$⊢ ((((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \land j \in (1 \dots x)) \to E : V \times V ⟶ ℝ^{*} ∖ \{−∞\}$
398		fzelp1	$⊢ j \in (1 \dots x) \to j \in (1 \dots x + 1)$
399	49	ad2antrr	$⊢ ((((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \land j \in (1 \dots x + 1)) \to g : (1 \dots n) ⟶ V \times V$
400	337	sselda	$⊢ ((((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \land j \in (1 \dots x + 1)) \to j \in (1 \dots n)$
401	399 400	ffvelrnd	$⊢ ((((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \land j \in (1 \dots x + 1)) \to g (j) \in (V \times V)$
402	398 401	sylan2	$⊢ ((((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \land j \in (1 \dots x)) \to g (j) \in (V \times V)$
403	397 402	ffvelrnd	$⊢ ((((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \land j \in (1 \dots x)) \to E (g (j)) \in (ℝ^{*} ∖ \{−∞\})$
404		fzp1disj	$⊢ (1 \dots x) \cap \{x + 1\} = \emptyset$
405	404	a1i	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (1 \dots x) \cap \{x + 1\} = \emptyset$
406		disjsn	$⊢ (1 \dots x) \cap \{x + 1\} = \emptyset \leftrightarrow \neg x + 1 \in (1 \dots x)$
407	405 406	sylib	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to \neg x + 1 \in (1 \dots x)$
408	44	adantr	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to E : V \times V ⟶ ℝ^{*} ∖ \{−∞\}$
409	408 346	ffvelrnd	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to E (g (x + 1)) \in (ℝ^{*} ∖ \{−∞\})$
410		2fveq3	$⊢ j = x + 1 \to E (g (j)) = E (g (x + 1))$
411	64 396 329 330 403 316 407 409 410	gsumunsn	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to \underset{j \in (1 \dots x) \cup \{x + 1\}}{\sum_{W}} E (g (j)) = ({\sum_{W}}_{j = 1}^{x}, E (g (j))) +_{𝑒} E (g (x + 1))$
412	292	adantr	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to E \circ g = (j \in (1 \dots n) ⟼ E (g (j)))$
413	412 333	reseq12d	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to {(E \circ g) ↾}_{(1 \dots x + 1)} = {(j \in (1 \dots n) ⟼ E (g (j))) ↾}_{((1 \dots x) \cup \{x + 1\})}$
414	338	resmptd	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to {(j \in (1 \dots n) ⟼ E (g (j))) ↾}_{((1 \dots x) \cup \{x + 1\})} = (j \in ((1 \dots x) \cup \{x + 1\}) ⟼ E (g (j)))$
415	413 414	eqtrd	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to {(E \circ g) ↾}_{(1 \dots x + 1)} = (j \in ((1 \dots x) \cup \{x + 1\}) ⟼ E (g (j)))$
416	415	oveq2d	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to \sum_{W} ({(E \circ g) ↾}_{(1 \dots x + 1)}) = \underset{j \in (1 \dots x) \cup \{x + 1\}}{\sum_{W}} E (g (j))$
417	412	reseq1d	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to {(E \circ g) ↾}_{(1 \dots x)} = {(j \in (1 \dots n) ⟼ E (g (j))) ↾}_{(1 \dots x)}$
418	339	resmptd	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to {(j \in (1 \dots n) ⟼ E (g (j))) ↾}_{(1 \dots x)} = (j \in (1 \dots x) ⟼ E (g (j)))$
419	417 418	eqtrd	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to {(E \circ g) ↾}_{(1 \dots x)} = (j \in (1 \dots x) ⟼ E (g (j)))$
420	419	oveq2d	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)}) = {\sum_{W}}_{j = 1}^{x} E (g (j))$
421	420	oveq1d	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1)) = ({\sum_{W}}_{j = 1}^{x}, E (g (j))) +_{𝑒} E (g (x + 1))$
422	411 416 421	3eqtr4d	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to \sum_{W} ({(E \circ g) ↾}_{(1 \dots x + 1)}) = (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1))$
423	422	breq2d	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (X E 2^{nd} (g (x + 1)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x + 1)}) \leftrightarrow X E 2^{nd} (g (x + 1)) \leq (\sum_{W}, ({(E \circ g) ↾}_{(1 \dots x)})) +_{𝑒} E (g (x + 1)))$
424	392 423	sylibrd	$⊢ (((φ \land n \in ℕ) \land g \in S) \land (x \in ℕ \land x + 1 \in (1 \dots n))) \to (X E 2^{nd} (g (x)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)}) \to X E 2^{nd} (g (x + 1)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x + 1)}))$
425	320 424	animpimp2impd	$⊢ x \in ℕ \to ((((φ \land n \in ℕ) \land g \in S) \to (x \in (1 \dots n) \to X E 2^{nd} (g (x)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x)}))) \to (((φ \land n \in ℕ) \land g \in S) \to (x + 1 \in (1 \dots n) \to X E 2^{nd} (g (x + 1)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots x + 1)}))))$
426	244 253 262 271 313 425	nnind	$⊢ n \in ℕ \to (((φ \land n \in ℕ) \land g \in S) \to (n \in (1 \dots n) \to X E 2^{nd} (g (n)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots n)})))$
427	224 426	mpcom	$⊢ ((φ \land n \in ℕ) \land g \in S) \to (n \in (1 \dots n) \to X E 2^{nd} (g (n)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots n)}))$
428	226 427	mpd	$⊢ ((φ \land n \in ℕ) \land g \in S) \to X E 2^{nd} (g (n)) \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots n)})$
429	234 428	eqbrtrrd	$⊢ ((φ \land n \in ℕ) \land g \in S) \to X E Y \leq \sum_{W} ({(E \circ g) ↾}_{(1 \dots n)})$
430		ffn	$⊢ (E \circ g) : (1 \dots n) ⟶ ℝ^{*} ∖ \{−∞\} \to (E \circ g) Fn (1 \dots n)$
431		fnresdm	$⊢ (E \circ g) Fn (1 \dots n) \to {(E \circ g) ↾}_{(1 \dots n)} = E \circ g$
432	51 430 431	3syl	$⊢ ((φ \land n \in ℕ) \land g \in S) \to {(E \circ g) ↾}_{(1 \dots n)} = E \circ g$
433	432	oveq2d	$⊢ ((φ \land n \in ℕ) \land g \in S) \to \sum_{W} ({(E \circ g) ↾}_{(1 \dots n)}) = \sum_{W} (E \circ g)$
434	62 433	eqtr4d	$⊢ ((φ \land n \in ℕ) \land g \in S) \to \sum_{ℝ_{𝑠}^{*}} (E \circ g) = \sum_{W} ({(E \circ g) ↾}_{(1 \dots n)})$
435	429 434	breqtrrd	$⊢ ((φ \land n \in ℕ) \land g \in S) \to X E Y \leq \sum_{ℝ_{𝑠}^{*}} (E \circ g)$
436		breq2	$⊢ p = \sum_{ℝ_{𝑠}^{}} (E \circ g) \to (X E Y \leq p \leftrightarrow X E Y \leq \sum_{ℝ_{𝑠}^{}} (E \circ g))$
437	435 436	syl5ibrcom	$⊢ ((φ \land n \in ℕ) \land g \in S) \to (p = \sum_{ℝ_{𝑠}^{*}} (E \circ g) \to X E Y \leq p)$
438	437	rexlimdva	$⊢ (φ \land n \in ℕ) \to (\exists g \in S p = \sum_{ℝ_{𝑠}^{*}} (E \circ g) \to X E Y \leq p)$
439	216 438	syl5bi	$⊢ (φ \land n \in ℕ) \to (p \in ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{*}} (E \circ g)) \to X E Y \leq p)$
440	439	rexlimdva	$⊢ φ \to (\exists n \in ℕ p \in ran (g \in S ⟼ \sum_{ℝ_{𝑠}^{*}} (E \circ g)) \to X E Y \leq p)$
441	214 440	syl5bi	$⊢ φ \to (p \in T \to X E Y \leq p)$
442	441	ralrimiv	$⊢ φ \to \forall p \in T X E Y \leq p$
443		infxrgelb	$⊢ (T \subseteq ℝ^{} \land X E Y \in ℝ^{}) \to (X E Y \leq sup (T ℝ^{*} <) \leftrightarrow \forall p \in T X E Y \leq p)$
444	79 83 443	syl2anc	$⊢ φ \to (X E Y \leq sup (T ℝ^{*} <) \leftrightarrow \forall p \in T X E Y \leq p)$
445	442 444	mpbird	$⊢ φ \to X E Y \leq sup (T ℝ^{*} <)$
446	81 83 211 445	xrletrid	$⊢ φ \to sup (T ℝ^{*} <) = X E Y$
447	22 446	eqtrd	$⊢ φ \to F (X) D F (Y) = X E Y$

Metamath Proof Explorer

Theorem imasdsf1olem

Proof