Theorem hsphoival

Description: H is a function (that returns the representation of the right side of a half-open interval intersected with a half-space). Step (b) in Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	hsphoival.h	$$⊢H=\left(x\in ℝ⟼\left(a\in \left({ℝ}^X\right)⟼\left(j\in X⟼if\left(j\in Y,a\left(j\right),if\left(a\left(j\right)\le x,a\left(j\right),x\right)\right)\right)\right)\right)$$
	hsphoival.a	$$⊢\phi \to A\in ℝ$$
	hsphoival.x	$$⊢\phi \to X\in V$$
	hsphoival.b	$$⊢\phi \to B:X⟶ℝ$$
	hsphoival.k	$$⊢\phi \to K\in X$$
Assertion	hsphoival	$$⊢\phi \to H\left(A\right)\left(B\right)\left(K\right)=if\left(K\in Y,B\left(K\right),if\left(B\left(K\right)\le A,B\left(K\right),A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hsphoival.h	$$⊢H=\left(x\in ℝ⟼\left(a\in \left({ℝ}^X\right)⟼\left(j\in X⟼if\left(j\in Y,a\left(j\right),if\left(a\left(j\right)\le x,a\left(j\right),x\right)\right)\right)\right)\right)$$
2		hsphoival.a	$$⊢\phi \to A\in ℝ$$
3		hsphoival.x	$$⊢\phi \to X\in V$$
4		hsphoival.b	$$⊢\phi \to B:X⟶ℝ$$
5		hsphoival.k	$$⊢\phi \to K\in X$$
6		breq2	$$⊢x=A\to \left(a\left(j\right)\le x\leftrightarrow a\left(j\right)\le A\right)$$
7		id	$$⊢x=A\to x=A$$
8	6 7	ifbieq2d	$$⊢x=A\to if\left(a\left(j\right)\le x,a\left(j\right),x\right)=if\left(a\left(j\right)\le A,a\left(j\right),A\right)$$
9	8	ifeq2d	$$⊢x=A\to if\left(j\in Y,a\left(j\right),if\left(a\left(j\right)\le x,a\left(j\right),x\right)\right)=if\left(j\in Y,a\left(j\right),if\left(a\left(j\right)\le A,a\left(j\right),A\right)\right)$$
10	9	mpteq2dv	$$⊢x=A\to \left(j\in X⟼if\left(j\in Y,a\left(j\right),if\left(a\left(j\right)\le x,a\left(j\right),x\right)\right)\right)=\left(j\in X⟼if\left(j\in Y,a\left(j\right),if\left(a\left(j\right)\le A,a\left(j\right),A\right)\right)\right)$$
11	10	mpteq2dv	$$⊢x=A\to \left(a\in \left({ℝ}^X\right)⟼\left(j\in X⟼if\left(j\in Y,a\left(j\right),if\left(a\left(j\right)\le x,a\left(j\right),x\right)\right)\right)\right)=\left(a\in \left({ℝ}^X\right)⟼\left(j\in X⟼if\left(j\in Y,a\left(j\right),if\left(a\left(j\right)\le A,a\left(j\right),A\right)\right)\right)\right)$$
12		ovex	$$⊢{ℝ}^X\in \mathrm{V}$$
13	12	mptex	$$⊢\left(a\in \left({ℝ}^X\right)⟼\left(j\in X⟼if\left(j\in Y,a\left(j\right),if\left(a\left(j\right)\le A,a\left(j\right),A\right)\right)\right)\right)\in \mathrm{V}$$
14	13	a1i	$$⊢\phi \to \left(a\in \left({ℝ}^X\right)⟼\left(j\in X⟼if\left(j\in Y,a\left(j\right),if\left(a\left(j\right)\le A,a\left(j\right),A\right)\right)\right)\right)\in \mathrm{V}$$
15	1 11 2 14	fvmptd3	$$⊢\phi \to H\left(A\right)=\left(a\in \left({ℝ}^X\right)⟼\left(j\in X⟼if\left(j\in Y,a\left(j\right),if\left(a\left(j\right)\le A,a\left(j\right),A\right)\right)\right)\right)$$
16		fveq1	$$⊢a=B\to a\left(j\right)=B\left(j\right)$$
17	16	breq1d	$$⊢a=B\to \left(a\left(j\right)\le A\leftrightarrow B\left(j\right)\le A\right)$$
18	17 16	ifbieq1d	$$⊢a=B\to if\left(a\left(j\right)\le A,a\left(j\right),A\right)=if\left(B\left(j\right)\le A,B\left(j\right),A\right)$$
19	16 18	ifeq12d	$$⊢a=B\to if\left(j\in Y,a\left(j\right),if\left(a\left(j\right)\le A,a\left(j\right),A\right)\right)=if\left(j\in Y,B\left(j\right),if\left(B\left(j\right)\le A,B\left(j\right),A\right)\right)$$
20	19	mpteq2dv	$$⊢a=B\to \left(j\in X⟼if\left(j\in Y,a\left(j\right),if\left(a\left(j\right)\le A,a\left(j\right),A\right)\right)\right)=\left(j\in X⟼if\left(j\in Y,B\left(j\right),if\left(B\left(j\right)\le A,B\left(j\right),A\right)\right)\right)$$
21	20	adantl	$$⊢\left(\phi \wedge a=B\right)\to \left(j\in X⟼if\left(j\in Y,a\left(j\right),if\left(a\left(j\right)\le A,a\left(j\right),A\right)\right)\right)=\left(j\in X⟼if\left(j\in Y,B\left(j\right),if\left(B\left(j\right)\le A,B\left(j\right),A\right)\right)\right)$$
22		reex	$$⊢ℝ\in \mathrm{V}$$
23	22	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
24	23 3	jca	$$⊢\phi \to \left(ℝ\in \mathrm{V}\wedge X\in V\right)$$
25		elmapg	$$⊢\left(ℝ\in \mathrm{V}\wedge X\in V\right)\to \left(B\in \left({ℝ}^X\right)\leftrightarrow B:X⟶ℝ\right)$$
26	24 25	syl	$$⊢\phi \to \left(B\in \left({ℝ}^X\right)\leftrightarrow B:X⟶ℝ\right)$$
27	4 26	mpbird	$$⊢\phi \to B\in \left({ℝ}^X\right)$$
28		mptexg	$$⊢X\in V\to \left(j\in X⟼if\left(j\in Y,B\left(j\right),if\left(B\left(j\right)\le A,B\left(j\right),A\right)\right)\right)\in \mathrm{V}$$
29	3 28	syl	$$⊢\phi \to \left(j\in X⟼if\left(j\in Y,B\left(j\right),if\left(B\left(j\right)\le A,B\left(j\right),A\right)\right)\right)\in \mathrm{V}$$
30	15 21 27 29	fvmptd	$$⊢\phi \to H\left(A\right)\left(B\right)=\left(j\in X⟼if\left(j\in Y,B\left(j\right),if\left(B\left(j\right)\le A,B\left(j\right),A\right)\right)\right)$$
31		eleq1	$$⊢j=K\to \left(j\in Y\leftrightarrow K\in Y\right)$$
32		fveq2	$$⊢j=K\to B\left(j\right)=B\left(K\right)$$
33	32	breq1d	$$⊢j=K\to \left(B\left(j\right)\le A\leftrightarrow B\left(K\right)\le A\right)$$
34	33 32	ifbieq1d	$$⊢j=K\to if\left(B\left(j\right)\le A,B\left(j\right),A\right)=if\left(B\left(K\right)\le A,B\left(K\right),A\right)$$
35	31 32 34	ifbieq12d	$$⊢j=K\to if\left(j\in Y,B\left(j\right),if\left(B\left(j\right)\le A,B\left(j\right),A\right)\right)=if\left(K\in Y,B\left(K\right),if\left(B\left(K\right)\le A,B\left(K\right),A\right)\right)$$
36	35	adantl	$$⊢\left(\phi \wedge j=K\right)\to if\left(j\in Y,B\left(j\right),if\left(B\left(j\right)\le A,B\left(j\right),A\right)\right)=if\left(K\in Y,B\left(K\right),if\left(B\left(K\right)\le A,B\left(K\right),A\right)\right)$$
37	4 5	ffvelcdmd	$$⊢\phi \to B\left(K\right)\in ℝ$$
38	37 2	ifcld	$$⊢\phi \to if\left(B\left(K\right)\le A,B\left(K\right),A\right)\in ℝ$$
39	37 38	ifexd	$$⊢\phi \to if\left(K\in Y,B\left(K\right),if\left(B\left(K\right)\le A,B\left(K\right),A\right)\right)\in \mathrm{V}$$
40	30 36 5 39	fvmptd	$$⊢\phi \to H\left(A\right)\left(B\right)\left(K\right)=if\left(K\in Y,B\left(K\right),if\left(B\left(K\right)\le A,B\left(K\right),A\right)\right)$$