Metamath Proof Explorer

Theorem cncfioobdlem

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

Ref Expression
Hypotheses cncfioobdlem.a 
|- ( ph -> A e. RR )
cncfioobdlem.b 
|- ( ph -> B e. RR )
cncfioobdlem.f 
|- ( ph -> F : ( A (,) B ) --> V )
cncfioobdlem.g 
|- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
cncfioobdlem.c 
|- ( ph -> C e. ( A (,) B ) )
Assertion cncfioobdlem 
|- ( ph -> ( G ` C ) = ( F ` C ) )

Proof

Step Hyp Ref Expression
1 cncfioobdlem.a 
 |-  ( ph -> A e. RR )
2 cncfioobdlem.b 
 |-  ( ph -> B e. RR )
3 cncfioobdlem.f 
 |-  ( ph -> F : ( A (,) B ) --> V )
4 cncfioobdlem.g 
 |-  G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
5 cncfioobdlem.c 
 |-  ( ph -> C e. ( A (,) B ) )
6 4 a1i 
 |-  ( ph -> G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) )
7 1 adantr 
 |-  ( ( ph /\ x = C ) -> A e. RR )
8 1 rexrd 
 |-  ( ph -> A e. RR* )
9 2 rexrd 
 |-  ( ph -> B e. RR* )
10 elioo2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> ( C e. RR /\ A < C /\ C < B ) ) )
11 8 9 10 syl2anc 
 |-  ( ph -> ( C e. ( A (,) B ) <-> ( C e. RR /\ A < C /\ C < B ) ) )
12 5 11 mpbid 
 |-  ( ph -> ( C e. RR /\ A < C /\ C < B ) )
13 12 simp2d 
 |-  ( ph -> A < C )
14 13 adantr 
 |-  ( ( ph /\ x = C ) -> A < C )
15 eqcom 
 |-  ( x = C <-> C = x )
16 15 biimpi 
 |-  ( x = C -> C = x )
17 16 adantl 
 |-  ( ( ph /\ x = C ) -> C = x )
18 14 17 breqtrd 
 |-  ( ( ph /\ x = C ) -> A < x )
19 7 18 gtned 
 |-  ( ( ph /\ x = C ) -> x =/= A )
20 19 neneqd 
 |-  ( ( ph /\ x = C ) -> -. x = A )
21 20 iffalsed 
 |-  ( ( ph /\ x = C ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
22 simpr 
 |-  ( ( ph /\ x = C ) -> x = C )
23 5 elioored 
 |-  ( ph -> C e. RR )
24 23 adantr 
 |-  ( ( ph /\ x = C ) -> C e. RR )
25 22 24 eqeltrd 
 |-  ( ( ph /\ x = C ) -> x e. RR )
26 12 simp3d 
 |-  ( ph -> C < B )
27 26 adantr 
 |-  ( ( ph /\ x = C ) -> C < B )
28 22 27 eqbrtrd 
 |-  ( ( ph /\ x = C ) -> x < B )
29 25 28 ltned 
 |-  ( ( ph /\ x = C ) -> x =/= B )
30 29 neneqd 
 |-  ( ( ph /\ x = C ) -> -. x = B )
31 30 iffalsed 
 |-  ( ( ph /\ x = C ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
32 22 fveq2d 
 |-  ( ( ph /\ x = C ) -> ( F ` x ) = ( F ` C ) )
33 21 31 32 3eqtrd 
 |-  ( ( ph /\ x = C ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( F ` C ) )
34 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
35 34 5 sseldi 
 |-  ( ph -> C e. ( A [,] B ) )
36 3 5 ffvelrnd 
 |-  ( ph -> ( F ` C ) e. V )
37 6 33 35 36 fvmptd 
 |-  ( ph -> ( G ` C ) = ( F ` C ) )