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 ) )