Theorem cncfioobdlem

Description: G actually extends F . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	cncfioobdlem.a	$$⊢\phi \to A\in ℝ$$
	cncfioobdlem.b	$$⊢\phi \to B\in ℝ$$
	cncfioobdlem.f	$$⊢\phi \to F:\left(A,B\right)⟶V$$
	cncfioobdlem.g	$$⊢G=\left(x\in \left[A,B\right]⟼if\left(x=A,R,if\left(x=B,L,F\left(x\right)\right)\right)\right)$$
	cncfioobdlem.c	$$⊢\phi \to C\in \left(A,B\right)$$
Assertion	cncfioobdlem	$$⊢\phi \to G\left(C\right)=F\left(C\right)$$

Proof

Step	Hyp	Ref	Expression
1		cncfioobdlem.a	$$⊢\phi \to A\in ℝ$$
2		cncfioobdlem.b	$$⊢\phi \to B\in ℝ$$
3		cncfioobdlem.f	$$⊢\phi \to F:\left(A,B\right)⟶V$$
4		cncfioobdlem.g	$$⊢G=\left(x\in \left[A,B\right]⟼if\left(x=A,R,if\left(x=B,L,F\left(x\right)\right)\right)\right)$$
5		cncfioobdlem.c	$$⊢\phi \to C\in \left(A,B\right)$$
6	4	a1i	$$⊢\phi \to G=\left(x\in \left[A,B\right]⟼if\left(x=A,R,if\left(x=B,L,F\left(x\right)\right)\right)\right)$$
7	1	adantr	$$⊢\left(\phi \wedge x=C\right)\to A\in ℝ$$
8	1	rexrd	$$⊢\phi \to A\in {ℝ}^{*}$$
9	2	rexrd	$$⊢\phi \to B\in {ℝ}^{*}$$
10		elioo2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(C\in \left(A,B\right)\leftrightarrow \left(C\in ℝ\wedge A<C\wedge C<B\right)\right)$$
11	8 9 10	syl2anc	$$⊢\phi \to \left(C\in \left(A,B\right)\leftrightarrow \left(C\in ℝ\wedge A<C\wedge C<B\right)\right)$$
12	5 11	mpbid	$$⊢\phi \to \left(C\in ℝ\wedge A<C\wedge C<B\right)$$
13	12	simp2d	$$⊢\phi \to A<C$$
14	13	adantr	$$⊢\left(\phi \wedge x=C\right)\to A<C$$
15		eqcom	$$⊢x=C\leftrightarrow C=x$$
16	15	biimpi	$$⊢x=C\to C=x$$
17	16	adantl	$$⊢\left(\phi \wedge x=C\right)\to C=x$$
18	14 17	breqtrd	$$⊢\left(\phi \wedge x=C\right)\to A<x$$
19	7 18	gtned	$$⊢\left(\phi \wedge x=C\right)\to x\ne A$$
20	19	neneqd	$$⊢\left(\phi \wedge x=C\right)\to \neg x=A$$
21	20	iffalsed	$$⊢\left(\phi \wedge x=C\right)\to if\left(x=A,R,if\left(x=B,L,F\left(x\right)\right)\right)=if\left(x=B,L,F\left(x\right)\right)$$
22		simpr	$$⊢\left(\phi \wedge x=C\right)\to x=C$$
23	5	elioored	$$⊢\phi \to C\in ℝ$$
24	23	adantr	$$⊢\left(\phi \wedge x=C\right)\to C\in ℝ$$
25	22 24	eqeltrd	$$⊢\left(\phi \wedge x=C\right)\to x\in ℝ$$
26	12	simp3d	$$⊢\phi \to C<B$$
27	26	adantr	$$⊢\left(\phi \wedge x=C\right)\to C<B$$
28	22 27	eqbrtrd	$$⊢\left(\phi \wedge x=C\right)\to x<B$$
29	25 28	ltned	$$⊢\left(\phi \wedge x=C\right)\to x\ne B$$
30	29	neneqd	$$⊢\left(\phi \wedge x=C\right)\to \neg x=B$$
31	30	iffalsed	$$⊢\left(\phi \wedge x=C\right)\to if\left(x=B,L,F\left(x\right)\right)=F\left(x\right)$$
32	22	fveq2d	$$⊢\left(\phi \wedge x=C\right)\to F\left(x\right)=F\left(C\right)$$
33	21 31 32	3eqtrd	$$⊢\left(\phi \wedge x=C\right)\to if\left(x=A,R,if\left(x=B,L,F\left(x\right)\right)\right)=F\left(C\right)$$
34		ioossicc	$$⊢\left(A,B\right)\subseteq \left[A,B\right]$$
35	34 5	sselid	$$⊢\phi \to C\in \left[A,B\right]$$
36	3 5	ffvelcdmd	$$⊢\phi \to F\left(C\right)\in V$$
37	6 33 35 36	fvmptd	$$⊢\phi \to G\left(C\right)=F\left(C\right)$$