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 42471

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	⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑_𝑚 𝑋))
hspmbllem2.d	⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑_𝑚 𝑋))
hspmbllem2.a	⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
hspmbllem2.g	⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
hspmbllem2.r	⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ)
hspmbllem2.i	⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ)
hspmbllem2.f	⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ)
hspmbllem2.l	⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_𝑚 𝑥), 𝑏 ∈ (ℝ ↑_𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
hspmbllem2.t	⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
hspmbllem2.s	⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ 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 10516	. 2 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ∈ ℝ)
4		hspmbllem2.r	. . . 4 ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ)
5		hspmbllem2.e	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
6	5	rpred 12281	. . . 4 ⊢ (𝜑 → 𝐸 ∈ ℝ)
7	4, 6	readdcld 10516	. . 3 ⊢ (𝜑 → (((voln*‘𝑋)‘𝐴) + 𝐸) ∈ ℝ)
8		nfv 1892	. . . 4 ⊢ Ⅎ𝑗𝜑
9		nnex 11492	. . . . 5 ⊢ ℕ ∈ V
10	9	a1i 11	. . . 4 ⊢ (𝜑 → ℕ ∈ V)
11		icossicc 12674	. . . . 5 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
12		hspmbllem2.l	. . . . . 6 ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_𝑚 𝑥), 𝑏 ∈ (ℝ ↑_𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
13		hspmbllem2.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ Fin)
14	13	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
15		hspmbllem2.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑_𝑚 𝑋))
16	15	ffvelrnda 6716	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑_𝑚 𝑋))
17		elmapi 8278	. . . . . . 7 ⊢ ((𝐶‘𝑗) ∈ (ℝ ↑_𝑚 𝑋) → (𝐶‘𝑗):𝑋⟶ℝ)
18	16, 17	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑋⟶ℝ)
19		hspmbllem2.d	. . . . . . . 8 ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑_𝑚 𝑋))
20	19	ffvelrnda 6716	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑_𝑚 𝑋))
21		elmapi 8278	. . . . . . 7 ⊢ ((𝐷‘𝑗) ∈ (ℝ ↑_𝑚 𝑋) → (𝐷‘𝑗):𝑋⟶ℝ)
22	20, 21	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ)
23	12, 14, 18, 22	hoidmvcl 42426	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞))
24	11, 23	sseldi 3887	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,]+∞))
25	8, 10, 24	sge0clmpt 42269	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ (0[,]+∞))
26		hspmbllem2.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
27		ne0i 4220	. . . . . . . . 9 ⊢ (𝐾 ∈ 𝑋 → 𝑋 ≠ ∅)
28	26, 27	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ≠ ∅)
29	28	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
30	12, 14, 29, 18, 22	hoidmvn0val 42428	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
31	30	mpteq2dva 5055	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))))
32	31	fveq2d 6542	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))))
33		hspmbllem2.g	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
34	32, 33	eqbrtrd 4984	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
35	7, 25, 34	ge0lere 41369	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ ℝ)
36		hspmbllem2.t	. . . . . . . . 9 ⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
37		hspmbllem2.y	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ ℝ)
38	37	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑌 ∈ ℝ)
39	36, 38, 14, 22	hsphoif 42420	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑗)):𝑋⟶ℝ)
40	12, 14, 18, 39	hoidmvcl 42426	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ∈ (0[,)+∞))
41	11, 40	sseldi 3887	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ∈ (0[,]+∞))
42	8, 10, 41	sge0clmpt 42269	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ∈ (0[,]+∞))
43		oveq2 7024	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (ℝ ↑_𝑚 𝑥) = (ℝ ↑_𝑚 𝑦))
44		eqeq1 2799	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
45		prodeq1 15096	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))
46	44, 45	ifbieq2d 4406	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))
47	43, 43, 46	mpoeq123dv 7087	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑎 ∈ (ℝ ↑_𝑚 𝑥), 𝑏 ∈ (ℝ ↑_𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑎 ∈ (ℝ ↑_𝑚 𝑦), 𝑏 ∈ (ℝ ↑_𝑚 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
48	47	cbvmptv 5061	. . . . . . . . 9 ⊢ (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_𝑚 𝑥), 𝑏 ∈ (ℝ ↑_𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_𝑚 𝑦), 𝑏 ∈ (ℝ ↑_𝑚 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
49	12, 48	eqtri 2819	. . . . . . . 8 ⊢ 𝐿 = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_𝑚 𝑦), 𝑏 ∈ (ℝ ↑_𝑚 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
50		diffi 8596	. . . . . . . . . . 11 ⊢ (𝑋 ∈ Fin → (𝑋 ∖ {𝐾}) ∈ Fin)
51	13, 50	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
52		snfi 8442	. . . . . . . . . . 11 ⊢ {𝐾} ∈ Fin
53	52	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {𝐾} ∈ Fin)
54		unfi 8631	. . . . . . . . . 10 ⊢ (((𝑋 ∖ {𝐾}) ∈ Fin ∧ {𝐾} ∈ Fin) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
55	51, 53, 54	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
56	55	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
57		snidg 4504	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ 𝑋 → 𝐾 ∈ {𝐾})
58	26, 57	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ {𝐾})
59		elun2 4074	. . . . . . . . . . 11 ⊢ (𝐾 ∈ {𝐾} → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
60	58, 59	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
61		neldifsnd 4633	. . . . . . . . . 10 ⊢ (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
62	60, 61	eldifd 3870	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
63	62	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
64		eqid 2795	. . . . . . . 8 ⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ((𝑋 ∖ {𝐾}) ∪ {𝐾})
65		eqid 2795	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
66		uncom 4050	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
67	66	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
68	26	snssd 4649	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐾} ⊆ 𝑋)
69		undif 4344	. . . . . . . . . . . . 13 ⊢ ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
70	68, 69	sylib 219	. . . . . . . . . . . 12 ⊢ (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
71	67, 70	eqtrd 2831	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
72	71	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
73	72	feq2d 6368	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐶‘𝑗):𝑋⟶ℝ))
74	18, 73	mpbird 258	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
75	72	feq2d 6368	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐷‘𝑗):𝑋⟶ℝ))
76	22, 75	mpbird 258	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
77	49, 56, 63, 64, 38, 65, 74, 76	hsphoidmvle 42430	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗)))
78	71	fveq2d 6542	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿‘𝑋))
79		eqidd 2796	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶‘𝑗) = (𝐶‘𝑗))
80	36	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))))
81	71	oveq2d 7032	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℝ ↑_𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (ℝ ↑_𝑚 𝑋))
82	71	mpteq1d 5049	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))
83	81, 82	mpteq12dv 5045	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑐 ∈ (ℝ ↑_𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
84	83	eqcomd 2801	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑_𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
85	84	mpteq2dv 5056	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))))
86	80, 85	eqtr2d 2832	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = 𝑇)
87	86	fveq1d 6540	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌) = (𝑇‘𝑌))
88	87	fveq1d 6540	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗)) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
89	78, 79, 88	oveq123d 7037	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
90	89	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
91	78	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿‘𝑋))
92	91	oveqd 7033	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗)) = ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
93	90, 92	breq12d 4975	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗)) ↔ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))
94	77, 93	mpbid 233	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
95	8, 10, 41, 24, 94	sge0lempt 42254	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
96	35, 42, 95	ge0lere 41369	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ∈ ℝ)
97		hspmbllem2.s	. . . . . . . . . 10 ⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ)))))
98	97, 38, 14, 18	hoidifhspf 42462	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑆‘𝑌)‘(𝐶‘𝑗)):𝑋⟶ℝ)
99	12, 14, 98, 22	hoidmvcl 42426	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞))
100	99	fmpttd 6742	. . . . . . 7 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,)+∞))
101	11	a1i 11	. . . . . . 7 ⊢ (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
102	100, 101	fssd 6396	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
103	10, 102	sge0cl 42225	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ (0[,]+∞))
104	11, 99	sseldi 3887	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,]+∞))
105	26	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐾 ∈ 𝑋)
106	12, 14, 18, 22, 105, 97, 38	hoidifhspdmvle 42464	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
107	8, 10, 104, 24, 106	sge0lempt 42254	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
108	35, 103, 107	ge0lere 41369	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ ℝ)
109	37	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → 𝑌 ∈ ℝ)
110	13	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → 𝑋 ∈ Fin)
111		eleq1w 2865	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑙 → (𝑗 ∈ ℕ ↔ 𝑙 ∈ ℕ))
112	111	anbi2d 628	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑙 → ((𝜑 ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ 𝑙 ∈ ℕ)))
113		fveq2 6538	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑙 → (𝐷‘𝑗) = (𝐷‘𝑙))
114	113	feq1d 6367	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑙 → ((𝐷‘𝑗):𝑋⟶ℝ ↔ (𝐷‘𝑙):𝑋⟶ℝ))
115	112, 114	imbi12d 346	. . . . . . . . . 10 ⊢ (𝑗 = 𝑙 → (((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ) ↔ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐷‘𝑙):𝑋⟶ℝ)))
116	115, 22	chvarv 2370	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐷‘𝑙):𝑋⟶ℝ)
117	36, 109, 110, 116	hsphoif 42420	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ)
118		reex 10474	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
119	118	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ∈ V)
120	119, 13	jca 512	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
121	120	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
122		elmapg 8269	. . . . . . . . 9 ⊢ ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑_𝑚 𝑋) ↔ ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ))
123	121, 122	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑_𝑚 𝑋) ↔ ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ))
124	117, 123	mpbird 258	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑_𝑚 𝑋))
125	124	fmpttd 6742	. . . . . 6 ⊢ (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))):ℕ⟶(ℝ ↑_𝑚 𝑋))
126		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝜑)
127		elinel1 4093	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ 𝐴)
128	127	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ 𝐴)
129		hspmbllem2.a	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
130	129	sselda 3889	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
131		eliun 4829	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
132	130, 131	sylib 219	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
133	126, 128, 132	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
134		simpll 763	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝜑)
135		elinel2 4094	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
136	135	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
137	136	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
138		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
139		ixpfn 8316	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 Fn 𝑋)
140	139	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
141		nfv 1892	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ)
142		nfcv 2949	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘𝑓
143		nfixp1 8330	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))
144	142, 143	nfel 2961	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))
145	141, 144	nfan 1881	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
146	18	3adant3 1125	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (𝐶‘𝑗):𝑋⟶ℝ)
147		simp3 1131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
148	146, 147	ffvelrnd 6717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ)
149	148	rexrd 10537	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ^*)
150	149	ad5ant135 1361	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ^*)
151	39	3adant3 1125	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝑇‘𝑌)‘(𝐷‘𝑗)):𝑋⟶ℝ)
152	151, 147	ffvelrnd 6717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈ ℝ)
153	152	rexrd 10537	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈ ℝ^*)
154	153	ad5ant135 1361	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈ ℝ^*)
155		iftrue 4387	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
156		ioossre 12648	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (-∞(,)𝑌) ⊆ ℝ
157	156	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝐾 → (-∞(,)𝑌) ⊆ ℝ)
158	155, 157	eqsstrd 3926	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
159		iffalse 4390	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = ℝ)
160		ssid 3910	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℝ ⊆ ℝ
161	160	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 = 𝐾 → ℝ ⊆ ℝ)
162	159, 161	eqsstrd 3926	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
163	158, 162	pm2.61i 183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ
164		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
165		hspmbllem2.h	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
166	165, 13, 26, 37	hspval 42453	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐾(𝐻‘𝑋)𝑌) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
167	166	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → (𝐾(𝐻‘𝑋)𝑌) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
168	164, 167	eleqtrd 2885	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
169	168	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
170		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
171		vex 3440	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑓 ∈ V
172	171	elixp 8317	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
173	172	biimpi 217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
174	173	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
175	174	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
176		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
177		rspa 3173	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
178	175, 176, 177	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
179	169, 170, 178	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
180	163, 179	sseldi 3887	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
181	180	rexrd 10537	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ^*)
182	181	ad4ant14 748	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ^*)
183	149	ad4ant124 1166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ^*)
184	22	3adant3 1125	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (𝐷‘𝑗):𝑋⟶ℝ)
185	184, 147	ffvelrnd 6717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ)
186	185	rexrd 10537	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*)
187	186	ad4ant124 1166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*)
188	171	elixp 8317	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
189	188	biimpi 217	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
190	189	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
191	190	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
192		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
193		rspa 3173	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
194	191, 192, 193	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
195	194	adantll 710	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
196		icogelb 12638	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ^* ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ^* ∧ (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
197	183, 187, 195, 196	syl3anc 1364	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
198	197	adantl3r 746	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
199		icoltub 41345	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ^* ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ^* ∧ (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
200	183, 187, 195, 199	syl3anc 1364	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
201	200	adantl3r 746	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
202	201	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
203		simpll 763	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝜑)
204		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
205	203, 204	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝜑 ∧ 𝑗 ∈ ℕ))
206	205	3ad2ant1 1126	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝜑 ∧ 𝑗 ∈ ℕ))
207		simp2 1130	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑘 = 𝐾)
208		simp3 1131	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) ≤ 𝑌)
209		fveq2 6538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 = 𝐾 → ((𝐷‘𝑗)‘𝑘) = ((𝐷‘𝑗)‘𝐾))
210	209	breq1d 4972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝐾 → (((𝐷‘𝑗)‘𝑘) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌))
211	210	biimpa 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝐾) ≤ 𝑌)
212	211	iftrued 4389	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝐾))
213	209	eqcomd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝐾 → ((𝐷‘𝑗)‘𝐾) = ((𝐷‘𝑗)‘𝑘))
214	213	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝐾) = ((𝐷‘𝑗)‘𝑘))
215	212, 214	eqtrd 2831	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝑘))
216	215	3adant1 1123	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝑘))
217		breq2 4966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑌 → ((𝑐‘ℎ) ≤ 𝑦 ↔ (𝑐‘ℎ) ≤ 𝑌))
218		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑌 → 𝑦 = 𝑌)
219	217, 218	ifbieq2d 4406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = 𝑌 → if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦) = if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))
220	219	ifeq2d 4400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = 𝑌 → if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)) = if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))
221	220	mpteq2dv 5056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = 𝑌 → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))))
222	221	mpteq2dv 5056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = 𝑌 → (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))))
223		ovex 7048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (ℝ ↑_𝑚 𝑋) ∈ V
224	223	mptex 6852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))) ∈ V
225	224	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))) ∈ V)
226	36, 222, 37, 225	fvmptd3 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝑇‘𝑌) = (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))))
227	226	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑌) = (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))))
228		fveq1 6537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = (𝐷‘𝑗) → (𝑐‘ℎ) = ((𝐷‘𝑗)‘ℎ))
229	228	breq1d 4972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = (𝐷‘𝑗) → ((𝑐‘ℎ) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘ℎ) ≤ 𝑌))
230	229, 228	ifbieq1d 4404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = (𝐷‘𝑗) → if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌) = if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))
231	228, 230	ifeq12d 4401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = (𝐷‘𝑗) → if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)) = if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))
232	231	mpteq2dv 5056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = (𝐷‘𝑗) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
233	232	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑐 = (𝐷‘𝑗)) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
234		mptexg 6850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑋 ∈ Fin → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) ∈ V)
235	13, 234	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) ∈ V)
236	235	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) ∈ V)
237	227, 233, 20, 236	fvmptd 6641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑗)) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
238	237	fveq1d 6540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘))
239	238	3adant3 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘))
240		simpl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝜑)
241		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝑘 = 𝐾)
242	240, 26	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝐾 ∈ 𝑋)
243	241, 242	eqeltrd 2883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝑘 ∈ 𝑋)
244		eqidd 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
245		eleq1w 2865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑘 → (ℎ ∈ (𝑋 ∖ {𝐾}) ↔ 𝑘 ∈ (𝑋 ∖ {𝐾})))
246		fveq2 6538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑘 → ((𝐷‘𝑗)‘ℎ) = ((𝐷‘𝑗)‘𝑘))
247	246	breq1d 4972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (ℎ = 𝑘 → (((𝐷‘𝑗)‘ℎ) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌))
248	247, 246	ifbieq1d 4404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑘 → if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌) = if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌))
249	245, 246, 248	ifbieq12d 4408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ℎ = 𝑘 → if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
250	249	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ℎ = 𝑘) → if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
251		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
252		fvexd 6553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((𝐷‘𝑗)‘𝑘) ∈ V)
253		ifexg 4428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝐷‘𝑗)‘𝑘) ∈ V ∧ 𝑌 ∈ ℝ) → if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌) ∈ V)
254	252, 37, 253	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌) ∈ V)
255		ifexg 4428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝐷‘𝑗)‘𝑘) ∈ V ∧ if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌) ∈ V) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V)
256	252, 254, 255	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V)
257	256	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V)
258	244, 250, 251, 257	fvmptd 6641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
259	240, 243, 258	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
260		eleq1 2870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝐾 → (𝑘 ∈ (𝑋 ∖ {𝐾}) ↔ 𝐾 ∈ (𝑋 ∖ {𝐾})))
261	210, 209	ifbieq1d 4404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝐾 → if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
262	260, 209, 261	ifbieq12d 4408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = 𝐾 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
263	262	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
264	259, 263	eqtrd 2831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
265	264	3adant2 1124	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
266		neldifsnd 4633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 = 𝐾 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
267	266	iffalsed 4392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝐾 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
268	267	3ad2ant3 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
269	239, 265, 268	3eqtrrd 2836	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
270	269	3expa 1111	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
271	270	3adant3 1125	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
272	216, 271	eqtr3d 2833	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
273	206, 207, 208, 272	syl3anc 1364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
274	273	ad5ant145 1362	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
275	202, 274	breqtrd 4988	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
276		mnfxr 10545	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ -∞ ∈ ℝ^*
277	276	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → -∞ ∈ ℝ^*)
278	37	rexrd 10537	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑌 ∈ ℝ^*)
279	278	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → 𝑌 ∈ ℝ^*)
280	279	3ad2ant1 1126	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → 𝑌 ∈ ℝ^*)
281	179	3adant3 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
282	155	3ad2ant3 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
283	281, 282	eleqtrd 2885	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ (-∞(,)𝑌))
284		iooltub 41347	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑌 ∈ ℝ^* ∧ (𝑓‘𝑘) ∈ (-∞(,)𝑌)) → (𝑓‘𝑘) < 𝑌)
285	277, 280, 283, 284	syl3anc 1364	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌)
286	285	3adant1r 1170	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌)
287	286	ad4ant123 1165	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < 𝑌)
288		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌)
289	210	notbid 319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝐾 → (¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌))
290	289	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌))
291	288, 290	mpbid 233	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌)
292	291	iffalsed 4392	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = 𝑌)
293		eqidd 2796	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = 𝑌)
294	292, 293	eqtr2d 2832	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
295	294	adantll 710	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
296	270	adantlr 711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
297	296	adantl3r 746	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
298	297	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
299	295, 298	eqtrd 2831	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
300	287, 299	breqtrd 4988	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
301	300	adantl3r 746	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
302	275, 301	pm2.61dan 809	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
303	201	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
304	237	3adant3 1125	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝑇‘𝑌)‘(𝐷‘𝑗)) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
305	249	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) ∧ ℎ = 𝑘) → if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
306	257	3adant2 1124	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V)
307	304, 305, 147, 306	fvmptd 6641	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
308	307	3expa 1111	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
309	308	adantllr 715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
310	309	ad4ant13 747	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
311		simpl 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ 𝑋)
312		neqne 2992	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑘 = 𝐾 → 𝑘 ≠ 𝐾)
313		nelsn 4510	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ≠ 𝐾 → ¬ 𝑘 ∈ {𝐾})
314	312, 313	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ 𝑘 = 𝐾 → ¬ 𝑘 ∈ {𝐾})
315	314	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → ¬ 𝑘 ∈ {𝐾})
316	311, 315	eldifd 3870	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ (𝑋 ∖ {𝐾}))
317	316	iftrued 4389	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = ((𝐷‘𝑗)‘𝑘))
318	317	adantll 710	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = ((𝐷‘𝑗)‘𝑘))
319	310, 318	eqtr2d 2832	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
320	303, 319	breqtrd 4988	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
321	302, 320	pm2.61dan 809	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
322	150, 154, 182, 198, 321	elicod 12637	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
323	322	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑘 ∈ 𝑋 → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
324	145, 323	ralrimi 3183	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
325	140, 324	jca 512	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
326	171	elixp 8317	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
327	325, 326	sylibr 235	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
328	327	ex 413	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
329	134, 137, 138, 328	syl21anc 834	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
330	329	reximdva 3237	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
331	133, 330	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
332		eliun 4829	. . . . . . . . . 10 ⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
333	331, 332	sylibr 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
334	333	ralrimiva 3149	. . . . . . . 8 ⊢ (𝜑 → ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
335		dfss3 3878	. . . . . . . 8 ⊢ ((𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
336	334, 335	sylibr 235	. . . . . . 7 ⊢ (𝜑 → (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
337		eqidd 2796	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))))
338		2fveq3 6543	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑗 → ((𝑇‘𝑌)‘(𝐷‘𝑙)) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
339	338	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑇‘𝑌)‘(𝐷‘𝑙)) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
340		id 22	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
341		fvexd 6553	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → ((𝑇‘𝑌)‘(𝐷‘𝑗)) ∈ V)
342	337, 339, 340, 341	fvmptd 6641	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
343	342	fveq1d 6540	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
344	343	oveq2d 7032	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
345	344	ixpeq2dv 8326	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
346	345	iuneq2i 4845	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
347	336, 346	syl6sseqr 3939	. . . . . 6 ⊢ (𝜑 → (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)))
348	13, 15, 125, 347, 12	ovnlecvr2 42454	. . . . 5 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)))))
349	342	oveq2d 7032	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
350	349	mpteq2ia 5051	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
351	350	fveq2i 6541	. . . . . 6 ⊢ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗)))))
352	351	a1i 11	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))))
353	348, 352	breqtrd 4988	. . . 4 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))))
354	15	ffvelrnda 6716	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐶‘𝑙) ∈ (ℝ ↑_𝑚 𝑋))
355		elmapi 8278	. . . . . . . . . 10 ⊢ ((𝐶‘𝑙) ∈ (ℝ ↑_𝑚 𝑋) → (𝐶‘𝑙):𝑋⟶ℝ)
356	354, 355	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐶‘𝑙):𝑋⟶ℝ)
357	97, 109, 110, 356	hoidifhspf 42462	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ)
358		elmapg 8269	. . . . . . . . . 10 ⊢ ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑_𝑚 𝑋) ↔ ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ))
359	120, 358	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑_𝑚 𝑋) ↔ ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ))
360	359	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑_𝑚 𝑋) ↔ ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ))
361	357, 360	mpbird 258	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑_𝑚 𝑋))
362	361	fmpttd 6742	. . . . . 6 ⊢ (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))):ℕ⟶(ℝ ↑_𝑚 𝑋))
363		simpl 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝜑)
364		eldifi 4024	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ 𝐴)
365	364	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ 𝐴)
366	363, 365, 132	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
367	139	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
368		nfv 1892	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ)
369	368, 144	nfan 1881	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
370	98	3adant3 1125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝑆‘𝑌)‘(𝐶‘𝑗)):𝑋⟶ℝ)
371	370, 147	ffvelrnd 6717	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ∈ ℝ)
372	371	rexrd 10537	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ∈ ℝ^*)
373	372	ad5ant135 1361	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ∈ ℝ^*)
374	187	adantl3r 746	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*)
375	148	3expa 1111	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ)
376	186	3expa 1111	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*)
377		icossre 12667	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ)
378	375, 376, 377	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ)
379	378	adantlr 711	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ)
380	379, 195	sseldd 3890	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
381	380	rexrd 10537	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ^*)
382	381	adantl3r 746	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ^*)
383	38	3adant3 1125	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → 𝑌 ∈ ℝ)
384	14	3adant3 1125	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → 𝑋 ∈ Fin)
385	97, 383, 384, 146, 147	hoidifhspval3 42463	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)))
386	385	ad5ant134 1360	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)))
387		iftrue 4387	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
388	387	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
389	386, 388	eqtrd 2831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
390	389	adantllr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
391		iftrue 4387	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑌 ≤ ((𝐶‘𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = ((𝐶‘𝑗)‘𝑘))
392	391	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = ((𝐶‘𝑗)‘𝑘))
393	197	adantl3r 746	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
394	393	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
395	392, 394	eqbrtrd 4984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘))
396		iffalse 4390	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = 𝑌)
397	396	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = 𝑌)
398		simpl1 1184	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))))
399		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑌 ≤ (𝑓‘𝑘))
400		fveq2 6538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 = 𝐾 → (𝑓‘𝑘) = (𝑓‘𝐾))
401	400	breq2d 4974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 = 𝐾 → (𝑌 ≤ (𝑓‘𝑘) ↔ 𝑌 ≤ (𝑓‘𝐾)))
402	401	notbid 319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝐾 → (¬ 𝑌 ≤ (𝑓‘𝑘) ↔ ¬ 𝑌 ≤ (𝑓‘𝐾)))
403	402	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (¬ 𝑌 ≤ (𝑓‘𝑘) ↔ ¬ 𝑌 ≤ (𝑓‘𝐾)))
404	399, 403	mpbid 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑌 ≤ (𝑓‘𝐾))
405	404	3ad2antl3 1180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑌 ≤ (𝑓‘𝐾))
406	400	eqcomd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 = 𝐾 → (𝑓‘𝐾) = (𝑓‘𝑘))
407	406	3ad2ant3 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝐾) = (𝑓‘𝑘))
408	366	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
409		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝜑 ∧ 𝑗 ∈ ℕ))
410	409	ad4ant13 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝜑 ∧ 𝑗 ∈ ℕ))
411		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
412	251	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑘 ∈ 𝑋)
413	410, 411, 412, 380	syl21anc 834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓‘𝑘) ∈ ℝ)
414	413	rexlimdva2 3250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓‘𝑘) ∈ ℝ))
415	414	adantlr 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓‘𝑘) ∈ ℝ))
416	408, 415	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
417	416	3adant3 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ ℝ)
418	407, 417	eqeltrd 2883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝐾) ∈ ℝ)
419	418	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝑓‘𝐾) ∈ ℝ)
420	398, 363, 37	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → 𝑌 ∈ ℝ)
421	419, 420	ltnled 10634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ((𝑓‘𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝑓‘𝐾)))
422	405, 421	mpbird 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝑓‘𝐾) < 𝑌)
423	367, 366	r19.29a 3252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 Fn 𝑋)
424	423	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) → 𝑓 Fn 𝑋)
425	276	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → -∞ ∈ ℝ^*)
426	278	ad4antr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ∈ ℝ^*)
427	416	ad4ant13 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ ℝ)
428	427	mnfltd 12369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → -∞ < (𝑓‘𝑘))
429	400	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) = (𝑓‘𝐾))
430		simpl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝐾) < 𝑌)
431	429, 430	eqbrtrd 4984	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌)
432	431	ad4ant24 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌)
433	425, 426, 427, 428, 432	eliood 41334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ (-∞(,)𝑌))
434	155	eqcomd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 = 𝐾 → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
435	434	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
436	433, 435	eleqtrd 2885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
437	416	ad4ant13 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ ℝ)
438	159	eqcomd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ 𝑘 = 𝐾 → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
439	438	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
440	437, 439	eleqtrd 2885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
441	436, 440	pm2.61dan 809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
442	441	ralrimiva 3149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
443	424, 442	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
444	398, 422, 443	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
445	444, 172	sylibr 235	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
446	166	eqcomd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌))
447	446	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌))
448	447	3ad2antl1 1178	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌))
449	445, 448	eleqtrd 2885	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
450		eldifn 4025	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
451	450	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
452	451	3ad2ant1 1126	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
453	452	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
454	449, 453	condan 814	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → 𝑌 ≤ (𝑓‘𝑘))
455	454	ad5ant145 1362	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ≤ (𝑓‘𝑘))
456	455	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → 𝑌 ≤ (𝑓‘𝑘))
457	397, 456	eqbrtrd 4984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘))
458	395, 457	pm2.61dan 809	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘))
459	390, 458	eqbrtrd 4984	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘))
460	385	ad5ant124 1358	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)))
461		iffalse 4390	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = ((𝐶‘𝑗)‘𝑘))
462	461	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = ((𝐶‘𝑗)‘𝑘))
463	460, 462	eqtrd 2831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = ((𝐶‘𝑗)‘𝑘))
464	197	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
465	463, 464	eqbrtrd 4984	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘))
466	465	adantl4r 751	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘))
467	459, 466	pm2.61dan 809	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘))
468	200	adantl3r 746	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
469	373, 374, 382, 467, 468	elicod 12637	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
470	469	ex 413	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑘 ∈ 𝑋 → (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
471	369, 470	ralrimi 3183	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
472	367, 471	jca 512	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
473	171	elixp 8317	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
474	472, 473	sylibr 235	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
475		eqidd 2796	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))))
476		2fveq3 6543	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 = 𝑗 → ((𝑆‘𝑌)‘(𝐶‘𝑙)) = ((𝑆‘𝑌)‘(𝐶‘𝑗)))
477	476	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑆‘𝑌)‘(𝐶‘𝑙)) = ((𝑆‘𝑌)‘(𝐶‘𝑗)))
478		fvexd 6553	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((𝑆‘𝑌)‘(𝐶‘𝑗)) ∈ V)
479	475, 477, 340, 478	fvmptd 6641	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗) = ((𝑆‘𝑌)‘(𝐶‘𝑗)))
480	479	fveq1d 6540	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘) = (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘))
481	480	oveq1d 7031	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
482	481	ixpeq2dv 8326	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
483	482	ad2antlr 723	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
484	483	eleq2d 2868	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
485	474, 484	mpbird 258	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
486	485	ex 413	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
487	486	reximdva 3237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
488	366, 487	mpd 15	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
489		eliun 4829	. . . . . . . . 9 ⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
490	488, 489	sylibr 235	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
491	490	ralrimiva 3149	. . . . . . 7 ⊢ (𝜑 → ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
492		dfss3 3878	. . . . . . 7 ⊢ ((𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
493	491, 492	sylibr 235	. . . . . 6 ⊢ (𝜑 → (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
494	13, 362, 19, 493, 12	ovnlecvr2 42454	. . . . 5 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
495	479	oveq1d 7031	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))
496	495	mpteq2ia 5051	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))
497	496	fveq2i 6541	. . . . . 6 ⊢ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))
498	497	a1i 11	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))
499	494, 498	breqtrd 4988	. . . 4 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))
500	1, 2, 96, 108, 353, 499	leadd12dd 41144	. . 3 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) + (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
501	14, 105, 38, 18, 22, 12, 36, 97	hspmbllem1 42470	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))
502	501	mpteq2dva 5055	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))
503	502	fveq2d 6542	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
504	8, 10, 41, 104	sge0xadd 42279	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) = ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) +_𝑒 (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
505	96, 108	rexaddd 12477	. . . 4 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) +_𝑒 (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) = ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) + (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
506	503, 504, 505	3eqtrrd 2836	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) + (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
507	500, 506	breqtrd 4988	. 2 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
508	3, 35, 7, 507, 34	letrd 10644	1 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1080 = wceq 1522 ∈ wcel 2081 ≠ wne 2984 ∀wral 3105 ∃wrex 3106 Vcvv 3437 ∖ cdif 3856 ∪ cun 3857 ∩ cin 3858 ⊆ wss 3859 ∅c0 4211 ifcif 4381 {csn 4472 ∪ ciun 4825 class class class wbr 4962 ↦ cmpt 5041 Fn wfn 6220 ⟶wf 6221 ‘cfv 6225 (class class class)co 7016 ∈ cmpo 7018 ↑_𝑚 cmap 8256 Xcixp 8310 Fincfn 8357 ℝcr 10382 0cc0 10383 + caddc 10386 +∞cpnf 10518 -∞cmnf 10519 ℝ^*cxr 10520 < clt 10521 ≤ cle 10522 ℕcn 11486 ℝ⁺crp 12239 +_𝑒 cxad 12355 (,)cioo 12588 [,)cico 12590 [,]cicc 12591 ∏cprod 15092 volcvol 23747 Σ^{^}csumge0 42206 voln*covoln 42380

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5081 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 ax-inf2 8950 ax-cnex 10439 ax-resscn 10440 ax-1cn 10441 ax-icn 10442 ax-addcl 10443 ax-addrcl 10444 ax-mulcl 10445 ax-mulrcl 10446 ax-mulcom 10447 ax-addass 10448 ax-mulass 10449 ax-distr 10450 ax-i2m1 10451 ax-1ne0 10452 ax-1rid 10453 ax-rnegex 10454 ax-rrecex 10455 ax-cnre 10456 ax-pre-lttri 10457 ax-pre-lttrn 10458 ax-pre-ltadd 10459 ax-pre-mulgt0 10460 ax-pre-sup 10461

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-fal 1535 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-reu 3112 df-rmo 3113 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-pss 3876 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-tp 4477 df-op 4479 df-uni 4746 df-int 4783 df-iun 4827 df-br 4963 df-opab 5025 df-mpt 5042 df-tr 5064 df-id 5348 df-eprel 5353 df-po 5362 df-so 5363 df-fr 5402 df-se 5403 df-we 5404 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-pred 6023 df-ord 6069 df-on 6070 df-lim 6071 df-suc 6072 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-isom 6234 df-riota 6977 df-ov 7019 df-oprab 7020 df-mpo 7021 df-of 7267 df-om 7437 df-1st 7545 df-2nd 7546 df-wrecs 7798 df-recs 7860 df-rdg 7898 df-1o 7953 df-2o 7954 df-oadd 7957 df-er 8139 df-map 8258 df-pm 8259 df-ixp 8311 df-en 8358 df-dom 8359 df-sdom 8360 df-fin 8361 df-fi 8721 df-sup 8752 df-inf 8753 df-oi 8820 df-dju 9176 df-card 9214 df-pnf 10523 df-mnf 10524 df-xr 10525 df-ltxr 10526 df-le 10527 df-sub 10719 df-neg 10720 df-div 11146 df-nn 11487 df-2 11548 df-3 11549 df-n0 11746 df-z 11830 df-uz 12094 df-q 12198 df-rp 12240 df-xneg 12357 df-xadd 12358 df-xmul 12359 df-ioo 12592 df-ico 12594 df-icc 12595 df-fz 12743 df-fzo 12884 df-fl 13012 df-seq 13220 df-exp 13280 df-hash 13541 df-cj 14292 df-re 14293 df-im 14294 df-sqrt 14428 df-abs 14429 df-clim 14679 df-rlim 14680 df-sum 14877 df-prod 15093 df-rest 16525 df-topgen 16546 df-psmet 20219 df-xmet 20220 df-met 20221 df-bl 20222 df-mopn 20223 df-top 21186 df-topon 21203 df-bases 21238 df-cmp 21679 df-ovol 23748 df-vol 23749 df-sumge0 42207 df-ovoln 42381

This theorem is referenced by: hspmbllem3 42472

W3C validator