Theorem hoidifhspval

Description: D is a function that returns the representation of the left side of the difference of a half-open interval and a half-space. Used in Lemma 115F of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	hoidifhspval.d	$$⊢D=\left(x\in ℝ⟼\left(a\in \left({ℝ}^X\right)⟼\left(k\in X⟼if\left(k=K,if\left(x\le a\left(k\right),a\left(k\right),x\right),a\left(k\right)\right)\right)\right)\right)$$
	hoidifhspval.y	$$⊢\phi \to Y\in ℝ$$
Assertion	hoidifhspval	$$⊢\phi \to D\left(Y\right)=\left(a\in \left({ℝ}^X\right)⟼\left(k\in X⟼if\left(k=K,if\left(Y\le a\left(k\right),a\left(k\right),Y\right),a\left(k\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hoidifhspval.d	$$⊢D=\left(x\in ℝ⟼\left(a\in \left({ℝ}^X\right)⟼\left(k\in X⟼if\left(k=K,if\left(x\le a\left(k\right),a\left(k\right),x\right),a\left(k\right)\right)\right)\right)\right)$$
2		hoidifhspval.y	$$⊢\phi \to Y\in ℝ$$
3		breq1	$$⊢x=Y\to \left(x\le a\left(k\right)\leftrightarrow Y\le a\left(k\right)\right)$$
4		id	$$⊢x=Y\to x=Y$$
5	3 4	ifbieq2d	$$⊢x=Y\to if\left(x\le a\left(k\right),a\left(k\right),x\right)=if\left(Y\le a\left(k\right),a\left(k\right),Y\right)$$
6	5	ifeq1d	$$⊢x=Y\to if\left(k=K,if\left(x\le a\left(k\right),a\left(k\right),x\right),a\left(k\right)\right)=if\left(k=K,if\left(Y\le a\left(k\right),a\left(k\right),Y\right),a\left(k\right)\right)$$
7	6	mpteq2dv	$$⊢x=Y\to \left(k\in X⟼if\left(k=K,if\left(x\le a\left(k\right),a\left(k\right),x\right),a\left(k\right)\right)\right)=\left(k\in X⟼if\left(k=K,if\left(Y\le a\left(k\right),a\left(k\right),Y\right),a\left(k\right)\right)\right)$$
8	7	mpteq2dv	$$⊢x=Y\to \left(a\in \left({ℝ}^X\right)⟼\left(k\in X⟼if\left(k=K,if\left(x\le a\left(k\right),a\left(k\right),x\right),a\left(k\right)\right)\right)\right)=\left(a\in \left({ℝ}^X\right)⟼\left(k\in X⟼if\left(k=K,if\left(Y\le a\left(k\right),a\left(k\right),Y\right),a\left(k\right)\right)\right)\right)$$
9		ovex	$$⊢{ℝ}^X\in \mathrm{V}$$
10	9	mptex	$$⊢\left(a\in \left({ℝ}^X\right)⟼\left(k\in X⟼if\left(k=K,if\left(Y\le a\left(k\right),a\left(k\right),Y\right),a\left(k\right)\right)\right)\right)\in \mathrm{V}$$
11	10	a1i	$$⊢\phi \to \left(a\in \left({ℝ}^X\right)⟼\left(k\in X⟼if\left(k=K,if\left(Y\le a\left(k\right),a\left(k\right),Y\right),a\left(k\right)\right)\right)\right)\in \mathrm{V}$$
12	1 8 2 11	fvmptd3	$$⊢\phi \to D\left(Y\right)=\left(a\in \left({ℝ}^X\right)⟼\left(k\in X⟼if\left(k=K,if\left(Y\le a\left(k\right),a\left(k\right),Y\right),a\left(k\right)\right)\right)\right)$$