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 47581

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 11319	. 2 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ∈ ℝ)
4		hspmbllem2.r	. . . 4 ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ)
5		hspmbllem2.e	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
6	5	rpred 13145	. . . 4 ⊢ (𝜑 → 𝐸 ∈ ℝ)
7	4, 6	readdcld 11319	. . 3 ⊢ (𝜑 → (((voln*‘𝑋)‘𝐴) + 𝐸) ∈ ℝ)
8		nfv 1947	. . . 4 ⊢ Ⅎ𝑗𝜑
9		nnex 12322	. . . . 5 ⊢ ℕ ∈ V
10	9	a1i 11	. . . 4 ⊢ (𝜑 → ℕ ∈ V)
11		icossicc 13548	. . . . 5 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
12		hspmbllem2.l	. . . . . 6 ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
13		hspmbllem2.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ Fin)
14	13	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin)
15		hspmbllem2.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑_m 𝑋))
16	15	ffvelcdmda 7076	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑_m 𝑋))
17		elmapi 8853	. . . . . . 7 ⊢ ((𝐶‘𝑗) ∈ (ℝ ↑_m 𝑋) → (𝐶‘𝑗):𝑋⟶ℝ)
18	16, 17	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑋⟶ℝ)
19		hspmbllem2.d	. . . . . . . 8 ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑_m 𝑋))
20	19	ffvelcdmda 7076	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑_m 𝑋))
21		elmapi 8853	. . . . . . 7 ⊢ ((𝐷‘𝑗) ∈ (ℝ ↑_m 𝑋) → (𝐷‘𝑗):𝑋⟶ℝ)
22	20, 21	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ)
23	12, 14, 18, 22	hoidmvcl 47536	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞))
24	11, 23	sselid 3929	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,]+∞))
25	8, 10, 24	sge0clmpt 47379	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ (0[,]+∞))
26		hspmbllem2.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
27		ne0i 4287	. . . . . . . . 9 ⊢ (𝐾 ∈ 𝑋 → 𝑋 ≠ ∅)
28	26, 27	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ≠ ∅)
29	28	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
30	12, 14, 29, 18, 22	hoidmvn0val 47538	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
31	30	mpteq2dva 5198	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))))
32	31	fveq2d 6881	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))))
33		hspmbllem2.g	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
34	32, 33	eqbrtrd 5127	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
35	7, 25, 34	ge0lere 46488	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ ℝ)
36		hspmbllem2.t	. . . . . . . . 9 ⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
37		hspmbllem2.y	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ ℝ)
38	37	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑌 ∈ ℝ)
39	36, 38, 14, 22	hsphoif 47530	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑗)):𝑋⟶ℝ)
40	12, 14, 18, 39	hoidmvcl 47536	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ∈ (0[,)+∞))
41	11, 40	sselid 3929	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ∈ (0[,]+∞))
42	8, 10, 41	sge0clmpt 47379	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ∈ (0[,]+∞))
43		oveq2 7420	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (ℝ ↑_m 𝑥) = (ℝ ↑_m 𝑦))
44		eqeq1 2765	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
45		prodeq1 16056	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))
46	44, 45	ifbieq2d 4509	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))
47	43, 43, 46	mpoeq123dv 7487	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑎 ∈ (ℝ ↑_m 𝑦), 𝑏 ∈ (ℝ ↑_m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
48	47	cbvmptv 5209	. . . . . . . . 9 ⊢ (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑦), 𝑏 ∈ (ℝ ↑_m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
49	12, 48	eqtri 2784	. . . . . . . 8 ⊢ 𝐿 = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑦), 𝑏 ∈ (ℝ ↑_m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
50		diffi 9174	. . . . . . . . . . 11 ⊢ (𝑋 ∈ Fin → (𝑋 ∖ {𝐾}) ∈ Fin)
51	13, 50	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
52		snfi 9055	. . . . . . . . . . 11 ⊢ {𝐾} ∈ Fin
53	52	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {𝐾} ∈ Fin)
54		unfi 9170	. . . . . . . . . 10 ⊢ (((𝑋 ∖ {𝐾}) ∈ Fin ∧ {𝐾} ∈ Fin) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
55	51, 53, 54	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
56	55	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
57		snidg 4621	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ 𝑋 → 𝐾 ∈ {𝐾})
58	26, 57	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ {𝐾})
59		elun2 4129	. . . . . . . . . . 11 ⊢ (𝐾 ∈ {𝐾} → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
60	58, 59	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
61		neldifsnd 4756	. . . . . . . . . 10 ⊢ (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
62	60, 61	eldifd 3910	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
63	62	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
64		eqid 2761	. . . . . . . 8 ⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ((𝑋 ∖ {𝐾}) ∪ {𝐾})
65		eqid 2761	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
66		uncom 4105	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
67	66	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
68	26	snssd 4747	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐾} ⊆ 𝑋)
69		undif 4438	. . . . . . . . . . . . 13 ⊢ ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
70	68, 69	sylib 221	. . . . . . . . . . . 12 ⊢ (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
71	67, 70	eqtrd 2796	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
72	71	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
73	72	feq2d 6685	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐶‘𝑗):𝑋⟶ℝ))
74	18, 73	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
75	72	feq2d 6685	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐷‘𝑗):𝑋⟶ℝ))
76	22, 75	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
77	49, 56, 63, 64, 38, 65, 74, 76	hsphoidmvle 47540	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗)))
78	71	fveq2d 6881	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿‘𝑋))
79		eqidd 2762	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶‘𝑗) = (𝐶‘𝑗))
80	36	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))))
81	71	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (ℝ ↑_m 𝑋))
82	71	mpteq1d 5195	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))
83	81, 82	mpteq12dv 5192	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
84	83	eqcomd 2767	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
85	84	mpteq2dv 5199	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))))
86	80, 85	eqtr2d 2797	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = 𝑇)
87	86	fveq1d 6879	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌) = (𝑇‘𝑌))
88	87	fveq1d 6879	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗)) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
89	78, 79, 88	oveq123d 7433	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
90	89	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
91	78	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿‘𝑋))
92	91	oveqd 7429	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗)) = ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
93	90, 92	breq12d 5116	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗)) ↔ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))
94	77, 93	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
95	8, 10, 41, 24, 94	sge0lempt 47364	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
96	35, 42, 95	ge0lere 46488	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ∈ ℝ)
97		hspmbllem2.s	. . . . . . . . . 10 ⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ)))))
98	97, 38, 14, 18	hoidifhspf 47572	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑆‘𝑌)‘(𝐶‘𝑗)):𝑋⟶ℝ)
99	12, 14, 98, 22	hoidmvcl 47536	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞))
100	99	fmpttd 7107	. . . . . . 7 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,)+∞))
101	11	a1i 11	. . . . . . 7 ⊢ (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
102	100, 101	fssd 6719	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
103	10, 102	sge0cl 47335	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ (0[,]+∞))
104	11, 99	sselid 3929	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,]+∞))
105	26	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐾 ∈ 𝑋)
106	12, 14, 18, 22, 105, 97, 38	hoidifhspdmvle 47574	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
107	8, 10, 104, 24, 106	sge0lempt 47364	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
108	35, 103, 107	ge0lere 46488	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ ℝ)
109	37	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → 𝑌 ∈ ℝ)
110	13	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → 𝑋 ∈ Fin)
111		eleq1w 2844	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑙 → (𝑗 ∈ ℕ ↔ 𝑙 ∈ ℕ))
112	111	anbi2d 642	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑙 → ((𝜑 ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ 𝑙 ∈ ℕ)))
113		fveq2 6877	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑙 → (𝐷‘𝑗) = (𝐷‘𝑙))
114	113	feq1d 6683	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑙 → ((𝐷‘𝑗):𝑋⟶ℝ ↔ (𝐷‘𝑙):𝑋⟶ℝ))
115	112, 114	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑗 = 𝑙 → (((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ) ↔ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐷‘𝑙):𝑋⟶ℝ)))
116	115, 22	chvarvv 2022	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐷‘𝑙):𝑋⟶ℝ)
117	36, 109, 110, 116	hsphoif 47530	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ)
118		reex 11272	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
119	118	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ∈ V)
120	119, 13	jca 521	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
121	120	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (ℝ ∈ V ∧ 𝑋 ∈ Fin))
122		elmapg 8843	. . . . . . . . 9 ⊢ ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑_m 𝑋) ↔ ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ))
123	121, 122	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑_m 𝑋) ↔ ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ))
124	117, 123	mpbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑_m 𝑋))
125	124	fmpttd 7107	. . . . . 6 ⊢ (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))):ℕ⟶(ℝ ↑_m 𝑋))
126		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝜑)
127		elinel1 4147	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ 𝐴)
128	127	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ 𝐴)
129		hspmbllem2.a	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
130	129	sselda 3931	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
131		eliun 4955	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
132	130, 131	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
133	126, 128, 132	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
134		simpll 779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝜑)
135		elinel2 4148	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
136	135	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
137	136	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
138		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
139		ixpfn 8915	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 Fn 𝑋)
140	139	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
141		nfv 1947	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ)
142		nfcv 2923	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘𝑓
143		nfixp1 8930	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))
144	142, 143	nfel 2937	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))
145	141, 144	nfan 1932	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
146	18	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (𝐶‘𝑗):𝑋⟶ℝ)
147		simp3 1156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
148	146, 147	ffvelcdmd 7077	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ)
149	148	rexrd 11340	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ^*)
150	149	ad5ant135 1394	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ^*)
151	39	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝑇‘𝑌)‘(𝐷‘𝑗)):𝑋⟶ℝ)
152	151, 147	ffvelcdmd 7077	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈ ℝ)
153	152	rexrd 11340	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈ ℝ^*)
154	153	ad5ant135 1394	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈ ℝ^*)
155		iftrue 4488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
156		ioossre 13519	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (-∞(,)𝑌) ⊆ ℝ
157	156	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝐾 → (-∞(,)𝑌) ⊆ ℝ)
158	155, 157	eqsstrd 3965	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
159		iffalse 4491	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = ℝ)
160		ssid 3953	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℝ ⊆ ℝ
161	160	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 = 𝐾 → ℝ ⊆ ℝ)
162	159, 161	eqsstrd 3965	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
163	158, 162	pm2.61i 184	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ
164		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
165		hspmbllem2.h	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
166	165, 13, 26, 37	hspval 47563	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐾(𝐻‘𝑋)𝑌) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
167	166	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → (𝐾(𝐻‘𝑋)𝑌) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
168	164, 167	eleqtrd 2863	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
169	168	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
170		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
171		vex 3455	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑓 ∈ V
172	171	elixp 8916	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
173	172	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
174	173	simprd 501	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
175	174	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
176		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
177		rspa 3252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
178	175, 176, 177	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
179	169, 170, 178	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
180	163, 179	sselid 3929	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
181	180	rexrd 11340	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ^*)
182	181	ad4ant14 765	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ^*)
183	149	ad4ant124 1192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ^*)
184	22	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (𝐷‘𝑗):𝑋⟶ℝ)
185	184, 147	ffvelcdmd 7077	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ)
186	185	rexrd 11340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*)
187	186	ad4ant124 1192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*)
188	171	elixp 8916	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
189	188	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
190	189	simprd 501	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
191	190	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
192		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
193		rspa 3252	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
194	191, 192, 193	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
195	194	adantll 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
196		icogelb 13508	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ^* ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ^* ∧ (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
197	183, 187, 195, 196	syl3anc 1398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
198	197	adantl3r 763	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
199		icoltub 46464	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ^* ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ^* ∧ (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
200	183, 187, 195, 199	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
201	200	adantl3r 763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
202	201	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
203		simpll 779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝜑)
204		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
205	203, 204	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝜑 ∧ 𝑗 ∈ ℕ))
206	205	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝜑 ∧ 𝑗 ∈ ℕ))
207		simp2 1155	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑘 = 𝐾)
208		simp3 1156	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) ≤ 𝑌)
209		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 = 𝐾 → ((𝐷‘𝑗)‘𝑘) = ((𝐷‘𝑗)‘𝐾))
210	209	breq1d 5113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝐾 → (((𝐷‘𝑗)‘𝑘) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌))
211	210	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝐾) ≤ 𝑌)
212	211	iftrued 4490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝐾))
213	209	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝐾 → ((𝐷‘𝑗)‘𝐾) = ((𝐷‘𝑗)‘𝑘))
214	213	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝐾) = ((𝐷‘𝑗)‘𝑘))
215	212, 214	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝑘))
216	215	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝑘))
217		breq2 5107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑌 → ((𝑐‘ℎ) ≤ 𝑦 ↔ (𝑐‘ℎ) ≤ 𝑌))
218		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑌 → 𝑦 = 𝑌)
219	217, 218	ifbieq2d 4509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = 𝑌 → if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦) = if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))
220	219	ifeq2d 4503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = 𝑌 → if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)) = if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))
221	220	mpteq2dv 5199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = 𝑌 → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))))
222	221	mpteq2dv 5199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = 𝑌 → (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))))
223		ovex 7445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (ℝ ↑_m 𝑋) ∈ V
224	223	mptex 7221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))) ∈ V
225	224	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))) ∈ V)
226	36, 222, 37, 225	fvmptd3 7009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝑇‘𝑌) = (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))))
227	226	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑌) = (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))))
228		fveq1 6876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = (𝐷‘𝑗) → (𝑐‘ℎ) = ((𝐷‘𝑗)‘ℎ))
229	228	breq1d 5113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = (𝐷‘𝑗) → ((𝑐‘ℎ) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘ℎ) ≤ 𝑌))
230	229, 228	ifbieq1d 4507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = (𝐷‘𝑗) → if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌) = if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))
231	228, 230	ifeq12d 4504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = (𝐷‘𝑗) → if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)) = if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))
232	231	mpteq2dv 5199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = (𝐷‘𝑗) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
233	232	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑐 = (𝐷‘𝑗)) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
234		mptexg 7219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑋 ∈ Fin → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) ∈ V)
235	13, 234	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) ∈ V)
236	235	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) ∈ V)
237	227, 233, 20, 236	fvmptd 6993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑗)) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
238	237	fveq1d 6879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘))
239	238	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘))
240		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝜑)
241		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝑘 = 𝐾)
242	240, 26	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝐾 ∈ 𝑋)
243	241, 242	eqeltrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝑘 ∈ 𝑋)
244		eqidd 2762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
245		eleq1w 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑘 → (ℎ ∈ (𝑋 ∖ {𝐾}) ↔ 𝑘 ∈ (𝑋 ∖ {𝐾})))
246		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑘 → ((𝐷‘𝑗)‘ℎ) = ((𝐷‘𝑗)‘𝑘))
247	246	breq1d 5113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (ℎ = 𝑘 → (((𝐷‘𝑗)‘ℎ) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌))
248	247, 246	ifbieq1d 4507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑘 → if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌) = if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌))
249	245, 246, 248	ifbieq12d 4511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ℎ = 𝑘 → if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
250	249	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ℎ = 𝑘) → if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
251		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
252		fvexd 6892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((𝐷‘𝑗)‘𝑘) ∈ V)
253	252, 37	ifexd 4531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌) ∈ V)
254	252, 253	ifexd 4531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V)
255	254	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V)
256	244, 250, 251, 255	fvmptd 6993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
257	240, 243, 256	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
258		eleq1 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝐾 → (𝑘 ∈ (𝑋 ∖ {𝐾}) ↔ 𝐾 ∈ (𝑋 ∖ {𝐾})))
259	210, 209	ifbieq1d 4507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝐾 → if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
260	258, 209, 259	ifbieq12d 4511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = 𝐾 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
261	260	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
262	257, 261	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
263	262	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
264		neldifsnd 4756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 = 𝐾 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
265	264	iffalsed 4493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝐾 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
266	265	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
267	239, 263, 266	3eqtrrd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
268	267	3expa 1136	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
269	268	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
270	216, 269	eqtr3d 2798	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
271	206, 207, 208, 270	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
272	271	ad5ant145 1396	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
273	202, 272	breqtrd 5131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
274		mnfxr 11347	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ -∞ ∈ ℝ^*
275	274	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → -∞ ∈ ℝ^*)
276	37	rexrd 11340	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑌 ∈ ℝ^*)
277	276	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → 𝑌 ∈ ℝ^*)
278	277	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → 𝑌 ∈ ℝ^*)
279	179	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
280	155	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
281	279, 280	eleqtrd 2863	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ (-∞(,)𝑌))
282		iooltub 46466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑌 ∈ ℝ^* ∧ (𝑓‘𝑘) ∈ (-∞(,)𝑌)) → (𝑓‘𝑘) < 𝑌)
283	275, 278, 281, 282	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌)
284	283	3adant1r 1196	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌)
285	284	ad4ant123 1191	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < 𝑌)
286		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌)
287	210	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝐾 → (¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌))
288	287	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌 ↔ ¬ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌))
289	286, 288	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ¬ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌)
290	289	iffalsed 4493	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = 𝑌)
291		eqidd 2762	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = 𝑌)
292	290, 291	eqtr2d 2797	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
293	292	adantll 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
294	268	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
295	294	adantl3r 763	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
296	295	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
297	293, 296	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
298	285, 297	breqtrd 5131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
299	298	adantl3r 763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
300	273, 299	pm2.61dan 825	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
301	201	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
302	237	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝑇‘𝑌)‘(𝐷‘𝑗)) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
303	249	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) ∧ ℎ = 𝑘) → if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
304	255	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V)
305	302, 303, 147, 304	fvmptd 6993	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
306	305	3expa 1136	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
307	306	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
308	307	ad4ant13 764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
309		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ 𝑋)
310		neqne 2964	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑘 = 𝐾 → 𝑘 ≠ 𝐾)
311		nelsn 4627	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ≠ 𝐾 → ¬ 𝑘 ∈ {𝐾})
312	310, 311	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ 𝑘 = 𝐾 → ¬ 𝑘 ∈ {𝐾})
313	312	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → ¬ 𝑘 ∈ {𝐾})
314	309, 313	eldifd 3910	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ (𝑋 ∖ {𝐾}))
315	314	iftrued 4490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = ((𝐷‘𝑗)‘𝑘))
316	315	adantll 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = ((𝐷‘𝑗)‘𝑘))
317	308, 316	eqtr2d 2797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
318	301, 317	breqtrd 5131	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
319	300, 318	pm2.61dan 825	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
320	150, 154, 182, 198, 319	elicod 13507	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
321	320	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑘 ∈ 𝑋 → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
322	145, 321	ralrimi 3261	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
323	140, 322	jca 521	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
324	171	elixp 8916	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
325	323, 324	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
326	325	ex 418	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) → (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
327	134, 137, 138, 326	syl21anc 851	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
328	327	reximdva 3176	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
329	133, 328	mpd 16	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
330		eliun 4955	. . . . . . . . . 10 ⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
331	329, 330	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
332	331	ralrimiva 3155	. . . . . . . 8 ⊢ (𝜑 → ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
333		dfss3 3920	. . . . . . . 8 ⊢ ((𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
334	332, 333	sylibr 237	. . . . . . 7 ⊢ (𝜑 → (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
335		eqidd 2762	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))))
336		2fveq3 6882	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑗 → ((𝑇‘𝑌)‘(𝐷‘𝑙)) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
337	336	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑇‘𝑌)‘(𝐷‘𝑙)) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
338		id 23	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
339		fvexd 6892	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → ((𝑇‘𝑌)‘(𝐷‘𝑗)) ∈ V)
340	335, 337, 338, 339	fvmptd 6993	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
341	340	fveq1d 6879	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
342	341	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
343	342	ixpeq2dv 8925	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
344	343	iuneq2i 4973	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
345	334, 344	sseqtrrdi 3972	. . . . . 6 ⊢ (𝜑 → (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)))
346	13, 15, 125, 345, 12	ovnlecvr2 47564	. . . . 5 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)))))
347	340	oveq2d 7428	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
348	347	mpteq2ia 5200	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
349	348	fveq2i 6880	. . . . . 6 ⊢ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗)))))
350	349	a1i 11	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))))
351	346, 350	breqtrd 5131	. . . 4 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))))
352	15	ffvelcdmda 7076	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐶‘𝑙) ∈ (ℝ ↑_m 𝑋))
353		elmapi 8853	. . . . . . . . . 10 ⊢ ((𝐶‘𝑙) ∈ (ℝ ↑_m 𝑋) → (𝐶‘𝑙):𝑋⟶ℝ)
354	352, 353	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐶‘𝑙):𝑋⟶ℝ)
355	97, 109, 110, 354	hoidifhspf 47572	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ)
356		elmapg 8843	. . . . . . . . . 10 ⊢ ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑_m 𝑋) ↔ ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ))
357	120, 356	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑_m 𝑋) ↔ ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ))
358	357	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑_m 𝑋) ↔ ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ))
359	355, 358	mpbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑆‘𝑌)‘(𝐶‘𝑙)) ∈ (ℝ ↑_m 𝑋))
360	359	fmpttd 7107	. . . . . 6 ⊢ (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))):ℕ⟶(ℝ ↑_m 𝑋))
361		simpl 488	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝜑)
362		eldifi 4078	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ 𝐴)
363	362	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ 𝐴)
364	361, 363, 132	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
365	139	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
366		nfv 1947	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ)
367	366, 144	nfan 1932	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
368	98	3adant3 1150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝑆‘𝑌)‘(𝐶‘𝑗)):𝑋⟶ℝ)
369	368, 147	ffvelcdmd 7077	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ∈ ℝ)
370	369	rexrd 11340	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ∈ ℝ^*)
371	370	ad5ant135 1394	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ∈ ℝ^*)
372	187	adantl3r 763	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*)
373	148	3expa 1136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ)
374	186	3expa 1136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*)
375		icossre 13540	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ)
376	373, 374, 375	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ)
377	376	adantlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ)
378	377, 195	sseldd 3932	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
379	378	rexrd 11340	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ^*)
380	379	adantl3r 763	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ^*)
381	38	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → 𝑌 ∈ ℝ)
382	14	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → 𝑋 ∈ Fin)
383	97, 381, 382, 146, 147	hoidifhspval3 47573	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)))
384	383	ad5ant134 1392	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)))
385		iftrue 4488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
386	385	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
387	384, 386	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
388	387	adantllr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
389		iftrue 4488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑌 ≤ ((𝐶‘𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = ((𝐶‘𝑗)‘𝑘))
390	389	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = ((𝐶‘𝑗)‘𝑘))
391	197	adantl3r 763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
392	391	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
393	390, 392	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘))
394		iffalse 4491	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = 𝑌)
395	394	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = 𝑌)
396		simpl1 1210	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))))
397		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑌 ≤ (𝑓‘𝑘))
398		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 = 𝐾 → (𝑓‘𝑘) = (𝑓‘𝐾))
399	398	breq2d 5115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 = 𝐾 → (𝑌 ≤ (𝑓‘𝑘) ↔ 𝑌 ≤ (𝑓‘𝐾)))
400	399	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝐾 → (¬ 𝑌 ≤ (𝑓‘𝑘) ↔ ¬ 𝑌 ≤ (𝑓‘𝐾)))
401	400	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (¬ 𝑌 ≤ (𝑓‘𝑘) ↔ ¬ 𝑌 ≤ (𝑓‘𝐾)))
402	397, 401	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑌 ≤ (𝑓‘𝐾))
403	402	3ad2antl3 1206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑌 ≤ (𝑓‘𝐾))
404	398	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 = 𝐾 → (𝑓‘𝐾) = (𝑓‘𝑘))
405	404	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝐾) = (𝑓‘𝑘))
406	364	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
407		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝜑 ∧ 𝑗 ∈ ℕ))
408	407	ad4ant13 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝜑 ∧ 𝑗 ∈ ℕ))
409		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
410	251	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑘 ∈ 𝑋)
411	408, 409, 410, 378	syl21anc 851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓‘𝑘) ∈ ℝ)
412	411	rexlimdva2 3166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓‘𝑘) ∈ ℝ))
413	412	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓‘𝑘) ∈ ℝ))
414	406, 413	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
415	414	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ ℝ)
416	405, 415	eqeltrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝐾) ∈ ℝ)
417	416	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝑓‘𝐾) ∈ ℝ)
418	396, 361, 37	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → 𝑌 ∈ ℝ)
419	417, 418	ltnled 11438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ((𝑓‘𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝑓‘𝐾)))
420	403, 419	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝑓‘𝐾) < 𝑌)
421	365, 364	r19.29a 3171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 Fn 𝑋)
422	421	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) → 𝑓 Fn 𝑋)
423	274	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → -∞ ∈ ℝ^*)
424	276	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ∈ ℝ^*)
425	414	ad4ant13 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ ℝ)
426	425	mnfltd 13234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → -∞ < (𝑓‘𝑘))
427	398	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) = (𝑓‘𝐾))
428		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝐾) < 𝑌)
429	427, 428	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌)
430	429	ad4ant24 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌)
431	423, 424, 425, 426, 430	eliood 46454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ (-∞(,)𝑌))
432	155	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 = 𝐾 → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
433	432	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
434	431, 433	eleqtrd 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
435	414	ad4ant13 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ ℝ)
436	159	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ 𝑘 = 𝐾 → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
437	436	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
438	435, 437	eleqtrd 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
439	434, 438	pm2.61dan 825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
440	439	ralrimiva 3155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
441	422, 440	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
442	396, 420, 441	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ)))
443	442, 172	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
444	166	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌))
445	444	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌))
446	445	3ad2antl1 1204	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌))
447	443, 446	eleqtrd 2863	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
448		eldifn 4079	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
449	448	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
450	449	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
451	450	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
452	447, 451	condan 830	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → 𝑌 ≤ (𝑓‘𝑘))
453	452	ad5ant145 1396	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → 𝑌 ≤ (𝑓‘𝑘))
454	453	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → 𝑌 ≤ (𝑓‘𝑘))
455	395, 454	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘))
456	393, 455	pm2.61dan 825	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘))
457	388, 456	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘))
458	383	ad5ant124 1388	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)))
459		iffalse 4491	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = ((𝐶‘𝑗)‘𝑘))
460	459	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = ((𝐶‘𝑗)‘𝑘))
461	458, 460	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = ((𝐶‘𝑗)‘𝑘))
462	197	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
463	461, 462	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘))
464	463	adantl4r 768	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘))
465	457, 464	pm2.61dan 825	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘))
466	200	adantl3r 763	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < ((𝐷‘𝑗)‘𝑘))
467	371, 372, 380, 465, 466	elicod 13507	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
468	467	ex 418	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑘 ∈ 𝑋 → (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
469	367, 468	ralrimi 3261	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
470	365, 469	jca 521	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
471	171	elixp 8916	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
472	470, 471	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
473		eqidd 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))))
474		2fveq3 6882	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 = 𝑗 → ((𝑆‘𝑌)‘(𝐶‘𝑙)) = ((𝑆‘𝑌)‘(𝐶‘𝑗)))
475	474	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑆‘𝑌)‘(𝐶‘𝑙)) = ((𝑆‘𝑌)‘(𝐶‘𝑗)))
476		fvexd 6892	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((𝑆‘𝑌)‘(𝐶‘𝑗)) ∈ V)
477	473, 475, 338, 476	fvmptd 6993	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗) = ((𝑆‘𝑌)‘(𝐶‘𝑗)))
478	477	fveq1d 6879	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘) = (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘))
479	478	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
480	479	ixpeq2dv 8925	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
481	480	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
482	481	eleq2d 2847	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
483	472, 482	mpbird 260	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
484	483	ex 418	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
485	484	reximdva 3176	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
486	364, 485	mpd 16	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
487		eliun 4955	. . . . . . . . 9 ⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
488	486, 487	sylibr 237	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
489	488	ralrimiva 3155	. . . . . . 7 ⊢ (𝜑 → ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
490		dfss3 3920	. . . . . . 7 ⊢ ((𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
491	489, 490	sylibr 237	. . . . . 6 ⊢ (𝜑 → (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
492	13, 360, 19, 491, 12	ovnlecvr2 47564	. . . . 5 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
493	477	oveq1d 7427	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))
494	493	mpteq2ia 5200	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))
495	494	fveq2i 6880	. . . . . 6 ⊢ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))
496	495	a1i 11	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))
497	492, 496	breqtrd 5131	. . . 4 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))
498	1, 2, 96, 108, 351, 497	le2addd 11916	. . 3 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) + (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
499	14, 105, 38, 18, 22, 12, 36, 97	hspmbllem1 47580	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))
500	499	mpteq2dva 5198	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))
501	500	fveq2d 6881	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
502	8, 10, 41, 104	sge0xadd 47389	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) = ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) +_𝑒 (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
503	96, 108	rexaddd 13345	. . . 4 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) +_𝑒 (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) = ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) + (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
504	501, 502, 503	3eqtrrd 2801	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) + (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
505	498, 504	breqtrd 5131	. 2 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
506	3, 35, 7, 505, 34	letrd 11448	1 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 Vcvv 3451 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 ifcif 4482 {csn 4584 ∪ ciun 4951 class class class wbr 5103 ↦ cmpt 5186 Fn wfn 6526 ⟶wf 6527 ‘cfv 6531 (class class class)co 7412 ∈ cmpo 7414 ↑_m cmap 8831 Xcixp 8909 Fincfn 8957 ℝcr 11180 0cc0 11181 + caddc 11184 +∞cpnf 11321 -∞cmnf 11322 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 ℕcn 12316 ℝ⁺crp 13101 +_𝑒 cxad 13220 (,)cioo 13457 [,)cico 13459 [,]cicc 13460 ∏cprod 16052 volcvol 25764 Σ^{^}csumge0 47316 voln*covoln 47490

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-inf2 9626 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-pre-sup 11259

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-2o 8461 df-er 8701 df-map 8833 df-pm 8834 df-ixp 8910 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-fi 9387 df-sup 9418 df-inf 9419 df-oi 9488 df-dju 9963 df-card 10001 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-2 12386 df-3 12387 df-n0 12588 df-z 12675 df-uz 12947 df-q 13057 df-rp 13102 df-xneg 13222 df-xadd 13223 df-xmul 13224 df-ioo 13461 df-ico 13463 df-icc 13464 df-fz 13621 df-fzo 13769 df-fl 13912 df-seq 14125 df-exp 14185 df-hash 14455 df-cj 15246 df-re 15247 df-im 15248 df-sqrt 15382 df-abs 15383 df-clim 15635 df-rlim 15636 df-sum 15834 df-prod 16053 df-rest 17573 df-topgen 17594 df-psmet 21650 df-xmet 21651 df-met 21652 df-bl 21653 df-mopn 21654 df-top 23192 df-topon 23209 df-bases 23244 df-cmp 23685 df-ovol 25765 df-vol 25766 df-sumge0 47317 df-ovoln 47491

This theorem is used by: hspmbllem3 47582

W3C validator