hspmbllem2 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hspmbllem2		Structured version Visualization version GIF version

Theorem hspmbllem2 46647

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.)

**Hypotheses**
Ref	Expression
hspmbllem2.h	⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
hspmbllem2.x	⊢ (𝜑 → 𝑋 ∈ Fin)
hspmbllem2.k	⊢ (𝜑 → 𝐾 ∈ 𝑋)
hspmbllem2.y	⊢ (𝜑 → 𝑌 ∈ ℝ)
hspmbllem2.e	⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
hspmbllem2.c	⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑_m 𝑋))
hspmbllem2.d	⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑_m 𝑋))
hspmbllem2.a	⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
hspmbllem2.g	⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
hspmbllem2.r	⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ)
hspmbllem2.i	⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ)
hspmbllem2.f	⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ)
hspmbllem2.l	⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
hspmbllem2.t	⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
hspmbllem2.s	⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ)))))

**Assertion**
Ref	Expression
hspmbllem2	⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))

Distinct variable groups: 𝐴,𝑗,𝑘 𝐶,𝑎,𝑏,𝑐,ℎ,𝑘,𝑙 𝐷,𝑎,𝑏,𝑐,ℎ,𝑗,𝑘,𝑙 𝑗,𝐻,𝑘 𝐾,𝑎,𝑏,𝑐,ℎ,𝑗,𝑘,𝑙,𝑥,𝑦 𝑆,𝑎,𝑏,𝑘,𝑙 𝑇,𝑎,𝑏,𝑘,𝑙 𝑋,𝑎,𝑏,𝑐,ℎ,𝑗,𝑘,𝑙,𝑥,𝑦 𝑌,𝑎,𝑏,𝑐,ℎ,𝑗,𝑘,𝑙,𝑥,𝑦 𝜑,𝑎,𝑏,𝑐,ℎ,𝑗,𝑘,𝑙,𝑥,𝑦 Allowed substitution hints: 𝐴(𝑥,𝑦,ℎ,𝑎,𝑏,𝑐,𝑙) 𝐶(𝑥,𝑦,𝑗) 𝐷(𝑥,𝑦) 𝑆(𝑥,𝑦,ℎ,𝑗,𝑐) 𝑇(𝑥,𝑦,ℎ,𝑗,𝑐) 𝐸(𝑥,𝑦,ℎ,𝑗,𝑘,𝑎,𝑏,𝑐,𝑙) 𝐻(𝑥,𝑦,ℎ,𝑎,𝑏,𝑐,𝑙) 𝐿(𝑥,𝑦,ℎ,𝑗,𝑘,𝑎,𝑏,𝑐,𝑙)

Proof of Theorem hspmbllem2 Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		hspmbllem2.i	. . 3 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ)
2		hspmbllem2.f	. . 3 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ)
3	1, 2	readdcld 11291	. 2 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ∈ ℝ)
4		hspmbllem2.r	. . . 4 ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ)
5		hspmbllem2.e	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
6	5	rpred 13078	. . . 4 ⊢ (𝜑 → 𝐸 ∈ ℝ)
7	4, 6	readdcld 11291	. . 3 ⊢ (𝜑 → (((voln*‘𝑋)‘𝐴) + 𝐸) ∈ ℝ)
8		nfv 1913	. . . 4 ⊢ Ⅎ𝑗𝜑
9		nnex 12273	. . . . 5 ⊢ ℕ ∈ V
10	9	a1i 11	. . . 4 ⊢ (𝜑 → ℕ ∈ V)
11		icossicc 13477	. . . . 5 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
12		hspmbllem2.l	. . . . . 6 ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
13		hspmbllem2.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ Fin)
14	13	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
15		hspmbllem2.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑_m 𝑋))
16	15	ffvelcdmda 7103	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑_m 𝑋))
17		elmapi 8890	. . . . . . 7 ⊢ ((𝐶‘𝑗) ∈ (ℝ ↑_m 𝑋) → (𝐶‘𝑗):𝑋⟶ℝ)
18	16, 17	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑋⟶ℝ)
19		hspmbllem2.d	. . . . . . . 8 ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑_m 𝑋))
20	19	ffvelcdmda 7103	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑_m 𝑋))
21		elmapi 8890	. . . . . . 7 ⊢ ((𝐷‘𝑗) ∈ (ℝ ↑_m 𝑋) → (𝐷‘𝑗):𝑋⟶ℝ)
22	20, 21	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ)
23	12, 14, 18, 22	hoidmvcl 46602	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞))
24	11, 23	sselid 3980	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,]+∞))
25	8, 10, 24	sge0clmpt 46445	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ (0[,]+∞))
26		hspmbllem2.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
27		ne0i 4340	. . . . . . . . 9 ⊢ (𝐾 ∈ 𝑋 → 𝑋 ≠ ∅)
28	26, 27	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ≠ ∅)
29	28	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
30	12, 14, 29, 18, 22	hoidmvn0val 46604	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
31	30	mpteq2dva 5241	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))))
32	31	fveq2d 6909	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))))
33		hspmbllem2.g	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
34	32, 33	eqbrtrd 5164	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
35	7, 25, 34	ge0lere 45550	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ ℝ)
36		hspmbllem2.t	. . . . . . . . 9 ⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
37		hspmbllem2.y	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ ℝ)
38	37	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑌 ∈ ℝ)
39	36, 38, 14, 22	hsphoif 46596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑗)):𝑋⟶ℝ)
40	12, 14, 18, 39	hoidmvcl 46602	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ∈ (0[,)+∞))
41	11, 40	sselid 3980	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ∈ (0[,]+∞))
42	8, 10, 41	sge0clmpt 46445	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ∈ (0[,]+∞))
43		oveq2 7440	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (ℝ ↑_m 𝑥) = (ℝ ↑_m 𝑦))
44		eqeq1 2740	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
45		prodeq1 15944	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))
46	44, 45	ifbieq2d 4551	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))
47	43, 43, 46	mpoeq123dv 7509	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑎 ∈ (ℝ ↑_m 𝑦), 𝑏 ∈ (ℝ ↑_m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
48	47	cbvmptv 5254	. . . . . . . . 9 ⊢ (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑦), 𝑏 ∈ (ℝ ↑_m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
49	12, 48	eqtri 2764	. . . . . . . 8 ⊢ 𝐿 = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑦), 𝑏 ∈ (ℝ ↑_m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
50		diffi 9216	. . . . . . . . . . 11 ⊢ (𝑋 ∈ Fin → (𝑋 ∖ {𝐾}) ∈ Fin)
51	13, 50	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
52		snfi 9084	. . . . . . . . . . 11 ⊢ {𝐾} ∈ Fin
53	52	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {𝐾} ∈ Fin)
54		unfi 9212	. . . . . . . . . 10 ⊢ (((𝑋 ∖ {𝐾}) ∈ Fin ∧ {𝐾} ∈ Fin) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
55	51, 53, 54	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
56	55	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
57		snidg 4659	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ 𝑋 → 𝐾 ∈ {𝐾})
58	26, 57	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ {𝐾})
59		elun2 4182	. . . . . . . . . . 11 ⊢ (𝐾 ∈ {𝐾} → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
60	58, 59	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
61		neldifsnd 4792	. . . . . . . . . 10 ⊢ (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
62	60, 61	eldifd 3961	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
63	62	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
64		eqid 2736	. . . . . . . 8 ⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ((𝑋 ∖ {𝐾}) ∪ {𝐾})
65		eqid 2736	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
66		uncom 4157	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
67	66	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
68	26	snssd 4808	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐾} ⊆ 𝑋)
69		undif 4481	. . . . . . . . . . . . 13 ⊢ ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
70	68, 69	sylib 218	. . . . . . . . . . . 12 ⊢ (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
71	67, 70	eqtrd 2776	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
72	71	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
73	72	feq2d 6721	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐶‘𝑗):𝑋⟶ℝ))
74	18, 73	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
75	72	feq2d 6721	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐷‘𝑗):𝑋⟶ℝ))
76	22, 75	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
77	49, 56, 63, 64, 38, 65, 74, 76	hsphoidmvle 46606	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗)))
78	71	fveq2d 6909	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿‘𝑋))
79		eqidd 2737	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶‘𝑗) = (𝐶‘𝑗))
80	36	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))))
81	71	oveq2d 7448	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (ℝ ↑_m 𝑋))
82	71	mpteq1d 5236	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))
83	81, 82	mpteq12dv 5232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
84	83	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
85	84	mpteq2dv 5243	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))))
86	80, 85	eqtr2d 2777	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = 𝑇)
87	86	fveq1d 6907	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌) = (𝑇‘𝑌))
88	87	fveq1d 6907	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗)) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
89	78, 79, 88	oveq123d 7453	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
90	89	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
91	78	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿‘𝑋))
92	91	oveqd 7449	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗)) = ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
93	90, 92	breq12d 5155	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗)) ↔ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))
94	77, 93	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
95	8, 10, 41, 24, 94	sge0lempt 46430	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
96	35, 42, 95	ge0lere 45550	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ∈ ℝ)
97		hspmbllem2.s	. . . . . . . . . 10 ⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ)))))
98	97, 38, 14, 18	hoidifhspf 46638	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑆‘𝑌)‘(𝐶‘𝑗)):𝑋⟶ℝ)
99	12, 14, 98, 22	hoidmvcl 46602	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞))
100	99	fmpttd 7134	. . . . . . 7 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,)+∞))
101	11	a1i 11	. . . . . . 7 ⊢ (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
102	100, 101	fssd 6752	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
103	10, 102	sge0cl 46401	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ (0[,]+∞))
104	11, 99	sselid 3980	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,]+∞))
105	26	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐾 ∈ 𝑋)
106	12, 14, 18, 22, 105, 97, 38	hoidifhspdmvle 46640	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
107	8, 10, 104, 24, 106	sge0lempt 46430	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
108	35, 103, 107	ge0lere 45550	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ ℝ)
109	37	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → 𝑌 ∈ ℝ)
110	13	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → 𝑋 ∈ Fin)
111		eleq1w 2823	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑙 → (𝑗 ∈ ℕ ↔ 𝑙 ∈ ℕ))
112	111	anbi2d 630	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑙 → ((𝜑 ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ 𝑙 ∈ ℕ)))
113		fveq2 6905	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑙 → (𝐷‘𝑗) = (𝐷‘𝑙))
114	113	feq1d 6719	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑙 → ((𝐷‘𝑗):𝑋⟶ℝ ↔ (𝐷‘𝑙):𝑋⟶ℝ))
115	112, 114	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑗 = 𝑙 → (((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ) ↔ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐷‘𝑙):𝑋⟶ℝ)))
116	115, 22	chvarvv 1997	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐷‘𝑙):𝑋⟶ℝ)
117	36, 109, 110, 116	hsphoif 46596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ)
118		reex 11247	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
119	118	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ∈ V)
120	119, 13	jca 511	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
121	120	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
122		elmapg 8880	. . . . . . . . 9 ⊢ ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑_m 𝑋) ↔ ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ))
123	121, 122	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑_m 𝑋) ↔ ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ))
124	117, 123	mpbird 257	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑_m 𝑋))
125	124	fmpttd 7134	. . . . . 6 ⊢ (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))):ℕ⟶(ℝ ↑_m 𝑋))
126		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝜑)
127		elinel1 4200	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ 𝐴)
128	127	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ 𝐴)
129		hspmbllem2.a	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
130	129	sselda 3982	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
131		eliun 4994	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
132	130, 131	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
133	126, 128, 132	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
134		simpll 766	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝜑)
135		elinel2 4201	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
136	135	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
137	136	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
138		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
139		ixpfn 8944	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 Fn 𝑋)
140	139	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
141		nfv 1913	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ)
142		nfcv 2904	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘𝑓
143		nfixp1 8959	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))
144	142, 143	nfel 2919	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))
145	141, 144	nfan 1898	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
146	18	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (𝐶‘𝑗):𝑋⟶ℝ)
147		simp3 1138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
148	146, 147	ffvelcdmd 7104	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ)
149	148	rexrd 11312	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ^*)
150	149	ad5ant135 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ^*)
151	39	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝑇‘𝑌)‘(𝐷‘𝑗)):𝑋⟶ℝ)
152	151, 147	ffvelcdmd 7104	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈ ℝ)
153	152	rexrd 11312	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈ ℝ^*)
154	153	ad5ant135 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈ ℝ^*)
155		iftrue 4530	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
156		ioossre 13449	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (-∞(,)𝑌) ⊆ ℝ
157	156	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝐾 → (-∞(,)𝑌) ⊆ ℝ)
158	155, 157	eqsstrd 4017	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
159		iffalse 4533	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = ℝ)
160		ssid 4005	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℝ ⊆ ℝ
161	160	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 = 𝐾 → ℝ ⊆ ℝ)
162	159, 161	eqsstrd 4017	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
163	158, 162	pm2.61i 182	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ
164		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
165		hspmbllem2.h	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
166	165, 13, 26, 37	hspval 46629	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐾(𝐻‘𝑋)𝑌) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
167	166	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → (𝐾(𝐻‘𝑋)𝑌) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
168	164, 167	eleqtrd 2842	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
169	168	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
170		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
171		vex 3483	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑓 ∈ V
172	171	elixp 8945	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
173	172	biimpi 216	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
174	173	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
175	174	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
176		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
177		rspa 3247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
178	175, 176, 177	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
179	169, 170, 178	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
180	163, 179	sselid 3980	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
181	180	rexrd 11312	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ^*)
182	181	ad4ant14 752	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ^*)
183	149	ad4ant124 1173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ^*)
184	22	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (𝐷‘𝑗):𝑋⟶ℝ)
185	184, 147	ffvelcdmd 7104	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ)
186	185	rexrd 11312	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*)
187	186	ad4ant124 1173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*)
188	171	elixp 8945	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
189	188	biimpi 216	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
190	189	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
191	190	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
192		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
193		rspa 3247	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
194	191, 192, 193	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
195	194	adantll 714	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
196		icogelb 13439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ^* ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ^* ∧ (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
197	183, 187, 195, 196	syl3anc 1372	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
198	197	adantl3r 750	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
199		icoltub 45526	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ^* ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ^* ∧ (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
200	183, 187, 195, 199	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
201	200	adantl3r 750	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
202	201	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
203		simpll 766	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝜑)
204		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
205	203, 204	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝜑 ∧ 𝑗 ∈ ℕ))
206	205	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝜑 ∧ 𝑗 ∈ ℕ))
207		simp2 1137	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑘 = 𝐾)
208		simp3 1138	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) ≤ 𝑌)
209		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 = 𝐾 → ((𝐷‘𝑗)‘𝑘) = ((𝐷‘𝑗)‘𝐾))
210	209	breq1d 5152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝐾 → (((𝐷‘𝑗)‘𝑘) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌))
211	210	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝐾) ≤ 𝑌)
212	211	iftrued 4532	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝐾))
213	209	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝐾 → ((𝐷‘𝑗)‘𝐾) = ((𝐷‘𝑗)‘𝑘))
214	213	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝐾) = ((𝐷‘𝑗)‘𝑘))
215	212, 214	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝑘))
216	215	3adant1 1130	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝑘))
217		breq2 5146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑌 → ((𝑐‘ℎ) ≤ 𝑦 ↔ (𝑐‘ℎ) ≤ 𝑌))
218		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑌 → 𝑦 = 𝑌)
219	217, 218	ifbieq2d 4551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = 𝑌 → if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦) = if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))
220	219	ifeq2d 4545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = 𝑌 → if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)) = if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))
221	220	mpteq2dv 5243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = 𝑌 → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))))
222	221	mpteq2dv 5243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = 𝑌 → (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))))
223		ovex 7465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (ℝ ↑_m 𝑋) ∈ V
224	223	mptex 7244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))) ∈ V
225	224	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))) ∈ V)
226	36, 222, 37, 225	fvmptd3 7038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝑇‘𝑌) = (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))))
227	226	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑌) = (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))))
228		fveq1 6904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = (𝐷‘𝑗) → (𝑐‘ℎ) = ((𝐷‘𝑗)‘ℎ))
229	228	breq1d 5152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = (𝐷‘𝑗) → ((𝑐‘ℎ) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘ℎ) ≤ 𝑌))
230	229, 228	ifbieq1d 4549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = (𝐷‘𝑗) → if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌) = if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))
231	228, 230	ifeq12d 4546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = (𝐷‘𝑗) → if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)) = if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))
232	231	mpteq2dv 5243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = (𝐷‘𝑗) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
233	232	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑐 = (𝐷‘𝑗)) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
234		mptexg 7242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑋 ∈ Fin → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) ∈ V)
235	13, 234	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) ∈ V)
236	235	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) ∈ V)
237	227, 233, 20, 236	fvmptd 7022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑗)) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
238	237	fveq1d 6907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘))
239	238	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘))
240		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝜑)
241		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝑘 = 𝐾)
242	240, 26	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝐾 ∈ 𝑋)
243	241, 242	eqeltrd 2840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝑘 ∈ 𝑋)
244		eqidd 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
245		eleq1w 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑘 → (ℎ ∈ (𝑋 ∖ {𝐾}) ↔ 𝑘 ∈ (𝑋 ∖ {𝐾})))
246		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑘 → ((𝐷‘𝑗)‘ℎ) = ((𝐷‘𝑗)‘𝑘))
247	246	breq1d 5152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (ℎ = 𝑘 → (((𝐷‘𝑗)‘ℎ) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌))
248	247, 246	ifbieq1d 4549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑘 → if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌) = if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌))
249	245, 246, 248	ifbieq12d 4553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ℎ = 𝑘 → if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
250	249	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ℎ = 𝑘) → if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
251		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
252		fvexd 6920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((𝐷‘𝑗)‘𝑘) ∈ V)
253	252, 37	ifexd 4573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌) ∈ V)
254	252, 253	ifexd 4573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V)
255	254	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V)
256	244, 250, 251, 255	fvmptd 7022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
257	240, 243, 256	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
258		eleq1 2828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝐾 → (𝑘 ∈ (𝑋 ∖ {𝐾}) ↔ 𝐾 ∈ (𝑋 ∖ {𝐾})))
259	210, 209	ifbieq1d 4549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝐾 → if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
260	258, 209, 259	ifbieq12d 4553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = 𝐾 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
261	260	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
262	257, 261	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
263	262	3adant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
264		neldifsnd 4792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 = 𝐾 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
265	264	iffalsed 4535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝐾 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
266	265	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
267	239, 263, 266	3eqtrrd 2781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
268	267	3expa 1118	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
269	268	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
270	216, 269	eqtr3d 2778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
271	206, 207, 208, 270	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
272	271	ad5ant145 1370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
273	202, 272	breqtrd 5168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
274		mnfxr 11319	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ -∞ ∈ ℝ^*
275	274	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → -∞ ∈ ℝ^*)
276	37	rexrd 11312	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑌 ∈ ℝ^*)
277	276	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → 𝑌 ∈ ℝ^*)
278	277	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → 𝑌 ∈ ℝ^*)
279	179	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
280	155	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
281	279, 280	eleqtrd 2842	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ (-∞(,)𝑌))
282		iooltub 45528	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑌 ∈ ℝ^* ∧ (𝑓‘𝑘) ∈ (-∞(,)𝑌)) → (𝑓‘𝑘) < 𝑌)
283	275, 278, 281, 282	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌)
284	283	3adant1r 1177	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌)
285	284	ad4ant123 1172	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < 𝑌)
286		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌)
287	210	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝐾 → (¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌))
288	287	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌))
289	286, 288	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌)
290	289	iffalsed 4535	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = 𝑌)
291		eqidd 2737	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = 𝑌)
292	290, 291	eqtr2d 2777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
293	292	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
294	268	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
295	294	adantl3r 750	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
296	295	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
297	293, 296	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
298	285, 297	breqtrd 5168	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
299	298	adantl3r 750	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
300	273, 299	pm2.61dan 812	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
301	201	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
302	237	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝑇‘𝑌)‘(𝐷‘𝑗)) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
303	249	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) ∧ ℎ = 𝑘) → if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
304	255	3adant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V)
305	302, 303, 147, 304	fvmptd 7022	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
306	305	3expa 1118	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
307	306	adantllr 719	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
308	307	ad4ant13 751	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
309		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ 𝑋)
310		neqne 2947	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑘 = 𝐾 → 𝑘 ≠ 𝐾)
311		nelsn 4665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ≠ 𝐾 → ¬ 𝑘 ∈ {𝐾})
312	310, 311	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ 𝑘 = 𝐾 → ¬ 𝑘 ∈ {𝐾})
313	312	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → ¬ 𝑘 ∈ {𝐾})
314	309, 313	eldifd 3961	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ (𝑋 ∖ {𝐾}))
315	314	iftrued 4532	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = ((𝐷‘𝑗)‘𝑘))
316	315	adantll 714	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = ((𝐷‘𝑗)‘𝑘))
317	308, 316	eqtr2d 2777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
318	301, 317	breqtrd 5168	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
319	300, 318	pm2.61dan 812	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
320	150, 154, 182, 198, 319	elicod 13438	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
321	320	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑘 ∈ 𝑋 → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
322	145, 321	ralrimi 3256	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
323	140, 322	jca 511	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
324	171	elixp 8945	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
325	323, 324	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
326	325	ex 412	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
327	134, 137, 138, 326	syl21anc 837	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
328	327	reximdva 3167	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
329	133, 328	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
330		eliun 4994	. . . . . . . . . 10 ⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
331	329, 330	sylibr 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
332	331	ralrimiva 3145	. . . . . . . 8 ⊢ (𝜑 → ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
333		dfss3 3971	. . . . . . . 8 ⊢ ((𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
334	332, 333	sylibr 234	. . . . . . 7 ⊢ (𝜑 → (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
335		eqidd 2737	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))))
336		2fveq3 6910	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑗 → ((𝑇‘𝑌)‘(𝐷‘𝑙)) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
337	336	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑇‘𝑌)‘(𝐷‘𝑙)) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
338		id 22	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
339		fvexd 6920	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → ((𝑇‘𝑌)‘(𝐷‘𝑗)) ∈ V)
340	335, 337, 338, 339	fvmptd 7022	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
341	340	fveq1d 6907	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
342	341	oveq2d 7448	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
343	342	ixpeq2dv 8954	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
344	343	iuneq2i 5012	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
345	334, 344	sseqtrrdi 4024	. . . . . 6 ⊢ (𝜑 → (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)))
346	13, 15, 125, 345, 12	ovnlecvr2 46630	. . . . 5 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)))))
347	340	oveq2d 7448	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
348	347	mpteq2ia 5244	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
349	348	fveq2i 6908	. . . . . 6 ⊢ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗)))))
350	349	a1i 11	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))))
351	346, 350	breqtrd 5168	. . . 4 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))))
352	15	ffvelcdmda 7103	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐶‘𝑙) ∈ (ℝ ↑_m 𝑋))
353		elmapi 8890	. . . . . . . . . 10 ⊢ ((𝐶‘𝑙) ∈ (ℝ ↑_m 𝑋) → (𝐶‘𝑙):𝑋⟶ℝ)
354	352, 353	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐶‘𝑙):𝑋⟶ℝ)
355	97, 109, 110, 354	hoidifhspf 46638	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ)
356		elmapg 8880	. . . . . . . . . 10 ⊢ ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑_m 𝑋) ↔ ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ))
357	120, 356	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑_m 𝑋) ↔ ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ))
358	357	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑_m 𝑋) ↔ ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ))
359	355, 358	mpbird 257	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑_m 𝑋))
360	359	fmpttd 7134	. . . . . 6 ⊢ (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))):ℕ⟶(ℝ ↑_m 𝑋))
361		simpl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝜑)
362		eldifi 4130	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ 𝐴)
363	362	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ 𝐴)
364	361, 363, 132	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
365	139	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
366		nfv 1913	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ)
367	366, 144	nfan 1898	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
368	98	3adant3 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝑆‘𝑌)‘(𝐶‘𝑗)):𝑋⟶ℝ)
369	368, 147	ffvelcdmd 7104	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ∈ ℝ)
370	369	rexrd 11312	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ∈ ℝ^*)
371	370	ad5ant135 1369	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ∈ ℝ^*)
372	187	adantl3r 750	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*)
373	148	3expa 1118	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ)
374	186	3expa 1118	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*)
375		icossre 13469	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ)
376	373, 374, 375	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ)
377	376	adantlr 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ)
378	377, 195	sseldd 3983	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
379	378	rexrd 11312	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ^*)
380	379	adantl3r 750	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ^*)
381	38	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → 𝑌 ∈ ℝ)
382	14	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → 𝑋 ∈ Fin)
383	97, 381, 382, 146, 147	hoidifhspval3 46639	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)))
384	383	ad5ant134 1368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)))
385		iftrue 4530	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
386	385	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
387	384, 386	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
388	387	adantllr 719	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
389		iftrue 4530	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑌 ≤ ((𝐶‘𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = ((𝐶‘𝑗)‘𝑘))
390	389	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = ((𝐶‘𝑗)‘𝑘))
391	197	adantl3r 750	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
392	391	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
393	390, 392	eqbrtrd 5164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘))
394		iffalse 4533	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = 𝑌)
395	394	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = 𝑌)
396		simpl1 1191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))))
397		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑌 ≤ (𝑓‘𝑘))
398		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 = 𝐾 → (𝑓‘𝑘) = (𝑓‘𝐾))
399	398	breq2d 5154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 = 𝐾 → (𝑌 ≤ (𝑓‘𝑘) ↔ 𝑌 ≤ (𝑓‘𝐾)))
400	399	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝐾 → (¬ 𝑌 ≤ (𝑓‘𝑘) ↔ ¬ 𝑌 ≤ (𝑓‘𝐾)))
401	400	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (¬ 𝑌 ≤ (𝑓‘𝑘) ↔ ¬ 𝑌 ≤ (𝑓‘𝐾)))
402	397, 401	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑌 ≤ (𝑓‘𝐾))
403	402	3ad2antl3 1187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑌 ≤ (𝑓‘𝐾))
404	398	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 = 𝐾 → (𝑓‘𝐾) = (𝑓‘𝑘))
405	404	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝐾) = (𝑓‘𝑘))
406	364	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
407		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝜑 ∧ 𝑗 ∈ ℕ))
408	407	ad4ant13 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝜑 ∧ 𝑗 ∈ ℕ))
409		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
410	251	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑘 ∈ 𝑋)
411	408, 409, 410, 378	syl21anc 837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓‘𝑘) ∈ ℝ)
412	411	rexlimdva2 3156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓‘𝑘) ∈ ℝ))
413	412	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓‘𝑘) ∈ ℝ))
414	406, 413	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
415	414	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ ℝ)
416	405, 415	eqeltrd 2840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝐾) ∈ ℝ)
417	416	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝑓‘𝐾) ∈ ℝ)
418	396, 361, 37	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → 𝑌 ∈ ℝ)
419	417, 418	ltnled 11409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ((𝑓‘𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝑓‘𝐾)))
420	403, 419	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝑓‘𝐾) < 𝑌)
421	365, 364	r19.29a 3161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 Fn 𝑋)
422	421	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) → 𝑓 Fn 𝑋)
423	274	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → -∞ ∈ ℝ^*)
424	276	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ∈ ℝ^*)
425	414	ad4ant13 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ ℝ)
426	425	mnfltd 13167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → -∞ < (𝑓‘𝑘))
427	398	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) = (𝑓‘𝐾))
428		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝐾) < 𝑌)
429	427, 428	eqbrtrd 5164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌)
430	429	ad4ant24 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌)
431	423, 424, 425, 426, 430	eliood 45516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ (-∞(,)𝑌))
432	155	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 = 𝐾 → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
433	432	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
434	431, 433	eleqtrd 2842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
435	414	ad4ant13 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ ℝ)
436	159	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ 𝑘 = 𝐾 → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
437	436	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
438	435, 437	eleqtrd 2842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
439	434, 438	pm2.61dan 812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
440	439	ralrimiva 3145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
441	422, 440	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
442	396, 420, 441	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
443	442, 172	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
444	166	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌))
445	444	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌))
446	445	3ad2antl1 1185	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌))
447	443, 446	eleqtrd 2842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
448		eldifn 4131	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
449	448	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
450	449	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
451	450	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
452	447, 451	condan 817	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → 𝑌 ≤ (𝑓‘𝑘))
453	452	ad5ant145 1370	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ≤ (𝑓‘𝑘))
454	453	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → 𝑌 ≤ (𝑓‘𝑘))
455	395, 454	eqbrtrd 5164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘))
456	393, 455	pm2.61dan 812	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘))
457	388, 456	eqbrtrd 5164	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘))
458	383	ad5ant124 1366	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)))
459		iffalse 4533	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = ((𝐶‘𝑗)‘𝑘))
460	459	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = ((𝐶‘𝑗)‘𝑘))
461	458, 460	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = ((𝐶‘𝑗)‘𝑘))
462	197	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
463	461, 462	eqbrtrd 5164	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘))
464	463	adantl4r 755	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘))
465	457, 464	pm2.61dan 812	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘))
466	200	adantl3r 750	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
467	371, 372, 380, 465, 466	elicod 13438	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
468	467	ex 412	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑘 ∈ 𝑋 → (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
469	367, 468	ralrimi 3256	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
470	365, 469	jca 511	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
471	171	elixp 8945	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
472	470, 471	sylibr 234	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
473		eqidd 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))))
474		2fveq3 6910	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 = 𝑗 → ((𝑆‘𝑌)‘(𝐶‘𝑙)) = ((𝑆‘𝑌)‘(𝐶‘𝑗)))
475	474	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑆‘𝑌)‘(𝐶‘𝑙)) = ((𝑆‘𝑌)‘(𝐶‘𝑗)))
476		fvexd 6920	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((𝑆‘𝑌)‘(𝐶‘𝑗)) ∈ V)
477	473, 475, 338, 476	fvmptd 7022	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗) = ((𝑆‘𝑌)‘(𝐶‘𝑗)))
478	477	fveq1d 6907	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘) = (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘))
479	478	oveq1d 7447	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
480	479	ixpeq2dv 8954	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
481	480	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
482	481	eleq2d 2826	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
483	472, 482	mpbird 257	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
484	483	ex 412	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
485	484	reximdva 3167	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
486	364, 485	mpd 15	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
487		eliun 4994	. . . . . . . . 9 ⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
488	486, 487	sylibr 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
489	488	ralrimiva 3145	. . . . . . 7 ⊢ (𝜑 → ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
490		dfss3 3971	. . . . . . 7 ⊢ ((𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
491	489, 490	sylibr 234	. . . . . 6 ⊢ (𝜑 → (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
492	13, 360, 19, 491, 12	ovnlecvr2 46630	. . . . 5 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
493	477	oveq1d 7447	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))
494	493	mpteq2ia 5244	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))
495	494	fveq2i 6908	. . . . . 6 ⊢ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))
496	495	a1i 11	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))
497	492, 496	breqtrd 5168	. . . 4 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))
498	1, 2, 96, 108, 351, 497	leadd12dd 45333	. . 3 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) + (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
499	14, 105, 38, 18, 22, 12, 36, 97	hspmbllem1 46646	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))
500	499	mpteq2dva 5241	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))
501	500	fveq2d 6909	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
502	8, 10, 41, 104	sge0xadd 46455	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) = ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) +_𝑒 (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
503	96, 108	rexaddd 13277	. . . 4 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) +_𝑒 (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) = ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) + (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
504	501, 502, 503	3eqtrrd 2781	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) + (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
505	498, 504	breqtrd 5168	. 2 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
506	3, 35, 7, 505, 34	letrd 11419	1 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2939 ∀wral 3060 ∃wrex 3069 Vcvv 3479 ∖ cdif 3947 ∪ cun 3948 ∩ cin 3949 ⊆ wss 3950 ∅c0 4332 ifcif 4524 {csn 4625 ∪ ciun 4990 class class class wbr 5142 ↦ cmpt 5224 Fn wfn 6555 ⟶wf 6556 ‘cfv 6560 (class class class)co 7432 ∈ cmpo 7434 ↑_m cmap 8867 Xcixp 8938 Fincfn 8986 ℝcr 11155 0cc0 11156 + caddc 11159 +∞cpnf 11293 -∞cmnf 11294 ℝ^*cxr 11295 < clt 11296 ≤ cle 11297 ℕcn 12267 ℝ⁺crp 13035 +_𝑒 cxad 13153 (,)cioo 13388 [,)cico 13390 [,]cicc 13391 ∏cprod 15940 volcvol 25499 Σ^{^}csumge0 46382 voln*covoln 46556

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5278 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 ax-inf2 9682 ax-cnex 11212 ax-resscn 11213 ax-1cn 11214 ax-icn 11215 ax-addcl 11216 ax-addrcl 11217 ax-mulcl 11218 ax-mulrcl 11219 ax-mulcom 11220 ax-addass 11221 ax-mulass 11222 ax-distr 11223 ax-i2m1 11224 ax-1ne0 11225 ax-1rid 11226 ax-rnegex 11227 ax-rrecex 11228 ax-cnre 11229 ax-pre-lttri 11230 ax-pre-lttrn 11231 ax-pre-ltadd 11232 ax-pre-mulgt0 11233 ax-pre-sup 11234

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-int 4946 df-iun 4992 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-se 5637 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-isom 6569 df-riota 7389 df-ov 7435 df-oprab 7436 df-mpo 7437 df-of 7698 df-om 7889 df-1st 8015 df-2nd 8016 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-rdg 8451 df-1o 8507 df-2o 8508 df-er 8746 df-map 8869 df-pm 8870 df-ixp 8939 df-en 8987 df-dom 8988 df-sdom 8989 df-fin 8990 df-fi 9452 df-sup 9483 df-inf 9484 df-oi 9551 df-dju 9942 df-card 9980 df-pnf 11298 df-mnf 11299 df-xr 11300 df-ltxr 11301 df-le 11302 df-sub 11495 df-neg 11496 df-div 11922 df-nn 12268 df-2 12330 df-3 12331 df-n0 12529 df-z 12616 df-uz 12880 df-q 12992 df-rp 13036 df-xneg 13155 df-xadd 13156 df-xmul 13157 df-ioo 13392 df-ico 13394 df-icc 13395 df-fz 13549 df-fzo 13696 df-fl 13833 df-seq 14044 df-exp 14104 df-hash 14371 df-cj 15139 df-re 15140 df-im 15141 df-sqrt 15275 df-abs 15276 df-clim 15525 df-rlim 15526 df-sum 15724 df-prod 15941 df-rest 17468 df-topgen 17489 df-psmet 21357 df-xmet 21358 df-met 21359 df-bl 21360 df-mopn 21361 df-top 22901 df-topon 22918 df-bases 22954 df-cmp 23396 df-ovol 25500 df-vol 25501 df-sumge0 46383 df-ovoln 46557

This theorem is referenced by: hspmbllem3 46648

W3C validator