Theorem hsphoif

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	hsphoif.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)$$
	hsphoif.a	$$⊢\phi \to A\in ℝ$$
	hsphoif.x	$$⊢\phi \to X\in V$$
	hsphoif.b	$$⊢\phi \to B:X⟶ℝ$$
Assertion	hsphoif	$$⊢\phi \to H\left(A\right)\left(B\right):X⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		hsphoif.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		hsphoif.a	$$⊢\phi \to A\in ℝ$$
3		hsphoif.x	$$⊢\phi \to X\in V$$
4		hsphoif.b	$$⊢\phi \to B:X⟶ℝ$$
5	4	ffvelrnda	$$⊢\left(\phi \wedge j\in X\right)\to B\left(j\right)\in ℝ$$
6	2	adantr	$$⊢\left(\phi \wedge j\in X\right)\to A\in ℝ$$
7	5 6	ifcld	$$⊢\left(\phi \wedge j\in X\right)\to if\left(B\left(j\right)\le A,B\left(j\right),A\right)\in ℝ$$
8	5 7	ifcld	$$⊢\left(\phi \wedge j\in X\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)\in ℝ$$
9		eqid	$$⊢\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)=\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)$$
10	8 9	fmptd	$$⊢\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):X⟶ℝ$$
11		breq2	$$⊢x=A\to \left(a\left(j\right)\le x\leftrightarrow a\left(j\right)\le A\right)$$
12		id	$$⊢x=A\to x=A$$
13	11 12	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)$$
14	13	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)$$
15	14	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)$$
16	15	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)$$
17		ovex	$$⊢{ℝ}^X\in \mathrm{V}$$
18	17	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}$$
19	18	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}$$
20	1 16 2 19	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)$$
21		fveq1	$$⊢a=B\to a\left(j\right)=B\left(j\right)$$
22	21	breq1d	$$⊢a=B\to \left(a\left(j\right)\le A\leftrightarrow B\left(j\right)\le A\right)$$
23	22 21	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)$$
24	21 23	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)$$
25	24	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)$$
26	25	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)$$
27		reex	$$⊢ℝ\in \mathrm{V}$$
28	27	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
29	28 3	jca	$$⊢\phi \to \left(ℝ\in \mathrm{V}\wedge X\in V\right)$$
30		elmapg	$$⊢\left(ℝ\in \mathrm{V}\wedge X\in V\right)\to \left(B\in \left({ℝ}^X\right)\leftrightarrow B:X⟶ℝ\right)$$
31	29 30	syl	$$⊢\phi \to \left(B\in \left({ℝ}^X\right)\leftrightarrow B:X⟶ℝ\right)$$
32	4 31	mpbird	$$⊢\phi \to B\in \left({ℝ}^X\right)$$
33		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}$$
34	3 33	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}$$
35	20 26 32 34	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)$$
36	35	feq1d	$$⊢\phi \to \left(H\left(A\right)\left(B\right):X⟶ℝ\leftrightarrow \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):X⟶ℝ\right)$$
37	10 36	mpbird	$$⊢\phi \to H\left(A\right)\left(B\right):X⟶ℝ$$