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 47382

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 11256	. 2 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ∈ ℝ)
4		hspmbllem2.r	. . . 4 ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ)
5		hspmbllem2.e	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
6	5	rpred 13078	. . . 4 ⊢ (𝜑 → 𝐸 ∈ ℝ)
7	4, 6	readdcld 11256	. . 3 ⊢ (𝜑 → (((voln*‘𝑋)‘𝐴) + 𝐸) ∈ ℝ)
8		nfv 1947	. . . 4 ⊢ Ⅎ𝑗𝜑
9		nnex 12257	. . . . 5 ⊢ ℕ ∈ V
10	9	a1i 11	. . . 4 ⊢ (𝜑 → ℕ ∈ V)
11		icossicc 13481	. . . . 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 7086	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑_m 𝑋))
17		elmapi 8855	. . . . . . 7 ⊢ ((𝐶‘𝑗) ∈ (ℝ ↑_m 𝑋) → (𝐶‘𝑗):𝑋⟶ℝ)
18	16, 17	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑋⟶ℝ)
19		hspmbllem2.d	. . . . . . . 8 ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑_m 𝑋))
20	19	ffvelcdmda 7086	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑_m 𝑋))
21		elmapi 8855	. . . . . . 7 ⊢ ((𝐷‘𝑗) ∈ (ℝ ↑_m 𝑋) → (𝐷‘𝑗):𝑋⟶ℝ)
22	20, 21	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ)
23	12, 14, 18, 22	hoidmvcl 47337	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞))
24	11, 23	sselid 3938	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,]+∞))
25	8, 10, 24	sge0clmpt 47180	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ (0[,]+∞))
26		hspmbllem2.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
27		ne0i 4297	. . . . . . . . 9 ⊢ (𝐾 ∈ 𝑋 → 𝑋 ≠ ∅)
28	26, 27	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ≠ ∅)
29	28	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ≠ ∅)
30	12, 14, 29, 18, 22	hoidmvn0val 47339	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
31	30	mpteq2dva 5209	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))))
32	31	fveq2d 6892	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))))
33		hspmbllem2.g	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
34	32, 33	eqbrtrd 5138	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸))
35	7, 25, 34	ge0lere 46289	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ ℝ)
36		hspmbllem2.t	. . . . . . . . 9 ⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
37		hspmbllem2.y	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ ℝ)
38	37	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑌 ∈ ℝ)
39	36, 38, 14, 22	hsphoif 47331	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑗)):𝑋⟶ℝ)
40	12, 14, 18, 39	hoidmvcl 47337	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ∈ (0[,)+∞))
41	11, 40	sselid 3938	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ∈ (0[,]+∞))
42	8, 10, 41	sge0clmpt 47180	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ∈ (0[,]+∞))
43		oveq2 7431	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (ℝ ↑_m 𝑥) = (ℝ ↑_m 𝑦))
44		eqeq1 2770	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
45		prodeq1 15987	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))) = ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))
46	44, 45	ifbieq2d 4519	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))) = if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))
47	43, 43, 46	mpoeq123dv 7498	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))) = (𝑎 ∈ (ℝ ↑_m 𝑦), 𝑏 ∈ (ℝ ↑_m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
48	47	cbvmptv 5220	. . . . . . . . 9 ⊢ (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑦), 𝑏 ∈ (ℝ ↑_m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
49	12, 48	eqtri 2789	. . . . . . . 8 ⊢ 𝐿 = (𝑦 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑦), 𝑏 ∈ (ℝ ↑_m 𝑦) ↦ if(𝑦 = ∅, 0, ∏𝑘 ∈ 𝑦 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
50		diffi 9169	. . . . . . . . . . 11 ⊢ (𝑋 ∈ Fin → (𝑋 ∖ {𝐾}) ∈ Fin)
51	13, 50	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
52		snfi 9050	. . . . . . . . . . 11 ⊢ {𝐾} ∈ Fin
53	52	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {𝐾} ∈ Fin)
54		unfi 9165	. . . . . . . . . 10 ⊢ (((𝑋 ∖ {𝐾}) ∈ Fin ∧ {𝐾} ∈ Fin) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
55	51, 53, 54	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
56	55	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∈ Fin)
57		snidg 4631	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ 𝑋 → 𝐾 ∈ {𝐾})
58	26, 57	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ {𝐾})
59		elun2 4139	. . . . . . . . . . 11 ⊢ (𝐾 ∈ {𝐾} → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
60	58, 59	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
61		neldifsnd 4766	. . . . . . . . . 10 ⊢ (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
62	60, 61	eldifd 3919	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
63	62	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐾 ∈ (((𝑋 ∖ {𝐾}) ∪ {𝐾}) ∖ (𝑋 ∖ {𝐾})))
64		eqid 2766	. . . . . . . 8 ⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ((𝑋 ∖ {𝐾}) ∪ {𝐾})
65		eqid 2766	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
66		uncom 4115	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
67	66	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
68	26	snssd 4757	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐾} ⊆ 𝑋)
69		undif 4448	. . . . . . . . . . . . 13 ⊢ ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
70	68, 69	sylib 221	. . . . . . . . . . . 12 ⊢ (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
71	67, 70	eqtrd 2801	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
72	71	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
73	72	feq2d 6696	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐶‘𝑗):𝑋⟶ℝ))
74	18, 73	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
75	72	feq2d 6696	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ ↔ (𝐷‘𝑗):𝑋⟶ℝ))
76	22, 75	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):((𝑋 ∖ {𝐾}) ∪ {𝐾})⟶ℝ)
77	49, 56, 63, 64, 38, 65, 74, 76	hsphoidmvle 47341	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗)))
78	71	fveq2d 6892	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿‘𝑋))
79		eqidd 2767	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶‘𝑗) = (𝐶‘𝑗))
80	36	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))))
81	71	oveq2d 7439	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (ℝ ↑_m 𝑋))
82	71	mpteq1d 5206	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))
83	81, 82	mpteq12dv 5203	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
84	83	eqcomd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
85	84	mpteq2dv 5210	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))))
86	80, 85	eqtr2d 2802	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) = 𝑇)
87	86	fveq1d 6890	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌) = (𝑇‘𝑌))
88	87	fveq1d 6890	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗)) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
89	78, 79, 88	oveq123d 7444	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
90	89	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
91	78	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾})) = (𝐿‘𝑋))
92	91	oveqd 7440	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗)) = ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
93	90, 92	breq12d 5127	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(((𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m ((𝑋 ∖ {𝐾}) ∪ {𝐾})) ↦ (ℎ ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘((𝑋 ∖ {𝐾}) ∪ {𝐾}))(𝐷‘𝑗)) ↔ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))
94	77, 93	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
95	8, 10, 41, 24, 94	sge0lempt 47165	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
96	35, 42, 95	ge0lere 46289	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) ∈ ℝ)
97		hspmbllem2.s	. . . . . . . . . 10 ⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ)))))
98	97, 38, 14, 18	hoidifhspf 47373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑆‘𝑌)‘(𝐶‘𝑗)):𝑋⟶ℝ)
99	12, 14, 98, 22	hoidmvcl 47337	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞))
100	99	fmpttd 7117	. . . . . . 7 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,)+∞))
101	11	a1i 11	. . . . . . 7 ⊢ (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
102	100, 101	fssd 6730	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
103	10, 102	sge0cl 47136	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ (0[,]+∞))
104	11, 99	sselid 3938	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,]+∞))
105	26	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐾 ∈ 𝑋)
106	12, 14, 18, 22, 105, 97, 38	hoidifhspdmvle 47375	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)) ≤ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))
107	8, 10, 104, 24, 106	sge0lempt 47165	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
108	35, 103, 107	ge0lere 46289	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ ℝ)
109	37	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → 𝑌 ∈ ℝ)
110	13	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → 𝑋 ∈ Fin)
111		eleq1w 2849	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑙 → (𝑗 ∈ ℕ ↔ 𝑙 ∈ ℕ))
112	111	anbi2d 642	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑙 → ((𝜑 ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ 𝑙 ∈ ℕ)))
113		fveq2 6888	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑙 → (𝐷‘𝑗) = (𝐷‘𝑙))
114	113	feq1d 6694	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑙 → ((𝐷‘𝑗):𝑋⟶ℝ ↔ (𝐷‘𝑙):𝑋⟶ℝ))
115	112, 114	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑗 = 𝑙 → (((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ) ↔ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐷‘𝑙):𝑋⟶ℝ)))
116	115, 22	chvarvv 2022	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐷‘𝑙):𝑋⟶ℝ)
117	36, 109, 110, 116	hsphoif 47331	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ)
118		reex 11209	. . . . . . . . . . . 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 8845	. . . . . . . . 9 ⊢ ((ℝ ∈ V ∧ 𝑋 ∈ Fin) → (((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑_m 𝑋) ↔ ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ))
123	121, 122	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑_m 𝑋) ↔ ((𝑇‘𝑌)‘(𝐷‘𝑙)):𝑋⟶ℝ))
124	117, 123	mpbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑙)) ∈ (ℝ ↑_m 𝑋))
125	124	fmpttd 7117	. . . . . 6 ⊢ (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))):ℕ⟶(ℝ ↑_m 𝑋))
126		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝜑)
127		elinel1 4157	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ 𝐴)
128	127	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ 𝐴)
129		hspmbllem2.a	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
130	129	sselda 3940	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
131		eliun 4965	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
132	130, 131	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
133	126, 128, 132	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
134		simpll 779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝜑)
135		elinel2 4158	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
136	135	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
137	136	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
138		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
139		ixpfn 8910	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 Fn 𝑋)
140	139	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 Fn 𝑋)
141		nfv 1947	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ)
142		nfcv 2928	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘𝑓
143		nfixp1 8925	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))
144	142, 143	nfel 2942	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))
145	141, 144	nfan 1932	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
146	18	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (𝐶‘𝑗):𝑋⟶ℝ)
147		simp3 1156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
148	146, 147	ffvelcdmd 7087	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ)
149	148	rexrd 11277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ^*)
150	149	ad5ant135 1394	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ^*)
151	39	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝑇‘𝑌)‘(𝐷‘𝑗)):𝑋⟶ℝ)
152	151, 147	ffvelcdmd 7087	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈ ℝ)
153	152	rexrd 11277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈ ℝ^*)
154	153	ad5ant135 1394	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘) ∈ ℝ^*)
155		iftrue 4498	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (-∞(,)𝑌))
156		ioossre 13452	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (-∞(,)𝑌) ⊆ ℝ
157	156	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝐾 → (-∞(,)𝑌) ⊆ ℝ)
158	155, 157	eqsstrd 3974	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) ⊆ ℝ)
159		iffalse 4501	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 = 𝐾 → if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = ℝ)
160		ssid 3962	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℝ ⊆ ℝ
161	160	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 = 𝐾 → ℝ ⊆ ℝ)
162	159, 161	eqsstrd 3974	. . . . . . . . . . . . . . . . . . . . . . 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 47364	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐾(𝐻‘𝑋)𝑌) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
167	166	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → (𝐾(𝐻‘𝑋)𝑌) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
168	164, 167	eleqtrd 2868	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
169	168	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
170		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
171		vex 3462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑓 ∈ V
172	171	elixp 8911	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3257	. . . . . . . . . . . . . . . . . . . . . . . 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 3938	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
181	180	rexrd 11277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ^*)
182	181	ad4ant14 765	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ^*)
183	149	ad4ant124 1192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ^*)
184	22	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (𝐷‘𝑗):𝑋⟶ℝ)
185	184, 147	ffvelcdmd 7087	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ)
186	185	rexrd 11277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*)
187	186	ad4ant124 1192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*)
188	171	elixp 8911	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3257	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
194	191, 192, 193	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
195	194	adantll 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
196		icogelb 13441	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ^* ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ^* ∧ (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
197	183, 187, 195, 196	syl3anc 1398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
198	197	adantl3r 763	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
199		icoltub 46265	. . . . . . . . . . . . . . . . . . . . . . . . 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 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 = 𝐾 → ((𝐷‘𝑗)‘𝑘) = ((𝐷‘𝑗)‘𝐾))
210	209	breq1d 5124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝐾 → (((𝐷‘𝑗)‘𝑘) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘𝐾) ≤ 𝑌))
211	210	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝐾) ≤ 𝑌)
212	211	iftrued 4500	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝐾))
213	209	eqcomd 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝐾 → ((𝐷‘𝑗)‘𝐾) = ((𝐷‘𝑗)‘𝑘))
214	213	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝐾) = ((𝐷‘𝑗)‘𝑘))
215	212, 214	eqtrd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝑘))
216	215	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = ((𝐷‘𝑗)‘𝑘))
217		breq2 5118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑌 → ((𝑐‘ℎ) ≤ 𝑦 ↔ (𝑐‘ℎ) ≤ 𝑌))
218		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = 𝑌 → 𝑦 = 𝑌)
219	217, 218	ifbieq2d 4519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = 𝑌 → if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦) = if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))
220	219	ifeq2d 4513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = 𝑌 → if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)) = if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))
221	220	mpteq2dv 5210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = 𝑌 → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))))
222	221	mpteq2dv 5210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = 𝑌 → (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))) = (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))))
223		ovex 7456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (ℝ ↑_m 𝑋) ∈ V
224	223	mptex 7228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))) ∈ V
225	224	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))) ∈ V)
226	36, 222, 37, 225	fvmptd3 7020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝑇‘𝑌) = (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))))
227	226	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑌) = (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)))))
228		fveq1 6887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = (𝐷‘𝑗) → (𝑐‘ℎ) = ((𝐷‘𝑗)‘ℎ))
229	228	breq1d 5124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = (𝐷‘𝑗) → ((𝑐‘ℎ) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘ℎ) ≤ 𝑌))
230	229, 228	ifbieq1d 4517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 = (𝐷‘𝑗) → if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌) = if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))
231	228, 230	ifeq12d 4514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = (𝐷‘𝑗) → if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌)) = if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))
232	231	mpteq2dv 5210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = (𝐷‘𝑗) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
233	232	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑐 = (𝐷‘𝑗)) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑌, (𝑐‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
234		mptexg 7226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑇‘𝑌)‘(𝐷‘𝑗)) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
238	237	fveq1d 6890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → 𝑘 ∈ 𝑋)
244		eqidd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))) = (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌))))
245		eleq1w 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑘 → (ℎ ∈ (𝑋 ∖ {𝐾}) ↔ 𝑘 ∈ (𝑋 ∖ {𝐾})))
246		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑘 → ((𝐷‘𝑗)‘ℎ) = ((𝐷‘𝑗)‘𝑘))
247	246	breq1d 5124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (ℎ = 𝑘 → (((𝐷‘𝑗)‘ℎ) ≤ 𝑌 ↔ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌))
248	247, 246	ifbieq1d 4517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑘 → if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌) = if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌))
249	245, 246, 248	ifbieq12d 4521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ℎ = 𝑘 → if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
250	249	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ℎ = 𝑘) → if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
251		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
252		fvexd 6903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((𝐷‘𝑗)‘𝑘) ∈ V)
253	252, 37	ifexd 4541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌) ∈ V)
254	252, 253	ifexd 4541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V)
255	254	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) ∈ V)
256	244, 250, 251, 255	fvmptd 7004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
257	240, 243, 256	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)))
258		eleq1 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝐾 → (𝑘 ∈ (𝑋 ∖ {𝐾}) ↔ 𝐾 ∈ (𝑋 ∖ {𝐾})))
259	210, 209	ifbieq1d 4517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝐾 → if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
260	258, 209, 259	ifbieq12d 4521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = 𝐾 → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
261	260	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
262	257, 261	eqtrd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
263	262	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → ((ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘ℎ), if(((𝐷‘𝑗)‘ℎ) ≤ 𝑌, ((𝐷‘𝑗)‘ℎ), 𝑌)))‘𝑘) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)))
264		neldifsnd 4766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 = 𝐾 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
265	264	iffalsed 4503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝐾 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
266	265	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(𝐾 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝐾), if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌)) = if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌))
267	239, 263, 266	3eqtrrd 2806	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
268	267	3expa 1136	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
269	268	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
270	216, 269	eqtr3d 2803	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
271	206, 207, 208, 270	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 = 𝐾 ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
272	271	ad5ant145 1396	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
273	202, 272	breqtrd 5142	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
274		mnfxr 11284	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ -∞ ∈ ℝ^*
275	274	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → -∞ ∈ ℝ^*)
276	37	rexrd 11277	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2868	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ (-∞(,)𝑌))
282		iooltub 46267	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4503	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → if(((𝐷‘𝑗)‘𝐾) ≤ 𝑌, ((𝐷‘𝑗)‘𝐾), 𝑌) = 𝑌)
291		eqidd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 = 𝐾 ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = 𝑌)
292	290, 291	eqtr2d 2802	. . . . . . . . . . . . . . . . . . . . . . . . 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 2801	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ ((𝐷‘𝑗)‘𝑘) ≤ 𝑌) → 𝑌 = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
298	285, 297	breqtrd 5142	. . . . . . . . . . . . . . . . . . . . . 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 7004	. . . . . . . . . . . . . . . . . . . . . . . . 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 2969	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑘 = 𝐾 → 𝑘 ≠ 𝐾)
311		nelsn 4637	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ≠ 𝐾 → ¬ 𝑘 ∈ {𝐾})
312	310, 311	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ 𝑘 = 𝐾 → ¬ 𝑘 ∈ {𝐾})
313	312	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → ¬ 𝑘 ∈ {𝐾})
314	309, 313	eldifd 3919	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → 𝑘 ∈ (𝑋 ∖ {𝐾}))
315	314	iftrued 4500	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ 𝑋 ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = ((𝐷‘𝑗)‘𝑘))
316	315	adantll 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑌, ((𝐷‘𝑗)‘𝑘), 𝑌)) = ((𝐷‘𝑗)‘𝑘))
317	308, 316	eqtr2d 2802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐷‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
318	301, 317	breqtrd 5142	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
319	300, 318	pm2.61dan 825	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
320	150, 154, 182, 198, 319	elicod 13440	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
321	320	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑘 ∈ 𝑋 → (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
322	145, 321	ralrimi 3266	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
323	140, 322	jca 521	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌)) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
324	171	elixp 8911	. . . . . . . . . . . . . . 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 3181	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))))
329	133, 328	mpd 16	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
330		eliun 4965	. . . . . . . . . 10 ⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
331	329, 330	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
332	331	ralrimiva 3160	. . . . . . . 8 ⊢ (𝜑 → ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
333		dfss3 3929	. . . . . . . 8 ⊢ ((𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
334	332, 333	sylibr 237	. . . . . . 7 ⊢ (𝜑 → (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
335		eqidd 2767	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙))))
336		2fveq3 6893	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑗 → ((𝑇‘𝑌)‘(𝐷‘𝑙)) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
337	336	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑇‘𝑌)‘(𝐷‘𝑙)) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
338		id 23	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
339		fvexd 6903	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → ((𝑇‘𝑌)‘(𝐷‘𝑗)) ∈ V)
340	335, 337, 338, 339	fvmptd 7004	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗) = ((𝑇‘𝑌)‘(𝐷‘𝑗)))
341	340	fveq1d 6890	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘) = (((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
342	341	oveq2d 7439	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
343	342	ixpeq2dv 8920	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘)))
344	343	iuneq2i 4983	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑇‘𝑌)‘(𝐷‘𝑗))‘𝑘))
345	334, 344	sseqtrrdi 3981	. . . . . 6 ⊢ (𝜑 → (𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)(((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)‘𝑘)))
346	13, 15, 125, 345, 12	ovnlecvr2 47365	. . . . 5 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)))))
347	340	oveq2d 7439	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)) = ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
348	347	mpteq2ia 5211	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))
349	348	fveq2i 6891	. . . . . 6 ⊢ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗)))))
350	349	a1i 11	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑙 ∈ ℕ ↦ ((𝑇‘𝑌)‘(𝐷‘𝑙)))‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))))
351	346, 350	breqtrd 5142	. . . 4 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))))
352	15	ffvelcdmda 7086	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐶‘𝑙) ∈ (ℝ ↑_m 𝑋))
353		elmapi 8855	. . . . . . . . . 10 ⊢ ((𝐶‘𝑙) ∈ (ℝ ↑_m 𝑋) → (𝐶‘𝑙):𝑋⟶ℝ)
354	352, 353	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐶‘𝑙):𝑋⟶ℝ)
355	97, 109, 110, 354	hoidifhspf 47373	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑆‘𝑌)‘(𝐶‘𝑙)):𝑋⟶ℝ)
356		elmapg 8845	. . . . . . . . . 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 7117	. . . . . 6 ⊢ (𝜑 → (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))):ℕ⟶(ℝ ↑_m 𝑋))
361		simpl 488	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝜑)
362		eldifi 4088	. . . . . . . . . . . 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 7087	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ∈ ℝ)
370	369	rexrd 11277	. . . . . . . . . . . . . . . . . . 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 13473	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ^*) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ)
376	373, 374, 375	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ)
377	376	adantlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ)
378	377, 195	sseldd 3941	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
379	378	rexrd 11277	. . . . . . . . . . . . . . . . . . 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 47374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)))
384	383	ad5ant134 1392	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)))
385		iftrue 4498	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
386	385	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
387	384, 386	eqtrd 2801	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
388	387	adantllr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌))
389		iftrue 4498	. . . . . . . . . . . . . . . . . . . . . . 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 5138	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘))
394		iffalse 4501	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = 𝑌)
395	394	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) = 𝑌)
396		simpl1 1210	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))))
397		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑘 = 𝐾 ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ¬ 𝑌 ≤ (𝑓‘𝑘))
398		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 = 𝐾 → (𝑓‘𝑘) = (𝑓‘𝐾))
399	398	breq2d 5126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓‘𝑘) ∈ ℝ))
413	412	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → (𝑓‘𝑘) ∈ ℝ))
414	406, 413	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
415	414	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ ℝ)
416	405, 415	eqeltrd 2866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) → (𝑓‘𝐾) ∈ ℝ)
417	416	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝑓‘𝐾) ∈ ℝ)
418	396, 361, 37	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → 𝑌 ∈ ℝ)
419	417, 418	ltnled 11375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → ((𝑓‘𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝑓‘𝐾)))
420	403, 419	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → (𝑓‘𝐾) < 𝑌)
421	365, 364	r19.29a 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → -∞ < (𝑓‘𝑘))
427	398	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) = (𝑓‘𝐾))
428		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝐾) < 𝑌)
429	427, 428	eqbrtrd 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑓‘𝐾) < 𝑌 ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌)
430	429	ad4ant24 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) < 𝑌)
431	423, 424, 425, 426, 430	eliood 46255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ (-∞(,)𝑌))
432	155	eqcomd 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 = 𝐾 → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
433	432	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (-∞(,)𝑌) = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
434	431, 433	eleqtrd 2868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
435	414	ad4ant13 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ ℝ)
436	159	eqcomd 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ 𝑘 = 𝐾 → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
437	436	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ℝ = if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
438	435, 437	eleqtrd 2868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
439	434, 438	pm2.61dan 825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ (𝑓‘𝐾) < 𝑌) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ))
440	439	ralrimiva 3160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌))
445	444	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌))
446	445	3ad2antl1 1204	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝐾, (-∞(,)𝑌), ℝ) = (𝐾(𝐻‘𝑋)𝑌))
447	443, 446	eleqtrd 2868	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑘 ∈ 𝑋 ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ (𝑓‘𝑘)) → 𝑓 ∈ (𝐾(𝐻‘𝑋)𝑌))
448		eldifn 4089	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5138	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) ∧ ¬ 𝑌 ≤ ((𝐶‘𝑗)‘𝑘)) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘))
456	393, 455	pm2.61dan 825	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌) ≤ (𝑓‘𝑘))
457	388, 456	eqbrtrd 5138	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) ≤ (𝑓‘𝑘))
458	383	ad5ant124 1388	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)))
459		iffalse 4501	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑘 = 𝐾 → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = ((𝐶‘𝑗)‘𝑘))
460	459	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → if(𝑘 = 𝐾, if(𝑌 ≤ ((𝐶‘𝑗)‘𝑘), ((𝐶‘𝑗)‘𝑘), 𝑌), ((𝐶‘𝑗)‘𝑘)) = ((𝐶‘𝑗)‘𝑘))
461	458, 460	eqtrd 2801	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘) = ((𝐶‘𝑗)‘𝑘))
462	197	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝐾) → ((𝐶‘𝑗)‘𝑘) ≤ (𝑓‘𝑘))
463	461, 462	eqbrtrd 5138	. . . . . . . . . . . . . . . . . . . 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 13440	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
468	467	ex 418	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑘 ∈ 𝑋 → (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
469	367, 468	ralrimi 3266	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
470	365, 469	jca 521	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
471	171	elixp 8911	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
472	470, 471	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
473		eqidd 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))) = (𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙))))
474		2fveq3 6893	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 = 𝑗 → ((𝑆‘𝑌)‘(𝐶‘𝑙)) = ((𝑆‘𝑌)‘(𝐶‘𝑗)))
475	474	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ ℕ ∧ 𝑙 = 𝑗) → ((𝑆‘𝑌)‘(𝐶‘𝑙)) = ((𝑆‘𝑌)‘(𝐶‘𝑗)))
476		fvexd 6903	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ → ((𝑆‘𝑌)‘(𝐶‘𝑗)) ∈ V)
477	473, 475, 338, 476	fvmptd 7004	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ ℕ → ((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗) = ((𝑆‘𝑌)‘(𝐶‘𝑗)))
478	477	fveq1d 6890	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘) = (((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘))
479	478	oveq1d 7438	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
480	479	ixpeq2dv 8920	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
481	480	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
482	481	eleq2d 2852	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → (𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑆‘𝑌)‘(𝐶‘𝑗))‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
483	472, 482	mpbird 260	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
484	483	ex 418	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∧ 𝑗 ∈ ℕ) → (𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
485	484	reximdva 3181	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → (∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))
486	364, 485	mpd 16	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
487		eliun 4965	. . . . . . . . 9 ⊢ (𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∃𝑗 ∈ ℕ 𝑓 ∈ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
488	486, 487	sylibr 237	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) → 𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
489	488	ralrimiva 3160	. . . . . . 7 ⊢ (𝜑 → ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
490		dfss3 3929	. . . . . . 7 ⊢ ((𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ↔ ∀𝑓 ∈ (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))𝑓 ∈ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
491	489, 490	sylibr 237	. . . . . 6 ⊢ (𝜑 → (𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
492	13, 360, 19, 491, 12	ovnlecvr2 47365	. . . . 5 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
493	477	oveq1d 7438	. . . . . . . 8 ⊢ (𝑗 ∈ ℕ → (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))
494	493	mpteq2ia 5211	. . . . . . 7 ⊢ (𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))
495	494	fveq2i 6891	. . . . . 6 ⊢ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))
496	495	a1i 11	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑙 ∈ ℕ ↦ ((𝑆‘𝑌)‘(𝐶‘𝑙)))‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))
497	492, 496	breqtrd 5142	. . . 4 ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))
498	1, 2, 96, 108, 351, 497	le2addd 11851	. . 3 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) + (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
499	14, 105, 38, 18, 22, 12, 36, 97	hspmbllem1 47381	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))
500	499	mpteq2dva 5209	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗)))))
501	500	fveq2d 6892	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
502	8, 10, 41, 104	sge0xadd 47190	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))) +_𝑒 (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) = ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) +_𝑒 (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
503	96, 108	rexaddd 13278	. . . 4 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) +_𝑒 (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) = ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) + (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))))
504	501, 502, 503	3eqtrrd 2806	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)((𝑇‘𝑌)‘(𝐷‘𝑗))))) + (Σ^{^}‘(𝑗 ∈ ℕ ↦ (((𝑆‘𝑌)‘(𝐶‘𝑗))(𝐿‘𝑋)(𝐷‘𝑗))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
505	498, 504	breqtrd 5142	. 2 ⊢ (𝜑 → (((voln‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))))
506	3, 35, 7, 505, 34	letrd 11385	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 2146 ≠ wne 2961 ∀wral 3082 ∃wrex 3092 Vcvv 3458 ∖ cdif 3905 ∪ cun 3906 ∩ cin 3907 ⊆ wss 3908 ∅c0 4289 ifcif 4492 {csn 4594 ∪ ciun 4961 class class class wbr 5114 ↦ cmpt 5197 Fn wfn 6538 ⟶wf 6539 ‘cfv 6543 (class class class)co 7423 ∈ cmpo 7425 ↑_m cmap 8833 Xcixp 8904 Fincfn 8952 ℝcr 11117 0cc0 11118 + caddc 11121 +∞cpnf 11258 -∞cmnf 11259 ℝ^*cxr 11260 < clt 11261 ≤ cle 11262 ℕcn 12251 ℝ⁺crp 13034 +_𝑒 cxad 13153 (,)cioo 13390 [,)cico 13392 [,]cicc 13393 ∏cprod 15983 volcvol 25659 Σ^{^}csumge0 47117 voln*covoln 47291

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-inf2 9620 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196

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 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-se 5620 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-of 7687 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-2o 8463 df-er 8703 df-map 8835 df-pm 8836 df-ixp 8905 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-fi 9381 df-sup 9412 df-inf 9413 df-oi 9482 df-dju 9906 df-card 9944 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-2 12321 df-3 12322 df-n0 12523 df-z 12610 df-uz 12881 df-q 12991 df-rp 13035 df-xneg 13155 df-xadd 13156 df-xmul 13157 df-ioo 13394 df-ico 13396 df-icc 13397 df-fz 13554 df-fzo 13702 df-fl 13845 df-seq 14058 df-exp 14118 df-hash 14387 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-clim 15565 df-rlim 15566 df-sum 15764 df-prod 15984 df-rest 17500 df-topgen 17521 df-psmet 21551 df-xmet 21552 df-met 21553 df-bl 21554 df-mopn 21555 df-top 23088 df-topon 23105 df-bases 23140 df-cmp 23581 df-ovol 25660 df-vol 25661 df-sumge0 47118 df-ovoln 47292

This theorem is used by: hspmbllem3 47383

W3C validator