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

Metamath Proof Explorer

Theorem dvgt0lem2

Description: Lemma for dvgt0 and dvlt0 . (Contributed by Mario Carneiro, 19-Feb-2015)

Ref Expression
Hypotheses dvgt0.a 
|- ( ph -> A e. RR )
dvgt0.b 
|- ( ph -> B e. RR )
dvgt0.f 
|- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
dvgt0lem.d 
|- ( ph -> ( RR _D F ) : ( A (,) B ) --> S )
dvgt0lem.o 
|- O Or RR
dvgt0lem.i 
|- ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` x ) O ( F ` y ) )
Assertion dvgt0lem2 
|- ( ph -> F Isom < , O ( ( A [,] B ) , ran F ) )

Proof

Step Hyp Ref Expression
1 dvgt0.a 
 |-  ( ph -> A e. RR )
2 dvgt0.b 
 |-  ( ph -> B e. RR )
3 dvgt0.f 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
4 dvgt0lem.d 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> S )
5 dvgt0lem.o 
 |-  O Or RR
6 dvgt0lem.i 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` x ) O ( F ` y ) )
7 6 ex 
 |-  ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( x < y -> ( F ` x ) O ( F ` y ) ) )
8 7 ralrimivva 
 |-  ( ph -> A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( x < y -> ( F ` x ) O ( F ` y ) ) )
9 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
10 1 2 9 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
11 ltso 
 |-  < Or RR
12 soss 
 |-  ( ( A [,] B ) C_ RR -> ( < Or RR -> < Or ( A [,] B ) ) )
13 10 11 12 mpisyl 
 |-  ( ph -> < Or ( A [,] B ) )
14 5 a1i 
 |-  ( ph -> O Or RR )
15 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> RR ) -> F : ( A [,] B ) --> RR )
16 3 15 syl 
 |-  ( ph -> F : ( A [,] B ) --> RR )
17 ssidd 
 |-  ( ph -> ( A [,] B ) C_ ( A [,] B ) )
18 soisores 
 |-  ( ( ( < Or ( A [,] B ) /\ O Or RR ) /\ ( F : ( A [,] B ) --> RR /\ ( A [,] B ) C_ ( A [,] B ) ) ) -> ( ( F |` ( A [,] B ) ) Isom < , O ( ( A [,] B ) , ( F " ( A [,] B ) ) ) <-> A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( x < y -> ( F ` x ) O ( F ` y ) ) ) )
19 13 14 16 17 18 syl22anc 
 |-  ( ph -> ( ( F |` ( A [,] B ) ) Isom < , O ( ( A [,] B ) , ( F " ( A [,] B ) ) ) <-> A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( x < y -> ( F ` x ) O ( F ` y ) ) ) )
20 8 19 mpbird 
 |-  ( ph -> ( F |` ( A [,] B ) ) Isom < , O ( ( A [,] B ) , ( F " ( A [,] B ) ) ) )
21 ffn 
 |-  ( F : ( A [,] B ) --> RR -> F Fn ( A [,] B ) )
22 3 15 21 3syl 
 |-  ( ph -> F Fn ( A [,] B ) )
23 fnresdm 
 |-  ( F Fn ( A [,] B ) -> ( F |` ( A [,] B ) ) = F )
24 isoeq1 
 |-  ( ( F |` ( A [,] B ) ) = F -> ( ( F |` ( A [,] B ) ) Isom < , O ( ( A [,] B ) , ( F " ( A [,] B ) ) ) <-> F Isom < , O ( ( A [,] B ) , ( F " ( A [,] B ) ) ) ) )
25 22 23 24 3syl 
 |-  ( ph -> ( ( F |` ( A [,] B ) ) Isom < , O ( ( A [,] B ) , ( F " ( A [,] B ) ) ) <-> F Isom < , O ( ( A [,] B ) , ( F " ( A [,] B ) ) ) ) )
26 20 25 mpbid 
 |-  ( ph -> F Isom < , O ( ( A [,] B ) , ( F " ( A [,] B ) ) ) )
27 fnima 
 |-  ( F Fn ( A [,] B ) -> ( F " ( A [,] B ) ) = ran F )
28 isoeq5 
 |-  ( ( F " ( A [,] B ) ) = ran F -> ( F Isom < , O ( ( A [,] B ) , ( F " ( A [,] B ) ) ) <-> F Isom < , O ( ( A [,] B ) , ran F ) ) )
29 22 27 28 3syl 
 |-  ( ph -> ( F Isom < , O ( ( A [,] B ) , ( F " ( A [,] B ) ) ) <-> F Isom < , O ( ( A [,] B ) , ran F ) ) )
30 26 29 mpbid 
 |-  ( ph -> F Isom < , O ( ( A [,] B ) , ran F ) )