Theorem xrhmeo 22745

Description: The bijection from [ -u 1 , 1 ] to the extended reals is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.)

Hypotheses

Ref	Expression
xrhmeo.f	|- F = ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) )
xrhmeo.g	|- G = ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
xrhmeo.j	|- J = ( TopOpen ` ℂfld )
xrhmeo.k	|- K = (ordTop ` <_ )

Assertion

Ref	Expression
xrhmeo	|- ( G Isom < , < ( ( -u 1 [,] 1 ) , RR* ) /\ G e. ( ( J ↾t ( -u 1 [,] 1 ) ) Homeo (ordTop ` <_ ) ) )

Distinct variable groups:   x, y   y, F   x, J, y

Allowed substitution hints:   F( x)   G( x, y)   K( x, y)

Proof of Theorem xrhmeo

Dummy variables w v z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iccssxr 12256	. . . 4 |- ( -u 1 [,] 1 ) C_ RR*
2		xrltso 11974	. . . 4 |- < Or RR*
3		soss 5053	. . . 4 |- ( ( -u 1 [,] 1 ) C_ RR* -> ( < Or RR* -> < Or ( -u 1 [,] 1 ) ) )
4	1, 2, 3	mp2 9	. . 3 |- < Or ( -u 1 [,] 1 )
5		sopo 5052	. . . 4 |- ( < Or RR* -> < Po RR* )
6	2, 5	ax-mp 5	. . 3 |- < Po RR*
7		xrhmeo.g	. . . . 5 |- G = ( y e. ( -u 1 [,] 1 ) |-> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
8		iccssxr 12256	. . . . . . 7 |- ( 0 [,] +oo ) C_ RR*
9		neg1rr 11125	. . . . . . . . . . . 12 |- -u 1 e. RR
10		1re 10039	. . . . . . . . . . . 12 |- 1 e. RR
11	9, 10	elicc2i 12239	. . . . . . . . . . 11 |- ( y e. ( -u 1 [,] 1 ) <-> ( y e. RR /\ -u 1 <_ y /\ y <_ 1 ) )
12	11	simp1bi 1076	. . . . . . . . . 10 |- ( y e. ( -u 1 [,] 1 ) -> y e. RR )
13	12	adantr 481	. . . . . . . . 9 |- ( ( y e. ( -u 1 [,] 1 ) /\ 0 <_ y ) -> y e. RR )
14		simpr 477	. . . . . . . . 9 |- ( ( y e. ( -u 1 [,] 1 ) /\ 0 <_ y ) -> 0 <_ y )
15	11	simp3bi 1078	. . . . . . . . . 10 |- ( y e. ( -u 1 [,] 1 ) -> y <_ 1 )
16	15	adantr 481	. . . . . . . . 9 |- ( ( y e. ( -u 1 [,] 1 ) /\ 0 <_ y ) -> y <_ 1 )
17		0re 10040	. . . . . . . . . 10 |- 0 e. RR
18	17, 10	elicc2i 12239	. . . . . . . . 9 |- ( y e. ( 0 [,] 1 ) <-> ( y e. RR /\ 0 <_ y /\ y <_ 1 ) )
19	13, 14, 16, 18	syl3anbrc 1246	. . . . . . . 8 |- ( ( y e. ( -u 1 [,] 1 ) /\ 0 <_ y ) -> y e. ( 0 [,] 1 ) )
20		xrhmeo.f	. . . . . . . . . . . 12 |- F = ( x e. ( 0 [,] 1 ) |-> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) )
21	20	iccpnfcnv 22743	. . . . . . . . . . 11 |- ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) /\ `' F = ( v e. ( 0 [,] +oo ) |-> if ( v = +oo , 1 , ( v / ( 1 + v ) ) ) ) )
22	21	simpli 474	. . . . . . . . . 10 |- F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo )
23		f1of 6137	. . . . . . . . . 10 |- ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) -> F : ( 0 [,] 1 ) --> ( 0 [,] +oo ) )
24	22, 23	ax-mp 5	. . . . . . . . 9 |- F : ( 0 [,] 1 ) --> ( 0 [,] +oo )
25	24	ffvelrni 6358	. . . . . . . 8 |- ( y e. ( 0 [,] 1 ) -> ( F ` y ) e. ( 0 [,] +oo ) )
26	19, 25	syl 17	. . . . . . 7 |- ( ( y e. ( -u 1 [,] 1 ) /\ 0 <_ y ) -> ( F ` y ) e. ( 0 [,] +oo ) )
27	8, 26	sseldi 3601	. . . . . 6 |- ( ( y e. ( -u 1 [,] 1 ) /\ 0 <_ y ) -> ( F ` y ) e. RR* )
28	12	adantr 481	. . . . . . . . . . 11 |- ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> y e. RR )
29	28	renegcld 10457	. . . . . . . . . 10 |- ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> -u y e. RR )
30		letric 10137	. . . . . . . . . . . . 13 |- ( ( 0 e. RR /\ y e. RR ) -> ( 0 <_ y \/ y <_ 0 ) )
31	17, 12, 30	sylancr 695	. . . . . . . . . . . 12 |- ( y e. ( -u 1 [,] 1 ) -> ( 0 <_ y \/ y <_ 0 ) )
32	31	orcanai 952	. . . . . . . . . . 11 |- ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> y <_ 0 )
33	28	le0neg1d 10599	. . . . . . . . . . 11 |- ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> ( y <_ 0 <-> 0 <_ -u y ) )
34	32, 33	mpbid 222	. . . . . . . . . 10 |- ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> 0 <_ -u y )
35	11	simp2bi 1077	. . . . . . . . . . . 12 |- ( y e. ( -u 1 [,] 1 ) -> -u 1 <_ y )
36	35	adantr 481	. . . . . . . . . . 11 |- ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> -u 1 <_ y )
37		lenegcon1 10532	. . . . . . . . . . . 12 |- ( ( 1 e. RR /\ y e. RR ) -> ( -u 1 <_ y <-> -u y <_ 1 ) )
38	10, 28, 37	sylancr 695	. . . . . . . . . . 11 |- ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> ( -u 1 <_ y <-> -u y <_ 1 ) )
39	36, 38	mpbid 222	. . . . . . . . . 10 |- ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> -u y <_ 1 )
40	17, 10	elicc2i 12239	. . . . . . . . . 10 |- ( -u y e. ( 0 [,] 1 ) <-> ( -u y e. RR /\ 0 <_ -u y /\ -u y <_ 1 ) )
41	29, 34, 39, 40	syl3anbrc 1246	. . . . . . . . 9 |- ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> -u y e. ( 0 [,] 1 ) )
42	24	ffvelrni 6358	. . . . . . . . 9 |- ( -u y e. ( 0 [,] 1 ) -> ( F ` -u y ) e. ( 0 [,] +oo ) )
43	41, 42	syl 17	. . . . . . . 8 |- ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> ( F ` -u y ) e. ( 0 [,] +oo ) )
44	8, 43	sseldi 3601	. . . . . . 7 |- ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> ( F ` -u y ) e. RR* )
45	44	xnegcld 12130	. . . . . 6 |- ( ( y e. ( -u 1 [,] 1 ) /\ -. 0 <_ y ) -> -e ( F ` -u y ) e. RR* )
46	27, 45	ifclda 4120	. . . . 5 |- ( y e. ( -u 1 [,] 1 ) -> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) e. RR* )
47	7, 46	fmpti 6383	. . . 4 |- G : ( -u 1 [,] 1 ) --> RR*
48		frn 6053	. . . . . 6 |- ( G : ( -u 1 [,] 1 ) --> RR* -> ran G C_ RR* )
49	47, 48	ax-mp 5	. . . . 5 |- ran G C_ RR*
50		ssabral 3673	. . . . . . 7 |- ( RR* C_ { z | E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) } <-> A. z e. RR* E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
51		0le1 10551	. . . . . . . . . . . . 13 |- 0 <_ 1
52		le0neg2 10537	. . . . . . . . . . . . . 14 |- ( 1 e. RR -> ( 0 <_ 1 <-> -u 1 <_ 0 ) )
53	10, 52	ax-mp 5	. . . . . . . . . . . . 13 |- ( 0 <_ 1 <-> -u 1 <_ 0 )
54	51, 53	mpbi 220	. . . . . . . . . . . 12 |- -u 1 <_ 0
55		1le1 10655	. . . . . . . . . . . 12 |- 1 <_ 1
56		iccss 12241	. . . . . . . . . . . 12 |- ( ( ( -u 1 e. RR /\ 1 e. RR ) /\ ( -u 1 <_ 0 /\ 1 <_ 1 ) ) -> ( 0 [,] 1 ) C_ ( -u 1 [,] 1 ) )
57	9, 10, 54, 55, 56	mp4an 709	. . . . . . . . . . 11 |- ( 0 [,] 1 ) C_ ( -u 1 [,] 1 )
58		elxrge0 12281	. . . . . . . . . . . 12 |- ( z e. ( 0 [,] +oo ) <-> ( z e. RR* /\ 0 <_ z ) )
59		f1ocnv 6149	. . . . . . . . . . . . . 14 |- ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) -> `' F : ( 0 [,] +oo ) -1-1-onto-> ( 0 [,] 1 ) )
60		f1of 6137	. . . . . . . . . . . . . 14 |- ( `' F : ( 0 [,] +oo ) -1-1-onto-> ( 0 [,] 1 ) -> `' F : ( 0 [,] +oo ) --> ( 0 [,] 1 ) )
61	22, 59, 60	mp2b 10	. . . . . . . . . . . . 13 |- `' F : ( 0 [,] +oo ) --> ( 0 [,] 1 )
62	61	ffvelrni 6358	. . . . . . . . . . . 12 |- ( z e. ( 0 [,] +oo ) -> ( `' F ` z ) e. ( 0 [,] 1 ) )
63	58, 62	sylbir 225	. . . . . . . . . . 11 |- ( ( z e. RR* /\ 0 <_ z ) -> ( `' F ` z ) e. ( 0 [,] 1 ) )
64	57, 63	sseldi 3601	. . . . . . . . . 10 |- ( ( z e. RR* /\ 0 <_ z ) -> ( `' F ` z ) e. ( -u 1 [,] 1 ) )
65	17, 10	elicc2i 12239	. . . . . . . . . . . 12 |- ( ( `' F ` z ) e. ( 0 [,] 1 ) <-> ( ( `' F ` z ) e. RR /\ 0 <_ ( `' F ` z ) /\ ( `' F ` z ) <_ 1 ) )
66	65	simp2bi 1077	. . . . . . . . . . 11 |- ( ( `' F ` z ) e. ( 0 [,] 1 ) -> 0 <_ ( `' F ` z ) )
67	63, 66	syl 17	. . . . . . . . . 10 |- ( ( z e. RR* /\ 0 <_ z ) -> 0 <_ ( `' F ` z ) )
68	58	biimpri 218	. . . . . . . . . . . 12 |- ( ( z e. RR* /\ 0 <_ z ) -> z e. ( 0 [,] +oo ) )
69		f1ocnvfv2 6533	. . . . . . . . . . . 12 |- ( ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) /\ z e. ( 0 [,] +oo ) ) -> ( F ` ( `' F ` z ) ) = z )
70	22, 68, 69	sylancr 695	. . . . . . . . . . 11 |- ( ( z e. RR* /\ 0 <_ z ) -> ( F ` ( `' F ` z ) ) = z )
71	70	eqcomd 2628	. . . . . . . . . 10 |- ( ( z e. RR* /\ 0 <_ z ) -> z = ( F ` ( `' F ` z ) ) )
72		breq2 4657	. . . . . . . . . . . 12 |- ( y = ( `' F ` z ) -> ( 0 <_ y <-> 0 <_ ( `' F ` z ) ) )
73		fveq2 6191	. . . . . . . . . . . . 13 |- ( y = ( `' F ` z ) -> ( F ` y ) = ( F ` ( `' F ` z ) ) )
74	73	eqeq2d 2632	. . . . . . . . . . . 12 |- ( y = ( `' F ` z ) -> ( z = ( F ` y ) <-> z = ( F ` ( `' F ` z ) ) ) )
75	72, 74	anbi12d 747	. . . . . . . . . . 11 |- ( y = ( `' F ` z ) -> ( ( 0 <_ y /\ z = ( F ` y ) ) <-> ( 0 <_ ( `' F ` z ) /\ z = ( F ` ( `' F ` z ) ) ) ) )
76	75	rspcev 3309	. . . . . . . . . 10 |- ( ( ( `' F ` z ) e. ( -u 1 [,] 1 ) /\ ( 0 <_ ( `' F ` z ) /\ z = ( F ` ( `' F ` z ) ) ) ) -> E. y e. ( -u 1 [,] 1 ) ( 0 <_ y /\ z = ( F ` y ) ) )
77	64, 67, 71, 76	syl12anc 1324	. . . . . . . . 9 |- ( ( z e. RR* /\ 0 <_ z ) -> E. y e. ( -u 1 [,] 1 ) ( 0 <_ y /\ z = ( F ` y ) ) )
78		iftrue 4092	. . . . . . . . . . . 12 |- ( 0 <_ y -> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) = ( F ` y ) )
79	78	eqeq2d 2632	. . . . . . . . . . 11 |- ( 0 <_ y -> ( z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) <-> z = ( F ` y ) ) )
80	79	biimpar 502	. . . . . . . . . 10 |- ( ( 0 <_ y /\ z = ( F ` y ) ) -> z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
81	80	reximi 3011	. . . . . . . . 9 |- ( E. y e. ( -u 1 [,] 1 ) ( 0 <_ y /\ z = ( F ` y ) ) -> E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
82	77, 81	syl 17	. . . . . . . 8 |- ( ( z e. RR* /\ 0 <_ z ) -> E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
83		xnegcl 12044	. . . . . . . . . . . . . . . 16 |- ( z e. RR* -> -e z e. RR* )
84	83	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( z e. RR* /\ -. 0 <_ z ) -> -e z e. RR* )
85		0xr 10086	. . . . . . . . . . . . . . . . . . 19 |- 0 e. RR*
86		xrletri 11984	. . . . . . . . . . . . . . . . . . 19 |- ( ( 0 e. RR* /\ z e. RR* ) -> ( 0 <_ z \/ z <_ 0 ) )
87	85, 86	mpan 706	. . . . . . . . . . . . . . . . . 18 |- ( z e. RR* -> ( 0 <_ z \/ z <_ 0 ) )
88	87	ord 392	. . . . . . . . . . . . . . . . 17 |- ( z e. RR* -> ( -. 0 <_ z -> z <_ 0 ) )
89		xle0neg1 12052	. . . . . . . . . . . . . . . . 17 |- ( z e. RR* -> ( z <_ 0 <-> 0 <_ -e z ) )
90	88, 89	sylibd 229	. . . . . . . . . . . . . . . 16 |- ( z e. RR* -> ( -. 0 <_ z -> 0 <_ -e z ) )
91	90	imp 445	. . . . . . . . . . . . . . 15 |- ( ( z e. RR* /\ -. 0 <_ z ) -> 0 <_ -e z )
92		elxrge0 12281	. . . . . . . . . . . . . . 15 |- ( -e z e. ( 0 [,] +oo ) <-> ( -e z e. RR* /\ 0 <_ -e z ) )
93	84, 91, 92	sylanbrc 698	. . . . . . . . . . . . . 14 |- ( ( z e. RR* /\ -. 0 <_ z ) -> -e z e. ( 0 [,] +oo ) )
94	61	ffvelrni 6358	. . . . . . . . . . . . . 14 |- ( -e z e. ( 0 [,] +oo ) -> ( `' F ` -e z ) e. ( 0 [,] 1 ) )
95	93, 94	syl 17	. . . . . . . . . . . . 13 |- ( ( z e. RR* /\ -. 0 <_ z ) -> ( `' F ` -e z ) e. ( 0 [,] 1 ) )
96	57, 95	sseldi 3601	. . . . . . . . . . . 12 |- ( ( z e. RR* /\ -. 0 <_ z ) -> ( `' F ` -e z ) e. ( -u 1 [,] 1 ) )
97		iccssre 12255	. . . . . . . . . . . . . . 15 |- ( ( -u 1 e. RR /\ 1 e. RR ) -> ( -u 1 [,] 1 ) C_ RR )
98	9, 10, 97	mp2an 708	. . . . . . . . . . . . . 14 |- ( -u 1 [,] 1 ) C_ RR
99	98, 96	sseldi 3601	. . . . . . . . . . . . 13 |- ( ( z e. RR* /\ -. 0 <_ z ) -> ( `' F ` -e z ) e. RR )
100		iccneg 12293	. . . . . . . . . . . . . 14 |- ( ( -u 1 e. RR /\ 1 e. RR /\ ( `' F ` -e z ) e. RR ) -> ( ( `' F ` -e z ) e. ( -u 1 [,] 1 ) <-> -u ( `' F ` -e z ) e. ( -u 1 [,] -u -u 1 ) ) )
101	9, 10, 100	mp3an12 1414	. . . . . . . . . . . . 13 |- ( ( `' F ` -e z ) e. RR -> ( ( `' F ` -e z ) e. ( -u 1 [,] 1 ) <-> -u ( `' F ` -e z ) e. ( -u 1 [,] -u -u 1 ) ) )
102	99, 101	syl 17	. . . . . . . . . . . 12 |- ( ( z e. RR* /\ -. 0 <_ z ) -> ( ( `' F ` -e z ) e. ( -u 1 [,] 1 ) <-> -u ( `' F ` -e z ) e. ( -u 1 [,] -u -u 1 ) ) )
103	96, 102	mpbid 222	. . . . . . . . . . 11 |- ( ( z e. RR* /\ -. 0 <_ z ) -> -u ( `' F ` -e z ) e. ( -u 1 [,] -u -u 1 ) )
104		negneg1e1 11128	. . . . . . . . . . . 12 |- -u -u 1 = 1
105	104	oveq2i 6661	. . . . . . . . . . 11 |- ( -u 1 [,] -u -u 1 ) = ( -u 1 [,] 1 )
106	103, 105	syl6eleq 2711	. . . . . . . . . 10 |- ( ( z e. RR* /\ -. 0 <_ z ) -> -u ( `' F ` -e z ) e. ( -u 1 [,] 1 ) )
107		xle0neg2 12053	. . . . . . . . . . . . . . 15 |- ( z e. RR* -> ( 0 <_ z <-> -e z <_ 0 ) )
108	107	notbid 308	. . . . . . . . . . . . . 14 |- ( z e. RR* -> ( -. 0 <_ z <-> -. -e z <_ 0 ) )
109	108	biimpa 501	. . . . . . . . . . . . 13 |- ( ( z e. RR* /\ -. 0 <_ z ) -> -. -e z <_ 0 )
110		f1ocnvfv2 6533	. . . . . . . . . . . . . . 15 |- ( ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) /\ -e z e. ( 0 [,] +oo ) ) -> ( F ` ( `' F ` -e z ) ) = -e z )
111	22, 93, 110	sylancr 695	. . . . . . . . . . . . . 14 |- ( ( z e. RR* /\ -. 0 <_ z ) -> ( F ` ( `' F ` -e z ) ) = -e z )
112		0elunit 12290	. . . . . . . . . . . . . . . 16 |- 0 e. ( 0 [,] 1 )
113		ax-1ne0 10005	. . . . . . . . . . . . . . . . . . . . 21 |- 1 =/= 0
114		neeq2 2857	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = 0 -> ( 1 =/= x <-> 1 =/= 0 ) )
115	113, 114	mpbiri 248	. . . . . . . . . . . . . . . . . . . 20 |- ( x = 0 -> 1 =/= x )
116	115	necomd 2849	. . . . . . . . . . . . . . . . . . 19 |- ( x = 0 -> x =/= 1 )
117		ifnefalse 4098	. . . . . . . . . . . . . . . . . . 19 |- ( x =/= 1 -> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) = ( x / ( 1 - x ) ) )
118	116, 117	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( x = 0 -> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) = ( x / ( 1 - x ) ) )
119		id 22	. . . . . . . . . . . . . . . . . . . 20 |- ( x = 0 -> x = 0 )
120		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = 0 -> ( 1 - x ) = ( 1 - 0 ) )
121		1m0e1 11131	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 - 0 ) = 1
122	120, 121	syl6eq 2672	. . . . . . . . . . . . . . . . . . . 20 |- ( x = 0 -> ( 1 - x ) = 1 )
123	119, 122	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19 |- ( x = 0 -> ( x / ( 1 - x ) ) = ( 0 / 1 ) )
124		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . 20 |- 1 e. CC
125	124, 113	div0i 10759	. . . . . . . . . . . . . . . . . . 19 |- ( 0 / 1 ) = 0
126	123, 125	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 |- ( x = 0 -> ( x / ( 1 - x ) ) = 0 )
127	118, 126	eqtrd 2656	. . . . . . . . . . . . . . . . 17 |- ( x = 0 -> if ( x = 1 , +oo , ( x / ( 1 - x ) ) ) = 0 )
128		c0ex 10034	. . . . . . . . . . . . . . . . 17 |- 0 e. _V
129	127, 20, 128	fvmpt 6282	. . . . . . . . . . . . . . . 16 |- ( 0 e. ( 0 [,] 1 ) -> ( F ` 0 ) = 0 )
130	112, 129	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( F ` 0 ) = 0
131	130	a1i 11	. . . . . . . . . . . . . 14 |- ( ( z e. RR* /\ -. 0 <_ z ) -> ( F ` 0 ) = 0 )
132	111, 131	breq12d 4666	. . . . . . . . . . . . 13 |- ( ( z e. RR* /\ -. 0 <_ z ) -> ( ( F ` ( `' F ` -e z ) ) <_ ( F ` 0 ) <-> -e z <_ 0 ) )
133	109, 132	mtbird 315	. . . . . . . . . . . 12 |- ( ( z e. RR* /\ -. 0 <_ z ) -> -. ( F ` ( `' F ` -e z ) ) <_ ( F ` 0 ) )
134		eqid 2622	. . . . . . . . . . . . . . . 16 |- ( (ordTop ` <_ ) ↾t ( 0 [,] +oo ) ) = ( (ordTop ` <_ ) ↾t ( 0 [,] +oo ) )
135	20, 134	iccpnfhmeo 22744	. . . . . . . . . . . . . . 15 |- ( F Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) /\ F e. ( II Homeo ( (ordTop ` <_ ) ↾t ( 0 [,] +oo ) ) ) )
136	135	simpli 474	. . . . . . . . . . . . . 14 |- F Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) )
137		iccssxr 12256	. . . . . . . . . . . . . . 15 |- ( 0 [,] 1 ) C_ RR*
138	137, 8	pm3.2i 471	. . . . . . . . . . . . . 14 |- ( ( 0 [,] 1 ) C_ RR* /\ ( 0 [,] +oo ) C_ RR* )
139		leisorel 13244	. . . . . . . . . . . . . 14 |- ( ( F Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) /\ ( ( 0 [,] 1 ) C_ RR* /\ ( 0 [,] +oo ) C_ RR* ) /\ ( ( `' F ` -e z ) e. ( 0 [,] 1 ) /\ 0 e. ( 0 [,] 1 ) ) ) -> ( ( `' F ` -e z ) <_ 0 <-> ( F ` ( `' F ` -e z ) ) <_ ( F ` 0 ) ) )
140	136, 138, 139	mp3an12 1414	. . . . . . . . . . . . 13 |- ( ( ( `' F ` -e z ) e. ( 0 [,] 1 ) /\ 0 e. ( 0 [,] 1 ) ) -> ( ( `' F ` -e z ) <_ 0 <-> ( F ` ( `' F ` -e z ) ) <_ ( F ` 0 ) ) )
141	95, 112, 140	sylancl 694	. . . . . . . . . . . 12 |- ( ( z e. RR* /\ -. 0 <_ z ) -> ( ( `' F ` -e z ) <_ 0 <-> ( F ` ( `' F ` -e z ) ) <_ ( F ` 0 ) ) )
142	133, 141	mtbird 315	. . . . . . . . . . 11 |- ( ( z e. RR* /\ -. 0 <_ z ) -> -. ( `' F ` -e z ) <_ 0 )
143	99	le0neg1d 10599	. . . . . . . . . . 11 |- ( ( z e. RR* /\ -. 0 <_ z ) -> ( ( `' F ` -e z ) <_ 0 <-> 0 <_ -u ( `' F ` -e z ) ) )
144	142, 143	mtbid 314	. . . . . . . . . 10 |- ( ( z e. RR* /\ -. 0 <_ z ) -> -. 0 <_ -u ( `' F ` -e z ) )
145		unitssre 12319	. . . . . . . . . . . . . . . . 17 |- ( 0 [,] 1 ) C_ RR
146	145, 95	sseldi 3601	. . . . . . . . . . . . . . . 16 |- ( ( z e. RR* /\ -. 0 <_ z ) -> ( `' F ` -e z ) e. RR )
147	146	recnd 10068	. . . . . . . . . . . . . . 15 |- ( ( z e. RR* /\ -. 0 <_ z ) -> ( `' F ` -e z ) e. CC )
148	147	negnegd 10383	. . . . . . . . . . . . . 14 |- ( ( z e. RR* /\ -. 0 <_ z ) -> -u -u ( `' F ` -e z ) = ( `' F ` -e z ) )
149	148	fveq2d 6195	. . . . . . . . . . . . 13 |- ( ( z e. RR* /\ -. 0 <_ z ) -> ( F ` -u -u ( `' F ` -e z ) ) = ( F ` ( `' F ` -e z ) ) )
150	149, 111	eqtrd 2656	. . . . . . . . . . . 12 |- ( ( z e. RR* /\ -. 0 <_ z ) -> ( F ` -u -u ( `' F ` -e z ) ) = -e z )
151		xnegeq 12038	. . . . . . . . . . . 12 |- ( ( F ` -u -u ( `' F ` -e z ) ) = -e z -> -e ( F ` -u -u ( `' F ` -e z ) ) = -e -e z )
152	150, 151	syl 17	. . . . . . . . . . 11 |- ( ( z e. RR* /\ -. 0 <_ z ) -> -e ( F ` -u -u ( `' F ` -e z ) ) = -e -e z )
153		xnegneg 12045	. . . . . . . . . . . 12 |- ( z e. RR* -> -e -e z = z )
154	153	adantr 481	. . . . . . . . . . 11 |- ( ( z e. RR* /\ -. 0 <_ z ) -> -e -e z = z )
155	152, 154	eqtr2d 2657	. . . . . . . . . 10 |- ( ( z e. RR* /\ -. 0 <_ z ) -> z = -e ( F ` -u -u ( `' F ` -e z ) ) )
156		breq2 4657	. . . . . . . . . . . . 13 |- ( y = -u ( `' F ` -e z ) -> ( 0 <_ y <-> 0 <_ -u ( `' F ` -e z ) ) )
157	156	notbid 308	. . . . . . . . . . . 12 |- ( y = -u ( `' F ` -e z ) -> ( -. 0 <_ y <-> -. 0 <_ -u ( `' F ` -e z ) ) )
158		negeq 10273	. . . . . . . . . . . . . . 15 |- ( y = -u ( `' F ` -e z ) -> -u y = -u -u ( `' F ` -e z ) )
159	158	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( y = -u ( `' F ` -e z ) -> ( F ` -u y ) = ( F ` -u -u ( `' F ` -e z ) ) )
160		xnegeq 12038	. . . . . . . . . . . . . 14 |- ( ( F ` -u y ) = ( F ` -u -u ( `' F ` -e z ) ) -> -e ( F ` -u y ) = -e ( F ` -u -u ( `' F ` -e z ) ) )
161	159, 160	syl 17	. . . . . . . . . . . . 13 |- ( y = -u ( `' F ` -e z ) -> -e ( F ` -u y ) = -e ( F ` -u -u ( `' F ` -e z ) ) )
162	161	eqeq2d 2632	. . . . . . . . . . . 12 |- ( y = -u ( `' F ` -e z ) -> ( z = -e ( F ` -u y ) <-> z = -e ( F ` -u -u ( `' F ` -e z ) ) ) )
163	157, 162	anbi12d 747	. . . . . . . . . . 11 |- ( y = -u ( `' F ` -e z ) -> ( ( -. 0 <_ y /\ z = -e ( F ` -u y ) ) <-> ( -. 0 <_ -u ( `' F ` -e z ) /\ z = -e ( F ` -u -u ( `' F ` -e z ) ) ) ) )
164	163	rspcev 3309	. . . . . . . . . 10 |- ( ( -u ( `' F ` -e z ) e. ( -u 1 [,] 1 ) /\ ( -. 0 <_ -u ( `' F ` -e z ) /\ z = -e ( F ` -u -u ( `' F ` -e z ) ) ) ) -> E. y e. ( -u 1 [,] 1 ) ( -. 0 <_ y /\ z = -e ( F ` -u y ) ) )
165	106, 144, 155, 164	syl12anc 1324	. . . . . . . . 9 |- ( ( z e. RR* /\ -. 0 <_ z ) -> E. y e. ( -u 1 [,] 1 ) ( -. 0 <_ y /\ z = -e ( F ` -u y ) ) )
166		iffalse 4095	. . . . . . . . . . . 12 |- ( -. 0 <_ y -> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) = -e ( F ` -u y ) )
167	166	eqeq2d 2632	. . . . . . . . . . 11 |- ( -. 0 <_ y -> ( z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) <-> z = -e ( F ` -u y ) ) )
168	167	biimpar 502	. . . . . . . . . 10 |- ( ( -. 0 <_ y /\ z = -e ( F ` -u y ) ) -> z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
169	168	reximi 3011	. . . . . . . . 9 |- ( E. y e. ( -u 1 [,] 1 ) ( -. 0 <_ y /\ z = -e ( F ` -u y ) ) -> E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
170	165, 169	syl 17	. . . . . . . 8 |- ( ( z e. RR* /\ -. 0 <_ z ) -> E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
171	82, 170	pm2.61dan 832	. . . . . . 7 |- ( z e. RR* -> E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) )
172	50, 171	mprgbir 2927	. . . . . 6 |- RR* C_ { z | E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) }
173	7	rnmpt 5371	. . . . . 6 |- ran G = { z | E. y e. ( -u 1 [,] 1 ) z = if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) }
174	172, 173	sseqtr4i 3638	. . . . 5 |- RR* C_ ran G
175	49, 174	eqssi 3619	. . . 4 |- ran G = RR*
176		dffo2 6119	. . . 4 |- ( G : ( -u 1 [,] 1 ) -onto-> RR* <-> ( G : ( -u 1 [,] 1 ) --> RR* /\ ran G = RR* ) )
177	47, 175, 176	mpbir2an 955	. . 3 |- G : ( -u 1 [,] 1 ) -onto-> RR*
178		breq1 4656	. . . . . . 7 |- ( ( F ` z ) = if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) -> ( ( F ` z ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) <-> if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) ) )
179		breq1 4656	. . . . . . 7 |- ( -e ( F ` -u z ) = if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) -> ( -e ( F ` -u z ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) <-> if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) ) )
180		simpl3 1066	. . . . . . . . 9 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> z < w )
181		simpl1 1064	. . . . . . . . . . 11 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> z e. ( -u 1 [,] 1 ) )
182		simpr 477	. . . . . . . . . . 11 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> 0 <_ z )
183		breq2 4657	. . . . . . . . . . . . 13 |- ( y = z -> ( 0 <_ y <-> 0 <_ z ) )
184		eleq1 2689	. . . . . . . . . . . . 13 |- ( y = z -> ( y e. ( 0 [,] 1 ) <-> z e. ( 0 [,] 1 ) ) )
185	183, 184	imbi12d 334	. . . . . . . . . . . 12 |- ( y = z -> ( ( 0 <_ y -> y e. ( 0 [,] 1 ) ) <-> ( 0 <_ z -> z e. ( 0 [,] 1 ) ) ) )
186	19	ex 450	. . . . . . . . . . . 12 |- ( y e. ( -u 1 [,] 1 ) -> ( 0 <_ y -> y e. ( 0 [,] 1 ) ) )
187	185, 186	vtoclga 3272	. . . . . . . . . . 11 |- ( z e. ( -u 1 [,] 1 ) -> ( 0 <_ z -> z e. ( 0 [,] 1 ) ) )
188	181, 182, 187	sylc 65	. . . . . . . . . 10 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> z e. ( 0 [,] 1 ) )
189		simpl2 1065	. . . . . . . . . . 11 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> w e. ( -u 1 [,] 1 ) )
190	17	a1i 11	. . . . . . . . . . . 12 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> 0 e. RR )
191	98, 181	sseldi 3601	. . . . . . . . . . . 12 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> z e. RR )
192	98, 189	sseldi 3601	. . . . . . . . . . . 12 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> w e. RR )
193	191, 192, 180	ltled 10185	. . . . . . . . . . . 12 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> z <_ w )
194	190, 191, 192, 182, 193	letrd 10194	. . . . . . . . . . 11 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> 0 <_ w )
195		breq2 4657	. . . . . . . . . . . . 13 |- ( y = w -> ( 0 <_ y <-> 0 <_ w ) )
196		eleq1 2689	. . . . . . . . . . . . 13 |- ( y = w -> ( y e. ( 0 [,] 1 ) <-> w e. ( 0 [,] 1 ) ) )
197	195, 196	imbi12d 334	. . . . . . . . . . . 12 |- ( y = w -> ( ( 0 <_ y -> y e. ( 0 [,] 1 ) ) <-> ( 0 <_ w -> w e. ( 0 [,] 1 ) ) ) )
198	197, 186	vtoclga 3272	. . . . . . . . . . 11 |- ( w e. ( -u 1 [,] 1 ) -> ( 0 <_ w -> w e. ( 0 [,] 1 ) ) )
199	189, 194, 198	sylc 65	. . . . . . . . . 10 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> w e. ( 0 [,] 1 ) )
200		isorel 6576	. . . . . . . . . . 11 |- ( ( F Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) /\ ( z e. ( 0 [,] 1 ) /\ w e. ( 0 [,] 1 ) ) ) -> ( z < w <-> ( F ` z ) < ( F ` w ) ) )
201	136, 200	mpan 706	. . . . . . . . . 10 |- ( ( z e. ( 0 [,] 1 ) /\ w e. ( 0 [,] 1 ) ) -> ( z < w <-> ( F ` z ) < ( F ` w ) ) )
202	188, 199, 201	syl2anc 693	. . . . . . . . 9 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> ( z < w <-> ( F ` z ) < ( F ` w ) ) )
203	180, 202	mpbid 222	. . . . . . . 8 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> ( F ` z ) < ( F ` w ) )
204	194	iftrued 4094	. . . . . . . 8 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) = ( F ` w ) )
205	203, 204	breqtrrd 4681	. . . . . . 7 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ 0 <_ z ) -> ( F ` z ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) )
206		breq2 4657	. . . . . . . 8 |- ( ( F ` w ) = if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) -> ( -e ( F ` -u z ) < ( F ` w ) <-> -e ( F ` -u z ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) ) )
207		breq2 4657	. . . . . . . 8 |- ( -e ( F ` -u w ) = if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) -> ( -e ( F ` -u z ) < -e ( F ` -u w ) <-> -e ( F ` -u z ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) ) )
208		simpl1 1064	. . . . . . . . . . . . . 14 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) -> z e. ( -u 1 [,] 1 ) )
209		simpr 477	. . . . . . . . . . . . . 14 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) -> -. 0 <_ z )
210	183	notbid 308	. . . . . . . . . . . . . . . 16 |- ( y = z -> ( -. 0 <_ y <-> -. 0 <_ z ) )
211		negeq 10273	. . . . . . . . . . . . . . . . 17 |- ( y = z -> -u y = -u z )
212	211	eleq1d 2686	. . . . . . . . . . . . . . . 16 |- ( y = z -> ( -u y e. ( 0 [,] 1 ) <-> -u z e. ( 0 [,] 1 ) ) )
213	210, 212	imbi12d 334	. . . . . . . . . . . . . . 15 |- ( y = z -> ( ( -. 0 <_ y -> -u y e. ( 0 [,] 1 ) ) <-> ( -. 0 <_ z -> -u z e. ( 0 [,] 1 ) ) ) )
214	41	ex 450	. . . . . . . . . . . . . . 15 |- ( y e. ( -u 1 [,] 1 ) -> ( -. 0 <_ y -> -u y e. ( 0 [,] 1 ) ) )
215	213, 214	vtoclga 3272	. . . . . . . . . . . . . 14 |- ( z e. ( -u 1 [,] 1 ) -> ( -. 0 <_ z -> -u z e. ( 0 [,] 1 ) ) )
216	208, 209, 215	sylc 65	. . . . . . . . . . . . 13 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) -> -u z e. ( 0 [,] 1 ) )
217	216	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> -u z e. ( 0 [,] 1 ) )
218	24	ffvelrni 6358	. . . . . . . . . . . 12 |- ( -u z e. ( 0 [,] 1 ) -> ( F ` -u z ) e. ( 0 [,] +oo ) )
219	217, 218	syl 17	. . . . . . . . . . 11 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( F ` -u z ) e. ( 0 [,] +oo ) )
220	8, 219	sseldi 3601	. . . . . . . . . 10 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( F ` -u z ) e. RR* )
221	220	xnegcld 12130	. . . . . . . . 9 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> -e ( F ` -u z ) e. RR* )
222	85	a1i 11	. . . . . . . . 9 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> 0 e. RR* )
223		simpll2 1101	. . . . . . . . . . . 12 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> w e. ( -u 1 [,] 1 ) )
224		simpr 477	. . . . . . . . . . . 12 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> 0 <_ w )
225	223, 224, 198	sylc 65	. . . . . . . . . . 11 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> w e. ( 0 [,] 1 ) )
226	24	ffvelrni 6358	. . . . . . . . . . 11 |- ( w e. ( 0 [,] 1 ) -> ( F ` w ) e. ( 0 [,] +oo ) )
227	225, 226	syl 17	. . . . . . . . . 10 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( F ` w ) e. ( 0 [,] +oo ) )
228	8, 227	sseldi 3601	. . . . . . . . 9 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( F ` w ) e. RR* )
229	209	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> -. 0 <_ z )
230		simpll1 1100	. . . . . . . . . . . . . . . 16 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> z e. ( -u 1 [,] 1 ) )
231	98, 230	sseldi 3601	. . . . . . . . . . . . . . 15 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> z e. RR )
232		ltnle 10117	. . . . . . . . . . . . . . 15 |- ( ( z e. RR /\ 0 e. RR ) -> ( z < 0 <-> -. 0 <_ z ) )
233	231, 17, 232	sylancl 694	. . . . . . . . . . . . . 14 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( z < 0 <-> -. 0 <_ z ) )
234	229, 233	mpbird 247	. . . . . . . . . . . . 13 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> z < 0 )
235	231	lt0neg1d 10597	. . . . . . . . . . . . 13 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( z < 0 <-> 0 < -u z ) )
236	234, 235	mpbid 222	. . . . . . . . . . . 12 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> 0 < -u z )
237		isorel 6576	. . . . . . . . . . . . . 14 |- ( ( F Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) /\ ( 0 e. ( 0 [,] 1 ) /\ -u z e. ( 0 [,] 1 ) ) ) -> ( 0 < -u z <-> ( F ` 0 ) < ( F ` -u z ) ) )
238	136, 237	mpan 706	. . . . . . . . . . . . 13 |- ( ( 0 e. ( 0 [,] 1 ) /\ -u z e. ( 0 [,] 1 ) ) -> ( 0 < -u z <-> ( F ` 0 ) < ( F ` -u z ) ) )
239	112, 217, 238	sylancr 695	. . . . . . . . . . . 12 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( 0 < -u z <-> ( F ` 0 ) < ( F ` -u z ) ) )
240	236, 239	mpbid 222	. . . . . . . . . . 11 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( F ` 0 ) < ( F ` -u z ) )
241	130, 240	syl5eqbrr 4689	. . . . . . . . . 10 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> 0 < ( F ` -u z ) )
242		xlt0neg2 12051	. . . . . . . . . . 11 |- ( ( F ` -u z ) e. RR* -> ( 0 < ( F ` -u z ) <-> -e ( F ` -u z ) < 0 ) )
243	220, 242	syl 17	. . . . . . . . . 10 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> ( 0 < ( F ` -u z ) <-> -e ( F ` -u z ) < 0 ) )
244	241, 243	mpbid 222	. . . . . . . . 9 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> -e ( F ` -u z ) < 0 )
245		elxrge0 12281	. . . . . . . . . . 11 |- ( ( F ` w ) e. ( 0 [,] +oo ) <-> ( ( F ` w ) e. RR* /\ 0 <_ ( F ` w ) ) )
246	245	simprbi 480	. . . . . . . . . 10 |- ( ( F ` w ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` w ) )
247	227, 246	syl 17	. . . . . . . . 9 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> 0 <_ ( F ` w ) )
248	221, 222, 228, 244, 247	xrltletrd 11992	. . . . . . . 8 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ 0 <_ w ) -> -e ( F ` -u z ) < ( F ` w ) )
249		simpll3 1102	. . . . . . . . . . 11 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> z < w )
250		simpll1 1100	. . . . . . . . . . . . 13 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> z e. ( -u 1 [,] 1 ) )
251	98, 250	sseldi 3601	. . . . . . . . . . . 12 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> z e. RR )
252		simpll2 1101	. . . . . . . . . . . . 13 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> w e. ( -u 1 [,] 1 ) )
253	98, 252	sseldi 3601	. . . . . . . . . . . 12 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> w e. RR )
254	251, 253	ltnegd 10605	. . . . . . . . . . 11 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( z < w <-> -u w < -u z ) )
255	249, 254	mpbid 222	. . . . . . . . . 10 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> -u w < -u z )
256		simpr 477	. . . . . . . . . . . 12 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> -. 0 <_ w )
257	195	notbid 308	. . . . . . . . . . . . . 14 |- ( y = w -> ( -. 0 <_ y <-> -. 0 <_ w ) )
258		negeq 10273	. . . . . . . . . . . . . . 15 |- ( y = w -> -u y = -u w )
259	258	eleq1d 2686	. . . . . . . . . . . . . 14 |- ( y = w -> ( -u y e. ( 0 [,] 1 ) <-> -u w e. ( 0 [,] 1 ) ) )
260	257, 259	imbi12d 334	. . . . . . . . . . . . 13 |- ( y = w -> ( ( -. 0 <_ y -> -u y e. ( 0 [,] 1 ) ) <-> ( -. 0 <_ w -> -u w e. ( 0 [,] 1 ) ) ) )
261	260, 214	vtoclga 3272	. . . . . . . . . . . 12 |- ( w e. ( -u 1 [,] 1 ) -> ( -. 0 <_ w -> -u w e. ( 0 [,] 1 ) ) )
262	252, 256, 261	sylc 65	. . . . . . . . . . 11 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> -u w e. ( 0 [,] 1 ) )
263	216	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> -u z e. ( 0 [,] 1 ) )
264		isorel 6576	. . . . . . . . . . . 12 |- ( ( F Isom < , < ( ( 0 [,] 1 ) , ( 0 [,] +oo ) ) /\ ( -u w e. ( 0 [,] 1 ) /\ -u z e. ( 0 [,] 1 ) ) ) -> ( -u w < -u z <-> ( F ` -u w ) < ( F ` -u z ) ) )
265	136, 264	mpan 706	. . . . . . . . . . 11 |- ( ( -u w e. ( 0 [,] 1 ) /\ -u z e. ( 0 [,] 1 ) ) -> ( -u w < -u z <-> ( F ` -u w ) < ( F ` -u z ) ) )
266	262, 263, 265	syl2anc 693	. . . . . . . . . 10 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( -u w < -u z <-> ( F ` -u w ) < ( F ` -u z ) ) )
267	255, 266	mpbid 222	. . . . . . . . 9 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( F ` -u w ) < ( F ` -u z ) )
268	24	ffvelrni 6358	. . . . . . . . . . . 12 |- ( -u w e. ( 0 [,] 1 ) -> ( F ` -u w ) e. ( 0 [,] +oo ) )
269	262, 268	syl 17	. . . . . . . . . . 11 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( F ` -u w ) e. ( 0 [,] +oo ) )
270	8, 269	sseldi 3601	. . . . . . . . . 10 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( F ` -u w ) e. RR* )
271	263, 218	syl 17	. . . . . . . . . . 11 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( F ` -u z ) e. ( 0 [,] +oo ) )
272	8, 271	sseldi 3601	. . . . . . . . . 10 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( F ` -u z ) e. RR* )
273		xltneg 12048	. . . . . . . . . 10 |- ( ( ( F ` -u w ) e. RR* /\ ( F ` -u z ) e. RR* ) -> ( ( F ` -u w ) < ( F ` -u z ) <-> -e ( F ` -u z ) < -e ( F ` -u w ) ) )
274	270, 272, 273	syl2anc 693	. . . . . . . . 9 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> ( ( F ` -u w ) < ( F ` -u z ) <-> -e ( F ` -u z ) < -e ( F ` -u w ) ) )
275	267, 274	mpbid 222	. . . . . . . 8 |- ( ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) /\ -. 0 <_ w ) -> -e ( F ` -u z ) < -e ( F ` -u w ) )
276	206, 207, 248, 275	ifbothda 4123	. . . . . . 7 |- ( ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) /\ -. 0 <_ z ) -> -e ( F ` -u z ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) )
277	178, 179, 205, 276	ifbothda 4123	. . . . . 6 |- ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) /\ z < w ) -> if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) )
278	277	3expia 1267	. . . . 5 |- ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) ) -> ( z < w -> if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) ) )
279		fveq2 6191	. . . . . . . 8 |- ( y = z -> ( F ` y ) = ( F ` z ) )
280	211	fveq2d 6195	. . . . . . . . 9 |- ( y = z -> ( F ` -u y ) = ( F ` -u z ) )
281		xnegeq 12038	. . . . . . . . 9 |- ( ( F ` -u y ) = ( F ` -u z ) -> -e ( F ` -u y ) = -e ( F ` -u z ) )
282	280, 281	syl 17	. . . . . . . 8 |- ( y = z -> -e ( F ` -u y ) = -e ( F ` -u z ) )
283	183, 279, 282	ifbieq12d 4113	. . . . . . 7 |- ( y = z -> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) = if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) )
284		fvex 6201	. . . . . . . 8 |- ( F ` z ) e. _V
285		xnegex 12039	. . . . . . . 8 |- -e ( F ` -u z ) e. _V
286	284, 285	ifex 4156	. . . . . . 7 |- if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) e. _V
287	283, 7, 286	fvmpt 6282	. . . . . 6 |- ( z e. ( -u 1 [,] 1 ) -> ( G ` z ) = if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) )
288		fveq2 6191	. . . . . . . 8 |- ( y = w -> ( F ` y ) = ( F ` w ) )
289	258	fveq2d 6195	. . . . . . . . 9 |- ( y = w -> ( F ` -u y ) = ( F ` -u w ) )
290		xnegeq 12038	. . . . . . . . 9 |- ( ( F ` -u y ) = ( F ` -u w ) -> -e ( F ` -u y ) = -e ( F ` -u w ) )
291	289, 290	syl 17	. . . . . . . 8 |- ( y = w -> -e ( F ` -u y ) = -e ( F ` -u w ) )
292	195, 288, 291	ifbieq12d 4113	. . . . . . 7 |- ( y = w -> if ( 0 <_ y , ( F ` y ) , -e ( F ` -u y ) ) = if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) )
293		fvex 6201	. . . . . . . 8 |- ( F ` w ) e. _V
294		xnegex 12039	. . . . . . . 8 |- -e ( F ` -u w ) e. _V
295	293, 294	ifex 4156	. . . . . . 7 |- if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) e. _V
296	292, 7, 295	fvmpt 6282	. . . . . 6 |- ( w e. ( -u 1 [,] 1 ) -> ( G ` w ) = if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) )
297	287, 296	breqan12d 4669	. . . . 5 |- ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) ) -> ( ( G ` z ) < ( G ` w ) <-> if ( 0 <_ z , ( F ` z ) , -e ( F ` -u z ) ) < if ( 0 <_ w , ( F ` w ) , -e ( F ` -u w ) ) ) )
298	278, 297	sylibrd 249	. . . 4 |- ( ( z e. ( -u 1 [,] 1 ) /\ w e. ( -u 1 [,] 1 ) ) -> ( z < w -> ( G ` z ) < ( G ` w ) ) )
299	298	rgen2a 2977	. . 3 |- A. z e. ( -u 1 [,] 1 ) A. w e. ( -u 1 [,] 1 ) ( z < w -> ( G ` z ) < ( G ` w ) )
300		soisoi 6578	. . 3 |- ( ( ( < Or ( -u 1 [,] 1 ) /\ < Po RR* ) /\ ( G : ( -u 1 [,] 1 ) -onto-> RR* /\ A. z e. ( -u 1 [,] 1 ) A. w e. ( -u 1 [,] 1 ) ( z < w -> ( G ` z ) < ( G ` w ) ) ) ) -> G Isom < , < ( ( -u 1 [,] 1 ) , RR* ) )
301	4, 6, 177, 299, 300	mp4an 709	. 2 |- G Isom < , < ( ( -u 1 [,] 1 ) , RR* )
302		letsr 17227	. . . . . 6 |- <_ e. TosetRel
303	302	elexi 3213	. . . . 5 |- <_ e. _V
304	303	inex1 4799	. . . 4 |- ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) e. _V
305		ssid 3624	. . . . . . 7 |- RR* C_ RR*
306		leiso 13243	. . . . . . 7 |- ( ( ( -u 1 [,] 1 ) C_ RR* /\ RR* C_ RR* ) -> ( G Isom < , < ( ( -u 1 [,] 1 ) , RR* ) <-> G Isom <_ , <_ ( ( -u 1 [,] 1 ) , RR* ) ) )
307	1, 305, 306	mp2an 708	. . . . . 6 |- ( G Isom < , < ( ( -u 1 [,] 1 ) , RR* ) <-> G Isom <_ , <_ ( ( -u 1 [,] 1 ) , RR* ) )
308	301, 307	mpbi 220	. . . . 5 |- G Isom <_ , <_ ( ( -u 1 [,] 1 ) , RR* )
309		isores1 6584	. . . . 5 |- ( G Isom <_ , <_ ( ( -u 1 [,] 1 ) , RR* ) <-> G Isom ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) , <_ ( ( -u 1 [,] 1 ) , RR* ) )
310	308, 309	mpbi 220	. . . 4 |- G Isom ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) , <_ ( ( -u 1 [,] 1 ) , RR* )
311		tsrps 17221	. . . . . . . 8 |- ( <_ e. TosetRel -> <_ e. PosetRel )
312	302, 311	ax-mp 5	. . . . . . 7 |- <_ e. PosetRel
313		ledm 17224	. . . . . . . 8 |- RR* = dom <_
314	313	psssdm 17216	. . . . . . 7 |- ( ( <_ e. PosetRel /\ ( -u 1 [,] 1 ) C_ RR* ) -> dom ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) = ( -u 1 [,] 1 ) )
315	312, 1, 314	mp2an 708	. . . . . 6 |- dom ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) = ( -u 1 [,] 1 )
316	315	eqcomi 2631	. . . . 5 |- ( -u 1 [,] 1 ) = dom ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) )
317	316, 313	ordthmeo 21605	. . . 4 |- ( ( ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) e. _V /\ <_ e. TosetRel /\ G Isom ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) , <_ ( ( -u 1 [,] 1 ) , RR* ) ) -> G e. ( (ordTop ` ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) ) Homeo (ordTop ` <_ ) ) )
318	304, 302, 310, 317	mp3an 1424	. . 3 |- G e. ( (ordTop ` ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) ) Homeo (ordTop ` <_ ) )
319		xrhmeo.j	. . . . . . 7 |- J = ( TopOpen ` ℂfld )
320		eqid 2622	. . . . . . 7 |- (ordTop ` <_ ) = (ordTop ` <_ )
321	319, 320	xrrest2 22611	. . . . . 6 |- ( ( -u 1 [,] 1 ) C_ RR -> ( J ↾t ( -u 1 [,] 1 ) ) = ( (ordTop ` <_ ) ↾t ( -u 1 [,] 1 ) ) )
322	98, 321	ax-mp 5	. . . . 5 |- ( J ↾t ( -u 1 [,] 1 ) ) = ( (ordTop ` <_ ) ↾t ( -u 1 [,] 1 ) )
323		ordtresticc 21027	. . . . 5 |- ( (ordTop ` <_ ) ↾t ( -u 1 [,] 1 ) ) = (ordTop ` ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) )
324	322, 323	eqtri 2644	. . . 4 |- ( J ↾t ( -u 1 [,] 1 ) ) = (ordTop ` ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) )
325	324	oveq1i 6660	. . 3 |- ( ( J ↾t ( -u 1 [,] 1 ) ) Homeo (ordTop ` <_ ) ) = ( (ordTop ` ( <_ i^i ( ( -u 1 [,] 1 ) X. ( -u 1 [,] 1 ) ) ) ) Homeo (ordTop ` <_ ) )
326	318, 325	eleqtrri 2700	. 2 |- G e. ( ( J ↾t ( -u 1 [,] 1 ) ) Homeo (ordTop ` <_ ) )
327	301, 326	pm3.2i 471	1 |- ( G Isom < , < ( ( -u 1 [,] 1 ) , RR* ) /\ G e. ( ( J ↾t ( -u 1 [,] 1 ) ) Homeo (ordTop ` <_ ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   i^i cin 3573   C_ wss 3574   ifcif 4086   class class class wbr 4653   |-> cmpt 4729   Po wpo 5033   Or wor 5034   X. cxp 5112   `'ccnv 5113   dom cdm 5114   ran crn 5115   -->wf 5884   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888   Isom wiso 5889  (class class class)co 6650   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   +oocpnf 10071   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   -ucneg 10267   / cdiv 10684   -ecxne 11943   [,]cicc 12178   ↾_t crest 16081   TopOpenctopn 16082  ordTopcordt 16159   PosetRelcps 17198   TosetRel ctsr 17199  ℂ_fldccnfld 19746   Homeochmeo 21556   IIcii 22678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fi 8317  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ioc 12180  df-ico 12181  df-icc 12182  df-fz 12327  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-plusg 15954  df-mulr 15955  df-starv 15956  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-rest 16083  df-topn 16084  df-topgen 16104  df-ordt 16161  df-ps 17200  df-tsr 17201  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cn 21031  df-hmeo 21558  df-xms 22125  df-ms 22126  df-ii 22680

This theorem is referenced by:  xrhmph  22746