This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bilani 
 |-  ( ( ph /\ x = C ) -> C = x )
17 14 16 breqtrd 
 |-  ( ( ph /\ x = C ) -> A < x )
18 7 17 gtned 
 |-  ( ( ph /\ x = C ) -> x =/= A )
19 18 neneqd 
 |-  ( ( ph /\ x = C ) -> -. x = A )
20 19 iffalsed 
 |-  ( ( ph /\ x = C ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
21 simpr 
 |-  ( ( ph /\ x = C ) -> x = C )
22 5 elioored 
 |-  ( ph -> C e. RR )
23 22 adantr 
 |-  ( ( ph /\ x = C ) -> C e. RR )
24 21 23 eqeltrd 
 |-  ( ( ph /\ x = C ) -> x e. RR )
25 12 simp3d 
 |-  ( ph -> C < B )
26 25 adantr 
 |-  ( ( ph /\ x = C ) -> C < B )
27 21 26 eqbrtrd 
 |-  ( ( ph /\ x = C ) -> x < B )
28 24 27 ltned 
 |-  ( ( ph /\ x = C ) -> x =/= B )
29 28 neneqd 
 |-  ( ( ph /\ x = C ) -> -. x = B )
30 29 iffalsed 
 |-  ( ( ph /\ x = C ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
31 21 fveq2d 
 |-  ( ( ph /\ x = C ) -> ( F ` x ) = ( F ` C ) )
32 20 30 31 3eqtrd 
 |-  ( ( ph /\ x = C ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( F ` C ) )
33 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
34 33 5 sselid 
 |-  ( ph -> C e. ( A [,] B ) )
35 3 5 ffvelcdmd 
 |-  ( ph -> ( F ` C ) e. V )
36 6 32 34 35 fvmptd 
 |-  ( ph -> ( G ` C ) = ( F ` C ) )