Theorem fourierdlem17

Description: The defined L is actually a function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem17.a	$$⊢\phi \to A\in ℝ$$
	fourierdlem17.b	$$⊢\phi \to B\in ℝ$$
	fourierdlem17.altb	$$⊢\phi \to A<B$$
	fourierdlem17.l	$$⊢L=\left(x\in \left(A,B\right]⟼if\left(x=B,A,x\right)\right)$$
Assertion	fourierdlem17	$$⊢\phi \to L:\left(A,B\right]⟶\left[A,B\right]$$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem17.a	$$⊢\phi \to A\in ℝ$$
2		fourierdlem17.b	$$⊢\phi \to B\in ℝ$$
3		fourierdlem17.altb	$$⊢\phi \to A<B$$
4		fourierdlem17.l	$$⊢L=\left(x\in \left(A,B\right]⟼if\left(x=B,A,x\right)\right)$$
5	1	leidd	$$⊢\phi \to A\le A$$
6	1 2 3	ltled	$$⊢\phi \to A\le B$$
7	1 2 1 5 6	eliccd	$$⊢\phi \to A\in \left[A,B\right]$$
8	7	ad2antrr	$$⊢\left(\left(\phi \wedge x\in \left(A,B\right]\right)\wedge x=B\right)\to A\in \left[A,B\right]$$
9		iocssicc	$$⊢\left(A,B\right]\subseteq \left[A,B\right]$$
10	9	sseli	$$⊢x\in \left(A,B\right]\to x\in \left[A,B\right]$$
11	10	ad2antlr	$$⊢\left(\left(\phi \wedge x\in \left(A,B\right]\right)\wedge \neg x=B\right)\to x\in \left[A,B\right]$$
12	8 11	ifclda	$$⊢\left(\phi \wedge x\in \left(A,B\right]\right)\to if\left(x=B,A,x\right)\in \left[A,B\right]$$
13	12 4	fmptd	$$⊢\phi \to L:\left(A,B\right]⟶\left[A,B\right]$$