hspmbllem2

Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (b) of Lemma 115F of Fremlin1 p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	hspmbllem2.h	$⊢ H = (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{k \in x}{⨉} if (k = l, (−∞, y), ℝ)))$
	hspmbllem2.x	$⊢ φ \to X \in Fin$
	hspmbllem2.k	$⊢ φ \to K \in X$
	hspmbllem2.y	$⊢ φ \to Y \in ℝ$
	hspmbllem2.e	$⊢ φ \to E \in ℝ^{+}$
	hspmbllem2.c	$⊢ φ \to C : ℕ ⟶ ℝ^{X}$
	hspmbllem2.d	$⊢ φ \to D : ℕ ⟶ ℝ^{X}$
	hspmbllem2.a	$⊢ φ \to A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
	hspmbllem2.g	$⊢ φ \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([C (j) (k), D (j) (k))))) \leq voln* (X) (A) + E$
	hspmbllem2.r	$⊢ φ \to voln* (X) (A) \in ℝ$
	hspmbllem2.i	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) \in ℝ$
	hspmbllem2.f	$⊢ φ \to voln* (X) (A ∖ (K H (X) Y)) \in ℝ$
	hspmbllem2.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
	hspmbllem2.t	$⊢ T = (y \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y)))))$
	hspmbllem2.s	$⊢ S = (x \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h = K, if (x \leq c (h), c (h), x), c (h)))))$
Assertion	hspmbllem2	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A) + E$

Proof

Step	Hyp	Ref	Expression
1		hspmbllem2.h	$⊢ H = (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{k \in x}{⨉} if (k = l, (−∞, y), ℝ)))$
2		hspmbllem2.x	$⊢ φ \to X \in Fin$
3		hspmbllem2.k	$⊢ φ \to K \in X$
4		hspmbllem2.y	$⊢ φ \to Y \in ℝ$
5		hspmbllem2.e	$⊢ φ \to E \in ℝ^{+}$
6		hspmbllem2.c	$⊢ φ \to C : ℕ ⟶ ℝ^{X}$
7		hspmbllem2.d	$⊢ φ \to D : ℕ ⟶ ℝ^{X}$
8		hspmbllem2.a	$⊢ φ \to A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
9		hspmbllem2.g	$⊢ φ \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([C (j) (k), D (j) (k))))) \leq voln* (X) (A) + E$
10		hspmbllem2.r	$⊢ φ \to voln* (X) (A) \in ℝ$
11		hspmbllem2.i	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) \in ℝ$
12		hspmbllem2.f	$⊢ φ \to voln* (X) (A ∖ (K H (X) Y)) \in ℝ$
13		hspmbllem2.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
14		hspmbllem2.t	$⊢ T = (y \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y)))))$
15		hspmbllem2.s	$⊢ S = (x \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h = K, if (x \leq c (h), c (h), x), c (h)))))$
16	11 12	readdcld	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \in ℝ$
17	5	rpred	$⊢ φ \to E \in ℝ$
18	10 17	readdcld	$⊢ φ \to voln* (X) (A) + E \in ℝ$
19		nfv	$⊢ Ⅎ j φ$
20		nnex	$⊢ ℕ \in V$
21	20	a1i	$⊢ φ \to ℕ \in V$
22		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
23	2	adantr	$⊢ (φ \land j \in ℕ) \to X \in Fin$
24	6	ffvelcdmda	$⊢ (φ \land j \in ℕ) \to C (j) \in (ℝ^{X})$
25		elmapi	$⊢ C (j) \in (ℝ^{X}) \to C (j) : X ⟶ ℝ$
26	24 25	syl	$⊢ (φ \land j \in ℕ) \to C (j) : X ⟶ ℝ$
27	7	ffvelcdmda	$⊢ (φ \land j \in ℕ) \to D (j) \in (ℝ^{X})$
28		elmapi	$⊢ D (j) \in (ℝ^{X}) \to D (j) : X ⟶ ℝ$
29	27 28	syl	$⊢ (φ \land j \in ℕ) \to D (j) : X ⟶ ℝ$
30	13 23 26 29	hoidmvcl	$⊢ (φ \land j \in ℕ) \to C (j) L (X) D (j) \in [0, +∞)$
31	22 30	sselid	$⊢ (φ \land j \in ℕ) \to C (j) L (X) D (j) \in [0, +∞]$
32	19 21 31	sge0clmpt	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (X) D (j))) \in [0, +∞]$
33		ne0i	$⊢ K \in X \to X \neq \emptyset$
34	3 33	syl	$⊢ φ \to X \neq \emptyset$
35	34	adantr	$⊢ (φ \land j \in ℕ) \to X \neq \emptyset$
36	13 23 35 26 29	hoidmvn0val	$⊢ (φ \land j \in ℕ) \to C (j) L (X) D (j) = \prod_{k \in X} vol ([C (j) (k), D (j) (k)))$
37	36	mpteq2dva	$⊢ φ \to (j \in ℕ ⟼ C (j) L (X) D (j)) = (j \in ℕ ⟼ \prod_{k \in X} vol ([C (j) (k), D (j) (k))))$
38	37	fveq2d	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([C (j) (k), D (j) (k)))))$
39	38 9	eqbrtrd	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (X) D (j))) \leq voln* (X) (A) + E$
40	18 32 39	ge0lere	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (X) D (j))) \in ℝ$
41	4	adantr	$⊢ (φ \land j \in ℕ) \to Y \in ℝ$
42	14 41 23 29	hsphoif	$⊢ (φ \land j \in ℕ) \to T (Y) (D (j)) : X ⟶ ℝ$
43	13 23 26 42	hoidmvcl	$⊢ (φ \land j \in ℕ) \to C (j) L (X) T (Y) (D (j)) \in [0, +∞)$
44	22 43	sselid	$⊢ (φ \land j \in ℕ) \to C (j) L (X) T (Y) (D (j)) \in [0, +∞]$
45	19 21 44	sge0clmpt	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (X) T (Y) (D (j)))) \in [0, +∞]$
46		oveq2	$⊢ x = y \to ℝ^{x} = ℝ^{y}$
47		eqeq1	$⊢ x = y \to (x = \emptyset \leftrightarrow y = \emptyset)$
48		prodeq1	$⊢ x = y \to \prod_{k \in x} vol ([a (k), b (k))) = \prod_{k \in y} vol ([a (k), b (k)))$
49	47 48	ifbieq2d	$⊢ x = y \to if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k)))) = if (y = \emptyset, 0, \prod_{k \in y} vol ([a (k), b (k))))$
50	46 46 49	mpoeq123dv	$⊢ x = y \to (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))) = (a \in (ℝ^{y}), b \in (ℝ^{y}) ⟼ if (y = \emptyset, 0, \prod_{k \in y} vol ([a (k), b (k)))))$
51	50	cbvmptv	$⊢ (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k)))))) = (y \in Fin ⟼ (a \in (ℝ^{y}), b \in (ℝ^{y}) ⟼ if (y = \emptyset, 0, \prod_{k \in y} vol ([a (k), b (k))))))$
52	13 51	eqtri	$⊢ L = (y \in Fin ⟼ (a \in (ℝ^{y}), b \in (ℝ^{y}) ⟼ if (y = \emptyset, 0, \prod_{k \in y} vol ([a (k), b (k))))))$
53		diffi	$⊢ X \in Fin \to X ∖ \{K\} \in Fin$
54	2 53	syl	$⊢ φ \to X ∖ \{K\} \in Fin$
55		snfi	$⊢ \{K\} \in Fin$
56	55	a1i	$⊢ φ \to \{K\} \in Fin$
57		unfi	$⊢ (X ∖ \{K\} \in Fin \land \{K\} \in Fin) \to (X ∖ \{K\}) \cup \{K\} \in Fin$
58	54 56 57	syl2anc	$⊢ φ \to (X ∖ \{K\}) \cup \{K\} \in Fin$
59	58	adantr	$⊢ (φ \land j \in ℕ) \to (X ∖ \{K\}) \cup \{K\} \in Fin$
60		snidg	$⊢ K \in X \to K \in \{K\}$
61	3 60	syl	$⊢ φ \to K \in \{K\}$
62		elun2	$⊢ K \in \{K\} \to K \in ((X ∖ \{K\}) \cup \{K\})$
63	61 62	syl	$⊢ φ \to K \in ((X ∖ \{K\}) \cup \{K\})$
64		neldifsnd	$⊢ φ \to \neg K \in (X ∖ \{K\})$
65	63 64	eldifd	$⊢ φ \to K \in (((X ∖ \{K\}) \cup \{K\}) ∖ (X ∖ \{K\}))$
66	65	adantr	$⊢ (φ \land j \in ℕ) \to K \in (((X ∖ \{K\}) \cup \{K\}) ∖ (X ∖ \{K\}))$
67		eqid	$⊢ (X ∖ \{K\}) \cup \{K\} = (X ∖ \{K\}) \cup \{K\}$
68		eqid	$⊢ (y \in ℝ ⟼ (c \in (ℝ^{((X ∖ \{K\}) \cup \{K\})}) ⟼ (h \in ((X ∖ \{K\}) \cup \{K\}) ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y))))) = (y \in ℝ ⟼ (c \in (ℝ^{((X ∖ \{K\}) \cup \{K\})}) ⟼ (h \in ((X ∖ \{K\}) \cup \{K\}) ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y)))))$
69		uncom	$⊢ (X ∖ \{K\}) \cup \{K\} = \{K\} \cup (X ∖ \{K\})$
70	69	a1i	$⊢ φ \to (X ∖ \{K\}) \cup \{K\} = \{K\} \cup (X ∖ \{K\})$
71	3	snssd	$⊢ φ \to \{K\} \subseteq X$
72		undif	$⊢ \{K\} \subseteq X \leftrightarrow \{K\} \cup (X ∖ \{K\}) = X$
73	71 72	sylib	$⊢ φ \to \{K\} \cup (X ∖ \{K\}) = X$
74	70 73	eqtrd	$⊢ φ \to (X ∖ \{K\}) \cup \{K\} = X$
75	74	adantr	$⊢ (φ \land j \in ℕ) \to (X ∖ \{K\}) \cup \{K\} = X$
76	75	feq2d	$⊢ (φ \land j \in ℕ) \to (C (j) : (X ∖ \{K\}) \cup \{K\} ⟶ ℝ \leftrightarrow C (j) : X ⟶ ℝ)$
77	26 76	mpbird	$⊢ (φ \land j \in ℕ) \to C (j) : (X ∖ \{K\}) \cup \{K\} ⟶ ℝ$
78	75	feq2d	$⊢ (φ \land j \in ℕ) \to (D (j) : (X ∖ \{K\}) \cup \{K\} ⟶ ℝ \leftrightarrow D (j) : X ⟶ ℝ)$
79	29 78	mpbird	$⊢ (φ \land j \in ℕ) \to D (j) : (X ∖ \{K\}) \cup \{K\} ⟶ ℝ$
80	52 59 66 67 41 68 77 79	hsphoidmvle	$⊢ (φ \land j \in ℕ) \to C (j) L ((X ∖ \{K\}) \cup \{K\}) (y \in ℝ ⟼ (c \in (ℝ^{((X ∖ \{K\}) \cup \{K\})}) ⟼ (h \in ((X ∖ \{K\}) \cup \{K\}) ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y))))) (Y) (D (j)) \leq C (j) L ((X ∖ \{K\}) \cup \{K\}) D (j)$
81	74	fveq2d	$⊢ φ \to L ((X ∖ \{K\}) \cup \{K\}) = L (X)$
82		eqidd	$⊢ φ \to C (j) = C (j)$
83	14	a1i	$⊢ φ \to T = (y \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y)))))$
84	74	oveq2d	$⊢ φ \to ℝ^{((X ∖ \{K\}) \cup \{K\})} = ℝ^{X}$
85	74	mpteq1d	$⊢ φ \to (h \in ((X ∖ \{K\}) \cup \{K\}) ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y))) = (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y)))$
86	84 85	mpteq12dv	$⊢ φ \to (c \in (ℝ^{((X ∖ \{K\}) \cup \{K\})}) ⟼ (h \in ((X ∖ \{K\}) \cup \{K\}) ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y)))) = (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y))))$
87	86	eqcomd	$⊢ φ \to (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y)))) = (c \in (ℝ^{((X ∖ \{K\}) \cup \{K\})}) ⟼ (h \in ((X ∖ \{K\}) \cup \{K\}) ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y))))$
88	87	mpteq2dv	$⊢ φ \to (y \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y))))) = (y \in ℝ ⟼ (c \in (ℝ^{((X ∖ \{K\}) \cup \{K\})}) ⟼ (h \in ((X ∖ \{K\}) \cup \{K\}) ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y)))))$
89	83 88	eqtr2d	$⊢ φ \to (y \in ℝ ⟼ (c \in (ℝ^{((X ∖ \{K\}) \cup \{K\})}) ⟼ (h \in ((X ∖ \{K\}) \cup \{K\}) ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y))))) = T$
90	89	fveq1d	$⊢ φ \to (y \in ℝ ⟼ (c \in (ℝ^{((X ∖ \{K\}) \cup \{K\})}) ⟼ (h \in ((X ∖ \{K\}) \cup \{K\}) ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y))))) (Y) = T (Y)$
91	90	fveq1d	$⊢ φ \to (y \in ℝ ⟼ (c \in (ℝ^{((X ∖ \{K\}) \cup \{K\})}) ⟼ (h \in ((X ∖ \{K\}) \cup \{K\}) ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y))))) (Y) (D (j)) = T (Y) (D (j))$
92	81 82 91	oveq123d	$⊢ φ \to C (j) L ((X ∖ \{K\}) \cup \{K\}) (y \in ℝ ⟼ (c \in (ℝ^{((X ∖ \{K\}) \cup \{K\})}) ⟼ (h \in ((X ∖ \{K\}) \cup \{K\}) ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y))))) (Y) (D (j)) = C (j) L (X) T (Y) (D (j))$
93	92	adantr	$⊢ (φ \land j \in ℕ) \to C (j) L ((X ∖ \{K\}) \cup \{K\}) (y \in ℝ ⟼ (c \in (ℝ^{((X ∖ \{K\}) \cup \{K\})}) ⟼ (h \in ((X ∖ \{K\}) \cup \{K\}) ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y))))) (Y) (D (j)) = C (j) L (X) T (Y) (D (j))$
94	81	adantr	$⊢ (φ \land j \in ℕ) \to L ((X ∖ \{K\}) \cup \{K\}) = L (X)$
95	94	oveqd	$⊢ (φ \land j \in ℕ) \to C (j) L ((X ∖ \{K\}) \cup \{K\}) D (j) = C (j) L (X) D (j)$
96	93 95	breq12d	$⊢ (φ \land j \in ℕ) \to (C (j) L ((X ∖ \{K\}) \cup \{K\}) (y \in ℝ ⟼ (c \in (ℝ^{((X ∖ \{K\}) \cup \{K\})}) ⟼ (h \in ((X ∖ \{K\}) \cup \{K\}) ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y))))) (Y) (D (j)) \leq C (j) L ((X ∖ \{K\}) \cup \{K\}) D (j) \leftrightarrow C (j) L (X) T (Y) (D (j)) \leq C (j) L (X) D (j))$
97	80 96	mpbid	$⊢ (φ \land j \in ℕ) \to C (j) L (X) T (Y) (D (j)) \leq C (j) L (X) D (j)$
98	19 21 44 31 97	sge0lempt	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (X) T (Y) (D (j)))) \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
99	40 45 98	ge0lere	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (X) T (Y) (D (j)))) \in ℝ$
100	15 41 23 26	hoidifhspf	$⊢ (φ \land j \in ℕ) \to S (Y) (C (j)) : X ⟶ ℝ$
101	13 23 100 29	hoidmvcl	$⊢ (φ \land j \in ℕ) \to S (Y) (C (j)) L (X) D (j) \in [0, +∞)$
102	101	fmpttd	$⊢ φ \to (j \in ℕ ⟼ S (Y) (C (j)) L (X) D (j)) : ℕ ⟶ [0, +∞)$
103	22	a1i	$⊢ φ \to [0, +∞) \subseteq [0, +∞]$
104	102 103	fssd	$⊢ φ \to (j \in ℕ ⟼ S (Y) (C (j)) L (X) D (j)) : ℕ ⟶ [0, +∞]$
105	21 104	sge0cl	$⊢ φ \to sum^((j \in ℕ ⟼ S (Y) (C (j)) L (X) D (j))) \in [0, +∞]$
106	22 101	sselid	$⊢ (φ \land j \in ℕ) \to S (Y) (C (j)) L (X) D (j) \in [0, +∞]$
107	3	adantr	$⊢ (φ \land j \in ℕ) \to K \in X$
108	13 23 26 29 107 15 41	hoidifhspdmvle	$⊢ (φ \land j \in ℕ) \to S (Y) (C (j)) L (X) D (j) \leq C (j) L (X) D (j)$
109	19 21 106 31 108	sge0lempt	$⊢ φ \to sum^((j \in ℕ ⟼ S (Y) (C (j)) L (X) D (j))) \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
110	40 105 109	ge0lere	$⊢ φ \to sum^((j \in ℕ ⟼ S (Y) (C (j)) L (X) D (j))) \in ℝ$
111	4	adantr	$⊢ (φ \land l \in ℕ) \to Y \in ℝ$
112	2	adantr	$⊢ (φ \land l \in ℕ) \to X \in Fin$
113		eleq1w	$⊢ j = l \to (j \in ℕ \leftrightarrow l \in ℕ)$
114	113	anbi2d	$⊢ j = l \to ((φ \land j \in ℕ) \leftrightarrow (φ \land l \in ℕ))$
115		fveq2	$⊢ j = l \to D (j) = D (l)$
116	115	feq1d	$⊢ j = l \to (D (j) : X ⟶ ℝ \leftrightarrow D (l) : X ⟶ ℝ)$
117	114 116	imbi12d	$⊢ j = l \to (((φ \land j \in ℕ) \to D (j) : X ⟶ ℝ) \leftrightarrow ((φ \land l \in ℕ) \to D (l) : X ⟶ ℝ))$
118	117 29	chvarvv	$⊢ (φ \land l \in ℕ) \to D (l) : X ⟶ ℝ$
119	14 111 112 118	hsphoif	$⊢ (φ \land l \in ℕ) \to T (Y) (D (l)) : X ⟶ ℝ$
120		reex	$⊢ ℝ \in V$
121	120	a1i	$⊢ φ \to ℝ \in V$
122	121 2	jca	$⊢ φ \to (ℝ \in V \land X \in Fin)$
123	122	adantr	$⊢ (φ \land l \in ℕ) \to (ℝ \in V \land X \in Fin)$
124		elmapg	$⊢ (ℝ \in V \land X \in Fin) \to (T (Y) (D (l)) \in (ℝ^{X}) \leftrightarrow T (Y) (D (l)) : X ⟶ ℝ)$
125	123 124	syl	$⊢ (φ \land l \in ℕ) \to (T (Y) (D (l)) \in (ℝ^{X}) \leftrightarrow T (Y) (D (l)) : X ⟶ ℝ)$
126	119 125	mpbird	$⊢ (φ \land l \in ℕ) \to T (Y) (D (l)) \in (ℝ^{X})$
127	126	fmpttd	$⊢ φ \to (l \in ℕ ⟼ T (Y) (D (l))) : ℕ ⟶ ℝ^{X}$
128		simpl	$⊢ (φ \land f \in (A \cap (K H (X) Y))) \to φ$
129		elinel1	$⊢ f \in (A \cap (K H (X) Y)) \to f \in A$
130	129	adantl	$⊢ (φ \land f \in (A \cap (K H (X) Y))) \to f \in A$
131	8	sselda	$⊢ (φ \land f \in A) \to f \in ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
132		eliun	$⊢ f \in ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \leftrightarrow \exists j \in ℕ f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
133	131 132	sylib	$⊢ (φ \land f \in A) \to \exists j \in ℕ f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
134	128 130 133	syl2anc	$⊢ (φ \land f \in (A \cap (K H (X) Y))) \to \exists j \in ℕ f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
135		simpll	$⊢ ((φ \land f \in (A \cap (K H (X) Y))) \land j \in ℕ) \to φ$
136		elinel2	$⊢ f \in (A \cap (K H (X) Y)) \to f \in (K H (X) Y)$
137	136	adantl	$⊢ (φ \land f \in (A \cap (K H (X) Y))) \to f \in (K H (X) Y)$
138	137	adantr	$⊢ ((φ \land f \in (A \cap (K H (X) Y))) \land j \in ℕ) \to f \in (K H (X) Y)$
139		simpr	$⊢ ((φ \land f \in (A \cap (K H (X) Y))) \land j \in ℕ) \to j \in ℕ$
140		ixpfn	$⊢ f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \to f Fn X$
141	140	adantl	$⊢ (((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to f Fn X$
142		nfv	$⊢ Ⅎ k ((φ \land f \in (K H (X) Y)) \land j \in ℕ)$
143		nfcv	$⊢ \underline{Ⅎ} k f$
144		nfixp1	$⊢ \underline{Ⅎ} k \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
145	143 144	nfel	$⊢ Ⅎ k f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
146	142 145	nfan	$⊢ Ⅎ k (((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)))$
147	26	3adant3	$⊢ (φ \land j \in ℕ \land k \in X) \to C (j) : X ⟶ ℝ$
148		simp3	$⊢ (φ \land j \in ℕ \land k \in X) \to k \in X$
149	147 148	ffvelcdmd	$⊢ (φ \land j \in ℕ \land k \in X) \to C (j) (k) \in ℝ$
150	149	rexrd	$⊢ (φ \land j \in ℕ \land k \in X) \to C (j) (k) \in ℝ^{*}$
151	150	ad5ant135	$⊢ ((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to C (j) (k) \in ℝ^{*}$
152	42	3adant3	$⊢ (φ \land j \in ℕ \land k \in X) \to T (Y) (D (j)) : X ⟶ ℝ$
153	152 148	ffvelcdmd	$⊢ (φ \land j \in ℕ \land k \in X) \to T (Y) (D (j)) (k) \in ℝ$
154	153	rexrd	$⊢ (φ \land j \in ℕ \land k \in X) \to T (Y) (D (j)) (k) \in ℝ^{*}$
155	154	ad5ant135	$⊢ ((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to T (Y) (D (j)) (k) \in ℝ^{*}$
156		iftrue	$⊢ k = K \to if (k = K, (−∞, Y), ℝ) = (−∞, Y)$
157		ioossre	$⊢ (−∞, Y) \subseteq ℝ$
158	157	a1i	$⊢ k = K \to (−∞, Y) \subseteq ℝ$
159	156 158	eqsstrd	$⊢ k = K \to if (k = K, (−∞, Y), ℝ) \subseteq ℝ$
160		iffalse	$⊢ \neg k = K \to if (k = K, (−∞, Y), ℝ) = ℝ$
161		ssid	$⊢ ℝ \subseteq ℝ$
162	161	a1i	$⊢ \neg k = K \to ℝ \subseteq ℝ$
163	160 162	eqsstrd	$⊢ \neg k = K \to if (k = K, (−∞, Y), ℝ) \subseteq ℝ$
164	159 163	pm2.61i	$⊢ if (k = K, (−∞, Y), ℝ) \subseteq ℝ$
165		simpr	$⊢ (φ \land f \in (K H (X) Y)) \to f \in (K H (X) Y)$
166	1 2 3 4	hspval	$⊢ φ \to K H (X) Y = \underset{k \in X}{⨉} if (k = K, (−∞, Y), ℝ)$
167	166	adantr	$⊢ (φ \land f \in (K H (X) Y)) \to K H (X) Y = \underset{k \in X}{⨉} if (k = K, (−∞, Y), ℝ)$
168	165 167	eleqtrd	$⊢ (φ \land f \in (K H (X) Y)) \to f \in \underset{k \in X}{⨉} if (k = K, (−∞, Y), ℝ)$
169	168	adantr	$⊢ ((φ \land f \in (K H (X) Y)) \land k \in X) \to f \in \underset{k \in X}{⨉} if (k = K, (−∞, Y), ℝ)$
170		simpr	$⊢ ((φ \land f \in (K H (X) Y)) \land k \in X) \to k \in X$
171		vex	$⊢ f \in V$
172	171	elixp	$⊢ f \in \underset{k \in X}{⨉} if (k = K, (−∞, Y), ℝ) \leftrightarrow (f Fn X \land \forall k \in X f (k) \in if (k = K, (−∞, Y), ℝ))$
173	172	biimpi	$⊢ f \in \underset{k \in X}{⨉} if (k = K, (−∞, Y), ℝ) \to (f Fn X \land \forall k \in X f (k) \in if (k = K, (−∞, Y), ℝ))$
174	173	simprd	$⊢ f \in \underset{k \in X}{⨉} if (k = K, (−∞, Y), ℝ) \to \forall k \in X f (k) \in if (k = K, (−∞, Y), ℝ)$
175	174	adantr	$⊢ (f \in \underset{k \in X}{⨉} if (k = K, (−∞, Y), ℝ) \land k \in X) \to \forall k \in X f (k) \in if (k = K, (−∞, Y), ℝ)$
176		simpr	$⊢ (f \in \underset{k \in X}{⨉} if (k = K, (−∞, Y), ℝ) \land k \in X) \to k \in X$
177		rspa	$⊢ (\forall k \in X f (k) \in if (k = K, (−∞, Y), ℝ) \land k \in X) \to f (k) \in if (k = K, (−∞, Y), ℝ)$
178	175 176 177	syl2anc	$⊢ (f \in \underset{k \in X}{⨉} if (k = K, (−∞, Y), ℝ) \land k \in X) \to f (k) \in if (k = K, (−∞, Y), ℝ)$
179	169 170 178	syl2anc	$⊢ ((φ \land f \in (K H (X) Y)) \land k \in X) \to f (k) \in if (k = K, (−∞, Y), ℝ)$
180	164 179	sselid	$⊢ ((φ \land f \in (K H (X) Y)) \land k \in X) \to f (k) \in ℝ$
181	180	rexrd	$⊢ ((φ \land f \in (K H (X) Y)) \land k \in X) \to f (k) \in ℝ^{*}$
182	181	ad4ant14	$⊢ ((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to f (k) \in ℝ^{*}$
183	150	ad4ant124	$⊢ (((φ \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to C (j) (k) \in ℝ^{*}$
184	29	3adant3	$⊢ (φ \land j \in ℕ \land k \in X) \to D (j) : X ⟶ ℝ$
185	184 148	ffvelcdmd	$⊢ (φ \land j \in ℕ \land k \in X) \to D (j) (k) \in ℝ$
186	185	rexrd	$⊢ (φ \land j \in ℕ \land k \in X) \to D (j) (k) \in ℝ^{*}$
187	186	ad4ant124	$⊢ (((φ \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to D (j) (k) \in ℝ^{*}$
188	171	elixp	$⊢ f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \leftrightarrow (f Fn X \land \forall k \in X f (k) \in [C (j) (k), D (j) (k)))$
189	188	biimpi	$⊢ f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \to (f Fn X \land \forall k \in X f (k) \in [C (j) (k), D (j) (k)))$
190	189	simprd	$⊢ f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \to \forall k \in X f (k) \in [C (j) (k), D (j) (k))$
191	190	adantr	$⊢ (f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \land k \in X) \to \forall k \in X f (k) \in [C (j) (k), D (j) (k))$
192		simpr	$⊢ (f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \land k \in X) \to k \in X$
193		rspa	$⊢ (\forall k \in X f (k) \in [C (j) (k), D (j) (k)) \land k \in X) \to f (k) \in [C (j) (k), D (j) (k))$
194	191 192 193	syl2anc	$⊢ (f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \land k \in X) \to f (k) \in [C (j) (k), D (j) (k))$
195	194	adantll	$⊢ (((φ \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to f (k) \in [C (j) (k), D (j) (k))$
196		icogelb	$⊢ (C (j) (k) \in ℝ^{} \land D (j) (k) \in ℝ^{} \land f (k) \in [C (j) (k), D (j) (k))) \to C (j) (k) \leq f (k)$
197	183 187 195 196	syl3anc	$⊢ (((φ \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to C (j) (k) \leq f (k)$
198	197	adantl3r	$⊢ ((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to C (j) (k) \leq f (k)$
199		icoltub	$⊢ (C (j) (k) \in ℝ^{} \land D (j) (k) \in ℝ^{} \land f (k) \in [C (j) (k), D (j) (k))) \to f (k) < D (j) (k)$
200	183 187 195 199	syl3anc	$⊢ (((φ \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to f (k) < D (j) (k)$
201	200	adantl3r	$⊢ ((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to f (k) < D (j) (k)$
202	201	ad2antrr	$⊢ ((((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \land D (j) (k) \leq Y) \to f (k) < D (j) (k)$
203		simpll	$⊢ ((φ \land f \in (K H (X) Y)) \land j \in ℕ) \to φ$
204		simpr	$⊢ ((φ \land f \in (K H (X) Y)) \land j \in ℕ) \to j \in ℕ$
205	203 204	jca	$⊢ ((φ \land f \in (K H (X) Y)) \land j \in ℕ) \to (φ \land j \in ℕ)$
206	205	3ad2ant1	$⊢ (((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land k = K \land D (j) (k) \leq Y) \to (φ \land j \in ℕ)$
207		simp2	$⊢ (((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land k = K \land D (j) (k) \leq Y) \to k = K$
208		simp3	$⊢ (((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land k = K \land D (j) (k) \leq Y) \to D (j) (k) \leq Y$
209		fveq2	$⊢ k = K \to D (j) (k) = D (j) (K)$
210	209	breq1d	$⊢ k = K \to (D (j) (k) \leq Y \leftrightarrow D (j) (K) \leq Y)$
211	210	biimpa	$⊢ (k = K \land D (j) (k) \leq Y) \to D (j) (K) \leq Y$
212	211	iftrued	$⊢ (k = K \land D (j) (k) \leq Y) \to if (D (j) (K) \leq Y, D (j) (K), Y) = D (j) (K)$
213	209	eqcomd	$⊢ k = K \to D (j) (K) = D (j) (k)$
214	213	adantr	$⊢ (k = K \land D (j) (k) \leq Y) \to D (j) (K) = D (j) (k)$
215	212 214	eqtrd	$⊢ (k = K \land D (j) (k) \leq Y) \to if (D (j) (K) \leq Y, D (j) (K), Y) = D (j) (k)$
216	215	3adant1	$⊢ ((φ \land j \in ℕ) \land k = K \land D (j) (k) \leq Y) \to if (D (j) (K) \leq Y, D (j) (K), Y) = D (j) (k)$
217		breq2	$⊢ y = Y \to (c (h) \leq y \leftrightarrow c (h) \leq Y)$
218		id	$⊢ y = Y \to y = Y$
219	217 218	ifbieq2d	$⊢ y = Y \to if (c (h) \leq y, c (h), y) = if (c (h) \leq Y, c (h), Y)$
220	219	ifeq2d	$⊢ y = Y \to if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y)) = if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq Y, c (h), Y))$
221	220	mpteq2dv	$⊢ y = Y \to (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y))) = (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq Y, c (h), Y)))$
222	221	mpteq2dv	$⊢ y = Y \to (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y)))) = (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq Y, c (h), Y))))$
223		ovex	$⊢ ℝ^{X} \in V$
224	223	mptex	$⊢ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq Y, c (h), Y)))) \in V$
225	224	a1i	$⊢ φ \to (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq Y, c (h), Y)))) \in V$
226	14 222 4 225	fvmptd3	$⊢ φ \to T (Y) = (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq Y, c (h), Y))))$
227	226	adantr	$⊢ (φ \land j \in ℕ) \to T (Y) = (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq Y, c (h), Y))))$
228		fveq1	$⊢ c = D (j) \to c (h) = D (j) (h)$
229	228	breq1d	$⊢ c = D (j) \to (c (h) \leq Y \leftrightarrow D (j) (h) \leq Y)$
230	229 228	ifbieq1d	$⊢ c = D (j) \to if (c (h) \leq Y, c (h), Y) = if (D (j) (h) \leq Y, D (j) (h), Y)$
231	228 230	ifeq12d	$⊢ c = D (j) \to if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq Y, c (h), Y)) = if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y))$
232	231	mpteq2dv	$⊢ c = D (j) \to (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq Y, c (h), Y))) = (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y)))$
233	232	adantl	$⊢ ((φ \land j \in ℕ) \land c = D (j)) \to (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq Y, c (h), Y))) = (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y)))$
234		mptexg	$⊢ X \in Fin \to (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y))) \in V$
235	2 234	syl	$⊢ φ \to (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y))) \in V$
236	235	adantr	$⊢ (φ \land j \in ℕ) \to (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y))) \in V$
237	227 233 27 236	fvmptd	$⊢ (φ \land j \in ℕ) \to T (Y) (D (j)) = (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y)))$
238	237	fveq1d	$⊢ (φ \land j \in ℕ) \to T (Y) (D (j)) (k) = (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y))) (k)$
239	238	3adant3	$⊢ (φ \land j \in ℕ \land k = K) \to T (Y) (D (j)) (k) = (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y))) (k)$
240		simpl	$⊢ (φ \land k = K) \to φ$
241		simpr	$⊢ (φ \land k = K) \to k = K$
242	240 3	syl	$⊢ (φ \land k = K) \to K \in X$
243	241 242	eqeltrd	$⊢ (φ \land k = K) \to k \in X$
244		eqidd	$⊢ (φ \land k \in X) \to (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y))) = (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y)))$
245		eleq1w	$⊢ h = k \to (h \in (X ∖ \{K\}) \leftrightarrow k \in (X ∖ \{K\}))$
246		fveq2	$⊢ h = k \to D (j) (h) = D (j) (k)$
247	246	breq1d	$⊢ h = k \to (D (j) (h) \leq Y \leftrightarrow D (j) (k) \leq Y)$
248	247 246	ifbieq1d	$⊢ h = k \to if (D (j) (h) \leq Y, D (j) (h), Y) = if (D (j) (k) \leq Y, D (j) (k), Y)$
249	245 246 248	ifbieq12d	$⊢ h = k \to if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y)) = if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y))$
250	249	adantl	$⊢ ((φ \land k \in X) \land h = k) \to if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y)) = if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y))$
251		simpr	$⊢ (φ \land k \in X) \to k \in X$
252		fvexd	$⊢ φ \to D (j) (k) \in V$
253	252 4	ifexd	$⊢ φ \to if (D (j) (k) \leq Y, D (j) (k), Y) \in V$
254	252 253	ifexd	$⊢ φ \to if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y)) \in V$
255	254	adantr	$⊢ (φ \land k \in X) \to if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y)) \in V$
256	244 250 251 255	fvmptd	$⊢ (φ \land k \in X) \to (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y))) (k) = if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y))$
257	240 243 256	syl2anc	$⊢ (φ \land k = K) \to (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y))) (k) = if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y))$
258		eleq1	$⊢ k = K \to (k \in (X ∖ \{K\}) \leftrightarrow K \in (X ∖ \{K\}))$
259	210 209	ifbieq1d	$⊢ k = K \to if (D (j) (k) \leq Y, D (j) (k), Y) = if (D (j) (K) \leq Y, D (j) (K), Y)$
260	258 209 259	ifbieq12d	$⊢ k = K \to if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y)) = if (K \in (X ∖ \{K\}), D (j) (K), if (D (j) (K) \leq Y, D (j) (K), Y))$
261	260	adantl	$⊢ (φ \land k = K) \to if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y)) = if (K \in (X ∖ \{K\}), D (j) (K), if (D (j) (K) \leq Y, D (j) (K), Y))$
262	257 261	eqtrd	$⊢ (φ \land k = K) \to (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y))) (k) = if (K \in (X ∖ \{K\}), D (j) (K), if (D (j) (K) \leq Y, D (j) (K), Y))$
263	262	3adant2	$⊢ (φ \land j \in ℕ \land k = K) \to (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y))) (k) = if (K \in (X ∖ \{K\}), D (j) (K), if (D (j) (K) \leq Y, D (j) (K), Y))$
264		neldifsnd	$⊢ k = K \to \neg K \in (X ∖ \{K\})$
265	264	iffalsed	$⊢ k = K \to if (K \in (X ∖ \{K\}), D (j) (K), if (D (j) (K) \leq Y, D (j) (K), Y)) = if (D (j) (K) \leq Y, D (j) (K), Y)$
266	265	3ad2ant3	$⊢ (φ \land j \in ℕ \land k = K) \to if (K \in (X ∖ \{K\}), D (j) (K), if (D (j) (K) \leq Y, D (j) (K), Y)) = if (D (j) (K) \leq Y, D (j) (K), Y)$
267	239 263 266	3eqtrrd	$⊢ (φ \land j \in ℕ \land k = K) \to if (D (j) (K) \leq Y, D (j) (K), Y) = T (Y) (D (j)) (k)$
268	267	3expa	$⊢ ((φ \land j \in ℕ) \land k = K) \to if (D (j) (K) \leq Y, D (j) (K), Y) = T (Y) (D (j)) (k)$
269	268	3adant3	$⊢ ((φ \land j \in ℕ) \land k = K \land D (j) (k) \leq Y) \to if (D (j) (K) \leq Y, D (j) (K), Y) = T (Y) (D (j)) (k)$
270	216 269	eqtr3d	$⊢ ((φ \land j \in ℕ) \land k = K \land D (j) (k) \leq Y) \to D (j) (k) = T (Y) (D (j)) (k)$
271	206 207 208 270	syl3anc	$⊢ (((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land k = K \land D (j) (k) \leq Y) \to D (j) (k) = T (Y) (D (j)) (k)$
272	271	ad5ant145	$⊢ ((((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \land D (j) (k) \leq Y) \to D (j) (k) = T (Y) (D (j)) (k)$
273	202 272	breqtrd	$⊢ ((((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \land D (j) (k) \leq Y) \to f (k) < T (Y) (D (j)) (k)$
274		mnfxr	$⊢ −∞ \in ℝ^{*}$
275	274	a1i	$⊢ ((φ \land f \in (K H (X) Y)) \land k \in X \land k = K) \to −∞ \in ℝ^{*}$
276	4	rexrd	$⊢ φ \to Y \in ℝ^{*}$
277	276	adantr	$⊢ (φ \land f \in (K H (X) Y)) \to Y \in ℝ^{*}$
278	277	3ad2ant1	$⊢ ((φ \land f \in (K H (X) Y)) \land k \in X \land k = K) \to Y \in ℝ^{*}$
279	179	3adant3	$⊢ ((φ \land f \in (K H (X) Y)) \land k \in X \land k = K) \to f (k) \in if (k = K, (−∞, Y), ℝ)$
280	156	3ad2ant3	$⊢ ((φ \land f \in (K H (X) Y)) \land k \in X \land k = K) \to if (k = K, (−∞, Y), ℝ) = (−∞, Y)$
281	279 280	eleqtrd	$⊢ ((φ \land f \in (K H (X) Y)) \land k \in X \land k = K) \to f (k) \in (−∞, Y)$
282		iooltub	$⊢ (−∞ \in ℝ^{} \land Y \in ℝ^{} \land f (k) \in (−∞, Y)) \to f (k) < Y$
283	275 278 281 282	syl3anc	$⊢ ((φ \land f \in (K H (X) Y)) \land k \in X \land k = K) \to f (k) < Y$
284	283	3adant1r	$⊢ (((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land k \in X \land k = K) \to f (k) < Y$
285	284	ad4ant123	$⊢ (((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land k \in X) \land k = K) \land \neg D (j) (k) \leq Y) \to f (k) < Y$
286		simpr	$⊢ (k = K \land \neg D (j) (k) \leq Y) \to \neg D (j) (k) \leq Y$
287	210	notbid	$⊢ k = K \to (\neg D (j) (k) \leq Y \leftrightarrow \neg D (j) (K) \leq Y)$
288	287	adantr	$⊢ (k = K \land \neg D (j) (k) \leq Y) \to (\neg D (j) (k) \leq Y \leftrightarrow \neg D (j) (K) \leq Y)$
289	286 288	mpbid	$⊢ (k = K \land \neg D (j) (k) \leq Y) \to \neg D (j) (K) \leq Y$
290	289	iffalsed	$⊢ (k = K \land \neg D (j) (k) \leq Y) \to if (D (j) (K) \leq Y, D (j) (K), Y) = Y$
291		eqidd	$⊢ (k = K \land \neg D (j) (k) \leq Y) \to Y = Y$
292	290 291	eqtr2d	$⊢ (k = K \land \neg D (j) (k) \leq Y) \to Y = if (D (j) (K) \leq Y, D (j) (K), Y)$
293	292	adantll	$⊢ (((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land k \in X) \land k = K) \land \neg D (j) (k) \leq Y) \to Y = if (D (j) (K) \leq Y, D (j) (K), Y)$
294	268	adantlr	$⊢ (((φ \land j \in ℕ) \land k \in X) \land k = K) \to if (D (j) (K) \leq Y, D (j) (K), Y) = T (Y) (D (j)) (k)$
295	294	adantl3r	$⊢ ((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land k \in X) \land k = K) \to if (D (j) (K) \leq Y, D (j) (K), Y) = T (Y) (D (j)) (k)$
296	295	adantr	$⊢ (((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land k \in X) \land k = K) \land \neg D (j) (k) \leq Y) \to if (D (j) (K) \leq Y, D (j) (K), Y) = T (Y) (D (j)) (k)$
297	293 296	eqtrd	$⊢ (((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land k \in X) \land k = K) \land \neg D (j) (k) \leq Y) \to Y = T (Y) (D (j)) (k)$
298	285 297	breqtrd	$⊢ (((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land k \in X) \land k = K) \land \neg D (j) (k) \leq Y) \to f (k) < T (Y) (D (j)) (k)$
299	298	adantl3r	$⊢ ((((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \land \neg D (j) (k) \leq Y) \to f (k) < T (Y) (D (j)) (k)$
300	273 299	pm2.61dan	$⊢ (((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \to f (k) < T (Y) (D (j)) (k)$
301	201	adantr	$⊢ (((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land \neg k = K) \to f (k) < D (j) (k)$
302	237	3adant3	$⊢ (φ \land j \in ℕ \land k \in X) \to T (Y) (D (j)) = (h \in X ⟼ if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y)))$
303	249	adantl	$⊢ ((φ \land j \in ℕ \land k \in X) \land h = k) \to if (h \in (X ∖ \{K\}), D (j) (h), if (D (j) (h) \leq Y, D (j) (h), Y)) = if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y))$
304	255	3adant2	$⊢ (φ \land j \in ℕ \land k \in X) \to if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y)) \in V$
305	302 303 148 304	fvmptd	$⊢ (φ \land j \in ℕ \land k \in X) \to T (Y) (D (j)) (k) = if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y))$
306	305	3expa	$⊢ ((φ \land j \in ℕ) \land k \in X) \to T (Y) (D (j)) (k) = if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y))$
307	306	adantllr	$⊢ (((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land k \in X) \to T (Y) (D (j)) (k) = if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y))$
308	307	ad4ant13	$⊢ (((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land \neg k = K) \to T (Y) (D (j)) (k) = if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y))$
309		simpl	$⊢ (k \in X \land \neg k = K) \to k \in X$
310		neqne	$⊢ \neg k = K \to k \neq K$
311		nelsn	$⊢ k \neq K \to \neg k \in \{K\}$
312	310 311	syl	$⊢ \neg k = K \to \neg k \in \{K\}$
313	312	adantl	$⊢ (k \in X \land \neg k = K) \to \neg k \in \{K\}$
314	309 313	eldifd	$⊢ (k \in X \land \neg k = K) \to k \in (X ∖ \{K\})$
315	314	iftrued	$⊢ (k \in X \land \neg k = K) \to if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y)) = D (j) (k)$
316	315	adantll	$⊢ (((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land \neg k = K) \to if (k \in (X ∖ \{K\}), D (j) (k), if (D (j) (k) \leq Y, D (j) (k), Y)) = D (j) (k)$
317	308 316	eqtr2d	$⊢ (((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land \neg k = K) \to D (j) (k) = T (Y) (D (j)) (k)$
318	301 317	breqtrd	$⊢ (((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land \neg k = K) \to f (k) < T (Y) (D (j)) (k)$
319	300 318	pm2.61dan	$⊢ ((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to f (k) < T (Y) (D (j)) (k)$
320	151 155 182 198 319	elicod	$⊢ ((((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to f (k) \in [C (j) (k), T (Y) (D (j)) (k))$
321	320	ex	$⊢ (((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to (k \in X \to f (k) \in [C (j) (k), T (Y) (D (j)) (k)))$
322	146 321	ralrimi	$⊢ (((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to \forall k \in X f (k) \in [C (j) (k), T (Y) (D (j)) (k))$
323	141 322	jca	$⊢ (((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to (f Fn X \land \forall k \in X f (k) \in [C (j) (k), T (Y) (D (j)) (k)))$
324	171	elixp	$⊢ f \in \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k)) \leftrightarrow (f Fn X \land \forall k \in X f (k) \in [C (j) (k), T (Y) (D (j)) (k)))$
325	323 324	sylibr	$⊢ (((φ \land f \in (K H (X) Y)) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to f \in \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k))$
326	325	ex	$⊢ ((φ \land f \in (K H (X) Y)) \land j \in ℕ) \to (f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \to f \in \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k)))$
327	135 138 139 326	syl21anc	$⊢ ((φ \land f \in (A \cap (K H (X) Y))) \land j \in ℕ) \to (f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \to f \in \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k)))$
328	327	reximdva	$⊢ (φ \land f \in (A \cap (K H (X) Y))) \to (\exists j \in ℕ f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \to \exists j \in ℕ f \in \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k)))$
329	134 328	mpd	$⊢ (φ \land f \in (A \cap (K H (X) Y))) \to \exists j \in ℕ f \in \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k))$
330		eliun	$⊢ f \in ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k)) \leftrightarrow \exists j \in ℕ f \in \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k))$
331	329 330	sylibr	$⊢ (φ \land f \in (A \cap (K H (X) Y))) \to f \in ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k))$
332	331	ralrimiva	$⊢ φ \to \forall f \in (A \cap (K H (X) Y)) f \in ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k))$
333		dfss3	$⊢ A \cap (K H (X) Y) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k)) \leftrightarrow \forall f \in (A \cap (K H (X) Y)) f \in ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k))$
334	332 333	sylibr	$⊢ φ \to A \cap (K H (X) Y) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k))$
335		eqidd	$⊢ j \in ℕ \to (l \in ℕ ⟼ T (Y) (D (l))) = (l \in ℕ ⟼ T (Y) (D (l)))$
336		2fveq3	$⊢ l = j \to T (Y) (D (l)) = T (Y) (D (j))$
337	336	adantl	$⊢ (j \in ℕ \land l = j) \to T (Y) (D (l)) = T (Y) (D (j))$
338		id	$⊢ j \in ℕ \to j \in ℕ$
339		fvexd	$⊢ j \in ℕ \to T (Y) (D (j)) \in V$
340	335 337 338 339	fvmptd	$⊢ j \in ℕ \to (l \in ℕ ⟼ T (Y) (D (l))) (j) = T (Y) (D (j))$
341	340	fveq1d	$⊢ j \in ℕ \to (l \in ℕ ⟼ T (Y) (D (l))) (j) (k) = T (Y) (D (j)) (k)$
342	341	oveq2d	$⊢ j \in ℕ \to [C (j) (k), (l \in ℕ ⟼ T (Y) (D (l))) (j) (k)) = [C (j) (k), T (Y) (D (j)) (k))$
343	342	ixpeq2dv	$⊢ j \in ℕ \to \underset{k \in X}{⨉} [C (j) (k), (l \in ℕ ⟼ T (Y) (D (l))) (j) (k)) = \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k))$
344	343	iuneq2i	$⊢ ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), (l \in ℕ ⟼ T (Y) (D (l))) (j) (k)) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), T (Y) (D (j)) (k))$
345	334 344	sseqtrrdi	$⊢ φ \to A \cap (K H (X) Y) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [C (j) (k), (l \in ℕ ⟼ T (Y) (D (l))) (j) (k))$
346	2 6 127 345 13	ovnlecvr2	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) \leq sum^((j \in ℕ ⟼ C (j) L (X) (l \in ℕ ⟼ T (Y) (D (l))) (j)))$
347	340	oveq2d	$⊢ j \in ℕ \to C (j) L (X) (l \in ℕ ⟼ T (Y) (D (l))) (j) = C (j) L (X) T (Y) (D (j))$
348	347	mpteq2ia	$⊢ (j \in ℕ ⟼ C (j) L (X) (l \in ℕ ⟼ T (Y) (D (l))) (j)) = (j \in ℕ ⟼ C (j) L (X) T (Y) (D (j)))$
349	348	fveq2i	$⊢ sum^((j \in ℕ ⟼ C (j) L (X) (l \in ℕ ⟼ T (Y) (D (l))) (j))) = sum^((j \in ℕ ⟼ C (j) L (X) T (Y) (D (j))))$
350	349	a1i	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (X) (l \in ℕ ⟼ T (Y) (D (l))) (j))) = sum^((j \in ℕ ⟼ C (j) L (X) T (Y) (D (j))))$
351	346 350	breqtrd	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) \leq sum^((j \in ℕ ⟼ C (j) L (X) T (Y) (D (j))))$
352	6	ffvelcdmda	$⊢ (φ \land l \in ℕ) \to C (l) \in (ℝ^{X})$
353		elmapi	$⊢ C (l) \in (ℝ^{X}) \to C (l) : X ⟶ ℝ$
354	352 353	syl	$⊢ (φ \land l \in ℕ) \to C (l) : X ⟶ ℝ$
355	15 111 112 354	hoidifhspf	$⊢ (φ \land l \in ℕ) \to S (Y) (C (l)) : X ⟶ ℝ$
356		elmapg	$⊢ (ℝ \in V \land X \in Fin) \to (S (Y) (C (l)) \in (ℝ^{X}) \leftrightarrow S (Y) (C (l)) : X ⟶ ℝ)$
357	122 356	syl	$⊢ φ \to (S (Y) (C (l)) \in (ℝ^{X}) \leftrightarrow S (Y) (C (l)) : X ⟶ ℝ)$
358	357	adantr	$⊢ (φ \land l \in ℕ) \to (S (Y) (C (l)) \in (ℝ^{X}) \leftrightarrow S (Y) (C (l)) : X ⟶ ℝ)$
359	355 358	mpbird	$⊢ (φ \land l \in ℕ) \to S (Y) (C (l)) \in (ℝ^{X})$
360	359	fmpttd	$⊢ φ \to (l \in ℕ ⟼ S (Y) (C (l))) : ℕ ⟶ ℝ^{X}$
361		simpl	$⊢ (φ \land f \in (A ∖ (K H (X) Y))) \to φ$
362		eldifi	$⊢ f \in (A ∖ (K H (X) Y)) \to f \in A$
363	362	adantl	$⊢ (φ \land f \in (A ∖ (K H (X) Y))) \to f \in A$
364	361 363 133	syl2anc	$⊢ (φ \land f \in (A ∖ (K H (X) Y))) \to \exists j \in ℕ f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
365	140	adantl	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to f Fn X$
366		nfv	$⊢ Ⅎ k ((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ)$
367	366 145	nfan	$⊢ Ⅎ k (((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)))$
368	100	3adant3	$⊢ (φ \land j \in ℕ \land k \in X) \to S (Y) (C (j)) : X ⟶ ℝ$
369	368 148	ffvelcdmd	$⊢ (φ \land j \in ℕ \land k \in X) \to S (Y) (C (j)) (k) \in ℝ$
370	369	rexrd	$⊢ (φ \land j \in ℕ \land k \in X) \to S (Y) (C (j)) (k) \in ℝ^{*}$
371	370	ad5ant135	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to S (Y) (C (j)) (k) \in ℝ^{*}$
372	187	adantl3r	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to D (j) (k) \in ℝ^{*}$
373	149	3expa	$⊢ ((φ \land j \in ℕ) \land k \in X) \to C (j) (k) \in ℝ$
374	186	3expa	$⊢ ((φ \land j \in ℕ) \land k \in X) \to D (j) (k) \in ℝ^{*}$
375		icossre	$⊢ (C (j) (k) \in ℝ \land D (j) (k) \in ℝ^{*}) \to [C (j) (k), D (j) (k)) \subseteq ℝ$
376	373 374 375	syl2anc	$⊢ ((φ \land j \in ℕ) \land k \in X) \to [C (j) (k), D (j) (k)) \subseteq ℝ$
377	376	adantlr	$⊢ (((φ \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to [C (j) (k), D (j) (k)) \subseteq ℝ$
378	377 195	sseldd	$⊢ (((φ \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to f (k) \in ℝ$
379	378	rexrd	$⊢ (((φ \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to f (k) \in ℝ^{*}$
380	379	adantl3r	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to f (k) \in ℝ^{*}$
381	41	3adant3	$⊢ (φ \land j \in ℕ \land k \in X) \to Y \in ℝ$
382	23	3adant3	$⊢ (φ \land j \in ℕ \land k \in X) \to X \in Fin$
383	15 381 382 147 148	hoidifhspval3	$⊢ (φ \land j \in ℕ \land k \in X) \to S (Y) (C (j)) (k) = if (k = K, if (Y \leq C (j) (k), C (j) (k), Y), C (j) (k))$
384	383	ad5ant134	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land k \in X) \land k = K) \to S (Y) (C (j)) (k) = if (k = K, if (Y \leq C (j) (k), C (j) (k), Y), C (j) (k))$
385		iftrue	$⊢ k = K \to if (k = K, if (Y \leq C (j) (k), C (j) (k), Y), C (j) (k)) = if (Y \leq C (j) (k), C (j) (k), Y)$
386	385	adantl	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land k \in X) \land k = K) \to if (k = K, if (Y \leq C (j) (k), C (j) (k), Y), C (j) (k)) = if (Y \leq C (j) (k), C (j) (k), Y)$
387	384 386	eqtrd	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land k \in X) \land k = K) \to S (Y) (C (j)) (k) = if (Y \leq C (j) (k), C (j) (k), Y)$
388	387	adantllr	$⊢ (((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \to S (Y) (C (j)) (k) = if (Y \leq C (j) (k), C (j) (k), Y)$
389		iftrue	$⊢ Y \leq C (j) (k) \to if (Y \leq C (j) (k), C (j) (k), Y) = C (j) (k)$
390	389	adantl	$⊢ ((((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \land Y \leq C (j) (k)) \to if (Y \leq C (j) (k), C (j) (k), Y) = C (j) (k)$
391	197	adantl3r	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to C (j) (k) \leq f (k)$
392	391	ad2antrr	$⊢ ((((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \land Y \leq C (j) (k)) \to C (j) (k) \leq f (k)$
393	390 392	eqbrtrd	$⊢ ((((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \land Y \leq C (j) (k)) \to if (Y \leq C (j) (k), C (j) (k), Y) \leq f (k)$
394		iffalse	$⊢ \neg Y \leq C (j) (k) \to if (Y \leq C (j) (k), C (j) (k), Y) = Y$
395	394	adantl	$⊢ ((((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \land \neg Y \leq C (j) (k)) \to if (Y \leq C (j) (k), C (j) (k), Y) = Y$
396		simpl1	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \land \neg Y \leq f (k)) \to (φ \land f \in (A ∖ (K H (X) Y)))$
397		simpr	$⊢ (k = K \land \neg Y \leq f (k)) \to \neg Y \leq f (k)$
398		fveq2	$⊢ k = K \to f (k) = f (K)$
399	398	breq2d	$⊢ k = K \to (Y \leq f (k) \leftrightarrow Y \leq f (K))$
400	399	notbid	$⊢ k = K \to (\neg Y \leq f (k) \leftrightarrow \neg Y \leq f (K))$
401	400	adantr	$⊢ (k = K \land \neg Y \leq f (k)) \to (\neg Y \leq f (k) \leftrightarrow \neg Y \leq f (K))$
402	397 401	mpbid	$⊢ (k = K \land \neg Y \leq f (k)) \to \neg Y \leq f (K)$
403	402	3ad2antl3	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \land \neg Y \leq f (k)) \to \neg Y \leq f (K)$
404	398	eqcomd	$⊢ k = K \to f (K) = f (k)$
405	404	3ad2ant3	$⊢ ((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \to f (K) = f (k)$
406	364	adantr	$⊢ ((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X) \to \exists j \in ℕ f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
407		id	$⊢ (φ \land j \in ℕ) \to (φ \land j \in ℕ)$
408	407	ad4ant13	$⊢ (((φ \land k \in X) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to (φ \land j \in ℕ)$
409		simpr	$⊢ (((φ \land k \in X) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))$
410	251	ad2antrr	$⊢ (((φ \land k \in X) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to k \in X$
411	408 409 410 378	syl21anc	$⊢ (((φ \land k \in X) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to f (k) \in ℝ$
412	411	rexlimdva2	$⊢ (φ \land k \in X) \to (\exists j \in ℕ f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \to f (k) \in ℝ)$
413	412	adantlr	$⊢ ((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X) \to (\exists j \in ℕ f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \to f (k) \in ℝ)$
414	406 413	mpd	$⊢ ((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X) \to f (k) \in ℝ$
415	414	3adant3	$⊢ ((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \to f (k) \in ℝ$
416	405 415	eqeltrd	$⊢ ((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \to f (K) \in ℝ$
417	416	adantr	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \land \neg Y \leq f (k)) \to f (K) \in ℝ$
418	396 361 4	3syl	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \land \neg Y \leq f (k)) \to Y \in ℝ$
419	417 418	ltnled	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \land \neg Y \leq f (k)) \to (f (K) < Y \leftrightarrow \neg Y \leq f (K))$
420	403 419	mpbird	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \land \neg Y \leq f (k)) \to f (K) < Y$
421	365 364	r19.29a	$⊢ (φ \land f \in (A ∖ (K H (X) Y))) \to f Fn X$
422	421	adantr	$⊢ ((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \to f Fn X$
423	274	a1i	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \land k \in X) \land k = K) \to −∞ \in ℝ^{*}$
424	276	ad4antr	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \land k \in X) \land k = K) \to Y \in ℝ^{*}$
425	414	ad4ant13	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \land k \in X) \land k = K) \to f (k) \in ℝ$
426	425	mnfltd	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \land k \in X) \land k = K) \to −∞ < f (k)$
427	398	adantl	$⊢ (f (K) < Y \land k = K) \to f (k) = f (K)$
428		simpl	$⊢ (f (K) < Y \land k = K) \to f (K) < Y$
429	427 428	eqbrtrd	$⊢ (f (K) < Y \land k = K) \to f (k) < Y$
430	429	ad4ant24	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \land k \in X) \land k = K) \to f (k) < Y$
431	423 424 425 426 430	eliood	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \land k \in X) \land k = K) \to f (k) \in (−∞, Y)$
432	156	eqcomd	$⊢ k = K \to (−∞, Y) = if (k = K, (−∞, Y), ℝ)$
433	432	adantl	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \land k \in X) \land k = K) \to (−∞, Y) = if (k = K, (−∞, Y), ℝ)$
434	431 433	eleqtrd	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \land k \in X) \land k = K) \to f (k) \in if (k = K, (−∞, Y), ℝ)$
435	414	ad4ant13	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \land k \in X) \land \neg k = K) \to f (k) \in ℝ$
436	160	eqcomd	$⊢ \neg k = K \to ℝ = if (k = K, (−∞, Y), ℝ)$
437	436	adantl	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \land k \in X) \land \neg k = K) \to ℝ = if (k = K, (−∞, Y), ℝ)$
438	435 437	eleqtrd	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \land k \in X) \land \neg k = K) \to f (k) \in if (k = K, (−∞, Y), ℝ)$
439	434 438	pm2.61dan	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \land k \in X) \to f (k) \in if (k = K, (−∞, Y), ℝ)$
440	439	ralrimiva	$⊢ ((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \to \forall k \in X f (k) \in if (k = K, (−∞, Y), ℝ)$
441	422 440	jca	$⊢ ((φ \land f \in (A ∖ (K H (X) Y))) \land f (K) < Y) \to (f Fn X \land \forall k \in X f (k) \in if (k = K, (−∞, Y), ℝ))$
442	396 420 441	syl2anc	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \land \neg Y \leq f (k)) \to (f Fn X \land \forall k \in X f (k) \in if (k = K, (−∞, Y), ℝ))$
443	442 172	sylibr	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \land \neg Y \leq f (k)) \to f \in \underset{k \in X}{⨉} if (k = K, (−∞, Y), ℝ)$
444	166	eqcomd	$⊢ φ \to \underset{k \in X}{⨉} if (k = K, (−∞, Y), ℝ) = K H (X) Y$
445	444	ad2antrr	$⊢ ((φ \land f \in (A ∖ (K H (X) Y))) \land \neg Y \leq f (k)) \to \underset{k \in X}{⨉} if (k = K, (−∞, Y), ℝ) = K H (X) Y$
446	445	3ad2antl1	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \land \neg Y \leq f (k)) \to \underset{k \in X}{⨉} if (k = K, (−∞, Y), ℝ) = K H (X) Y$
447	443 446	eleqtrd	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \land \neg Y \leq f (k)) \to f \in (K H (X) Y)$
448		eldifn	$⊢ f \in (A ∖ (K H (X) Y)) \to \neg f \in (K H (X) Y)$
449	448	adantl	$⊢ (φ \land f \in (A ∖ (K H (X) Y))) \to \neg f \in (K H (X) Y)$
450	449	3ad2ant1	$⊢ ((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \to \neg f \in (K H (X) Y)$
451	450	adantr	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \land \neg Y \leq f (k)) \to \neg f \in (K H (X) Y)$
452	447 451	condan	$⊢ ((φ \land f \in (A ∖ (K H (X) Y))) \land k \in X \land k = K) \to Y \leq f (k)$
453	452	ad5ant145	$⊢ (((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \to Y \leq f (k)$
454	453	adantr	$⊢ ((((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \land \neg Y \leq C (j) (k)) \to Y \leq f (k)$
455	395 454	eqbrtrd	$⊢ ((((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \land \neg Y \leq C (j) (k)) \to if (Y \leq C (j) (k), C (j) (k), Y) \leq f (k)$
456	393 455	pm2.61dan	$⊢ (((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \to if (Y \leq C (j) (k), C (j) (k), Y) \leq f (k)$
457	388 456	eqbrtrd	$⊢ (((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land k = K) \to S (Y) (C (j)) (k) \leq f (k)$
458	383	ad5ant124	$⊢ ((((φ \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land \neg k = K) \to S (Y) (C (j)) (k) = if (k = K, if (Y \leq C (j) (k), C (j) (k), Y), C (j) (k))$
459		iffalse	$⊢ \neg k = K \to if (k = K, if (Y \leq C (j) (k), C (j) (k), Y), C (j) (k)) = C (j) (k)$
460	459	adantl	$⊢ ((((φ \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land \neg k = K) \to if (k = K, if (Y \leq C (j) (k), C (j) (k), Y), C (j) (k)) = C (j) (k)$
461	458 460	eqtrd	$⊢ ((((φ \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land \neg k = K) \to S (Y) (C (j)) (k) = C (j) (k)$
462	197	adantr	$⊢ ((((φ \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land \neg k = K) \to C (j) (k) \leq f (k)$
463	461 462	eqbrtrd	$⊢ ((((φ \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land \neg k = K) \to S (Y) (C (j)) (k) \leq f (k)$
464	463	adantl4r	$⊢ (((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \land \neg k = K) \to S (Y) (C (j)) (k) \leq f (k)$
465	457 464	pm2.61dan	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to S (Y) (C (j)) (k) \leq f (k)$
466	200	adantl3r	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to f (k) < D (j) (k)$
467	371 372 380 465 466	elicod	$⊢ ((((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \land k \in X) \to f (k) \in [S (Y) (C (j)) (k), D (j) (k))$
468	467	ex	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to (k \in X \to f (k) \in [S (Y) (C (j)) (k), D (j) (k)))$
469	367 468	ralrimi	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to \forall k \in X f (k) \in [S (Y) (C (j)) (k), D (j) (k))$
470	365 469	jca	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to (f Fn X \land \forall k \in X f (k) \in [S (Y) (C (j)) (k), D (j) (k)))$
471	171	elixp	$⊢ f \in \underset{k \in X}{⨉} [S (Y) (C (j)) (k), D (j) (k)) \leftrightarrow (f Fn X \land \forall k \in X f (k) \in [S (Y) (C (j)) (k), D (j) (k)))$
472	470 471	sylibr	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to f \in \underset{k \in X}{⨉} [S (Y) (C (j)) (k), D (j) (k))$
473		eqidd	$⊢ j \in ℕ \to (l \in ℕ ⟼ S (Y) (C (l))) = (l \in ℕ ⟼ S (Y) (C (l)))$
474		2fveq3	$⊢ l = j \to S (Y) (C (l)) = S (Y) (C (j))$
475	474	adantl	$⊢ (j \in ℕ \land l = j) \to S (Y) (C (l)) = S (Y) (C (j))$
476		fvexd	$⊢ j \in ℕ \to S (Y) (C (j)) \in V$
477	473 475 338 476	fvmptd	$⊢ j \in ℕ \to (l \in ℕ ⟼ S (Y) (C (l))) (j) = S (Y) (C (j))$
478	477	fveq1d	$⊢ j \in ℕ \to (l \in ℕ ⟼ S (Y) (C (l))) (j) (k) = S (Y) (C (j)) (k)$
479	478	oveq1d	$⊢ j \in ℕ \to [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k)) = [S (Y) (C (j)) (k), D (j) (k))$
480	479	ixpeq2dv	$⊢ j \in ℕ \to \underset{k \in X}{⨉} [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k)) = \underset{k \in X}{⨉} [S (Y) (C (j)) (k), D (j) (k))$
481	480	ad2antlr	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to \underset{k \in X}{⨉} [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k)) = \underset{k \in X}{⨉} [S (Y) (C (j)) (k), D (j) (k))$
482	481	eleq2d	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to (f \in \underset{k \in X}{⨉} [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k)) \leftrightarrow f \in \underset{k \in X}{⨉} [S (Y) (C (j)) (k), D (j) (k)))$
483	472 482	mpbird	$⊢ (((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \land f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k))) \to f \in \underset{k \in X}{⨉} [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k))$
484	483	ex	$⊢ ((φ \land f \in (A ∖ (K H (X) Y))) \land j \in ℕ) \to (f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \to f \in \underset{k \in X}{⨉} [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k)))$
485	484	reximdva	$⊢ (φ \land f \in (A ∖ (K H (X) Y))) \to (\exists j \in ℕ f \in \underset{k \in X}{⨉} [C (j) (k), D (j) (k)) \to \exists j \in ℕ f \in \underset{k \in X}{⨉} [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k)))$
486	364 485	mpd	$⊢ (φ \land f \in (A ∖ (K H (X) Y))) \to \exists j \in ℕ f \in \underset{k \in X}{⨉} [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k))$
487		eliun	$⊢ f \in ⋃_{j \in ℕ} \underset{k \in X}{⨉} [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k)) \leftrightarrow \exists j \in ℕ f \in \underset{k \in X}{⨉} [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k))$
488	486 487	sylibr	$⊢ (φ \land f \in (A ∖ (K H (X) Y))) \to f \in ⋃_{j \in ℕ} \underset{k \in X}{⨉} [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k))$
489	488	ralrimiva	$⊢ φ \to \forall f \in (A ∖ (K H (X) Y)) f \in ⋃_{j \in ℕ} \underset{k \in X}{⨉} [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k))$
490		dfss3	$⊢ A ∖ (K H (X) Y) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k)) \leftrightarrow \forall f \in (A ∖ (K H (X) Y)) f \in ⋃_{j \in ℕ} \underset{k \in X}{⨉} [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k))$
491	489 490	sylibr	$⊢ φ \to A ∖ (K H (X) Y) \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [(l \in ℕ ⟼ S (Y) (C (l))) (j) (k), D (j) (k))$
492	2 360 7 491 13	ovnlecvr2	$⊢ φ \to voln* (X) (A ∖ (K H (X) Y)) \leq sum^((j \in ℕ ⟼ (l \in ℕ ⟼ S (Y) (C (l))) (j) L (X) D (j)))$
493	477	oveq1d	$⊢ j \in ℕ \to (l \in ℕ ⟼ S (Y) (C (l))) (j) L (X) D (j) = S (Y) (C (j)) L (X) D (j)$
494	493	mpteq2ia	$⊢ (j \in ℕ ⟼ (l \in ℕ ⟼ S (Y) (C (l))) (j) L (X) D (j)) = (j \in ℕ ⟼ S (Y) (C (j)) L (X) D (j))$
495	494	fveq2i	$⊢ sum^((j \in ℕ ⟼ (l \in ℕ ⟼ S (Y) (C (l))) (j) L (X) D (j))) = sum^((j \in ℕ ⟼ S (Y) (C (j)) L (X) D (j)))$
496	495	a1i	$⊢ φ \to sum^((j \in ℕ ⟼ (l \in ℕ ⟼ S (Y) (C (l))) (j) L (X) D (j))) = sum^((j \in ℕ ⟼ S (Y) (C (j)) L (X) D (j)))$
497	492 496	breqtrd	$⊢ φ \to voln* (X) (A ∖ (K H (X) Y)) \leq sum^((j \in ℕ ⟼ S (Y) (C (j)) L (X) D (j)))$
498	11 12 99 110 351 497	le2addd	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \leq sum^((j \in ℕ ⟼ C (j) L (X) T (Y) (D (j)))) + sum^((j \in ℕ ⟼ S (Y) (C (j)) L (X) D (j)))$
499	23 107 41 26 29 13 14 15	hspmbllem1	$⊢ (φ \land j \in ℕ) \to C (j) L (X) D (j) = (C (j) L (X) T (Y) (D (j))) +_{𝑒} (S (Y) (C (j)) L (X) D (j))$
500	499	mpteq2dva	$⊢ φ \to (j \in ℕ ⟼ C (j) L (X) D (j)) = (j \in ℕ ⟼ (C (j) L (X) T (Y) (D (j))) +_{𝑒} (S (Y) (C (j)) L (X) D (j)))$
501	500	fveq2d	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (X) D (j))) = sum^((j \in ℕ ⟼ (C (j) L (X) T (Y) (D (j))) +_{𝑒} (S (Y) (C (j)) L (X) D (j))))$
502	19 21 44 106	sge0xadd	$⊢ φ \to sum^((j \in ℕ ⟼ (C (j) L (X) T (Y) (D (j))) +_{𝑒} (S (Y) (C (j)) L (X) D (j)))) = sum^((j \in ℕ ⟼ C (j) L (X) T (Y) (D (j)))) +_{𝑒} sum^((j \in ℕ ⟼ S (Y) (C (j)) L (X) D (j)))$
503	99 110	rexaddd	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (X) T (Y) (D (j)))) +_{𝑒} sum^((j \in ℕ ⟼ S (Y) (C (j)) L (X) D (j))) = sum^((j \in ℕ ⟼ C (j) L (X) T (Y) (D (j)))) + sum^((j \in ℕ ⟼ S (Y) (C (j)) L (X) D (j)))$
504	501 502 503	3eqtrrd	$⊢ φ \to sum^((j \in ℕ ⟼ C (j) L (X) T (Y) (D (j)))) + sum^((j \in ℕ ⟼ S (Y) (C (j)) L (X) D (j))) = sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
505	498 504	breqtrd	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \leq sum^((j \in ℕ ⟼ C (j) L (X) D (j)))$
506	16 40 18 505 39	letrd	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A) + E$

Metamath Proof Explorer

Theorem hspmbllem2

Proof