Theorem xrhmeo 25282

Description: The bijection from [ -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	⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))
xrhmeo.g	⊢ 𝐺 = (𝑦 ∈ ( -1[,]1) ↦ if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)))
xrhmeo.j	⊢ 𝐽 = (TopOpen‘ℂfld)

Assertion

Ref	Expression
xrhmeo	⊢ (𝐺 Isom < , < (( -1[,]1), ℝ*) ∧ 𝐺 ∈ ((𝐽 ↾t ( -1[,]1))Homeo(ordTop‘ ≤ )))

Distinct variable groups:   𝑥,𝑦   𝑦,𝐹   𝑥,𝐽,𝑦

Allowed substitution hints:   𝐹(𝑥)   𝐺(𝑥, 𝑦)

Proof of Theorem xrhmeo

Dummy variables 𝑤 𝑣 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iccssxr 13574	. . . 4 ⊢ ( -1[,]1) ⊆ ℝ*
2		xrltso 13283	. . . 4 ⊢ < Or ℝ*
3		soss 5583	. . . 4 ⊢ (( -1[,]1) ⊆ ℝ* → ( < Or ℝ* → < Or ( -1[,]1)))
4	1, 2, 3	mp2 9	. . 3 ⊢ < Or ( -1[,]1)
5		sopo 5582	. . . 4 ⊢ ( < Or ℝ* → < Po ℝ*)
6	2, 5	ax-mp 5	. . 3 ⊢ < Po ℝ*
7		xrhmeo.g	. . . . 5 ⊢ 𝐺 = (𝑦 ∈ ( -1[,]1) ↦ if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)))
8		iccssxr 13574	. . . . . . 7 ⊢ (0[,]+∞) ⊆ ℝ*
9		neg1rr 12319	. . . . . . . . . . . 12 ⊢ -1 ∈ ℝ
10		1re 11321	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
11	9, 10	elicc2i 13556	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ( -1[,]1) ↔ (𝑦 ∈ ℝ ∧ -1 ≤ 𝑦 ∧ 𝑦 ≤ 1))
12	11	simp1bi 1163	. . . . . . . . . 10 ⊢ (𝑦 ∈ ( -1[,]1) → 𝑦 ∈ ℝ)
13	12	adantr 486	. . . . . . . . 9 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ 0 ≤ 𝑦) → 𝑦 ∈ ℝ)
14		simpr 490	. . . . . . . . 9 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ 0 ≤ 𝑦) → 0 ≤ 𝑦)
15	11	simp3bi 1165	. . . . . . . . . 10 ⊢ (𝑦 ∈ ( -1[,]1) → 𝑦 ≤ 1)
16	15	adantr 486	. . . . . . . . 9 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ 0 ≤ 𝑦) → 𝑦 ≤ 1)
17		elicc01 13610	. . . . . . . . 9 ⊢ (𝑦 ∈ (0[,]1) ↔ (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ∧ 𝑦 ≤ 1))
18	13, 14, 16, 17	syl3anbrc 1362	. . . . . . . 8 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ 0 ≤ 𝑦) → 𝑦 ∈ (0[,]1))
19		xrhmeo.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))
20	19	iccpnfcnv 25280	. . . . . . . . . . 11 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑣 ∈ (0[,]+∞) ↦ if(𝑣 = +∞, 1, (𝑣 / (1 + 𝑣)))))
21	20	simpli 489	. . . . . . . . . 10 ⊢ 𝐹:(0[,]1)–1-1-onto→(0[,]+∞)
22		f1of 6835	. . . . . . . . . 10 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → 𝐹:(0[,]1)⟶(0[,]+∞))
23	21, 22	ax-mp 5	. . . . . . . . 9 ⊢ 𝐹:(0[,]1)⟶(0[,]+∞)
24	23	ffvelcdmi 7094	. . . . . . . 8 ⊢ (𝑦 ∈ (0[,]1) → (𝐹‘𝑦) ∈ (0[,]+∞))
25	18, 24	syl 18	. . . . . . 7 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ 0 ≤ 𝑦) → (𝐹‘𝑦) ∈ (0[,]+∞))
26	8, 25	sselid 3911	. . . . . 6 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ 0 ≤ 𝑦) → (𝐹‘𝑦) ∈ ℝ*)
27	12	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ ¬ 0 ≤ 𝑦) → 𝑦 ∈ ℝ)
28	27	renegcld 11756	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ∈ ℝ)
29		0re 11323	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
30		letric 11423	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 ≤ 𝑦 ∨ 𝑦 ≤ 0))
31	29, 12, 30	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ( -1[,]1) → (0 ≤ 𝑦 ∨ 𝑦 ≤ 0))
32	31	orcanai 1018	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ ¬ 0 ≤ 𝑦) → 𝑦 ≤ 0)
33	27	le0neg1d 11900	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝑦 ≤ 0 ↔ 0 ≤ -𝑦))
34	32, 33	mpbid 235	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ ¬ 0 ≤ 𝑦) → 0 ≤ -𝑦)
35	11	simp2bi 1164	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ( -1[,]1) → -1 ≤ 𝑦)
36	35	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ ¬ 0 ≤ 𝑦) → -1 ≤ 𝑦)
37		lenegcon1 11833	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ( -1 ≤ 𝑦 ↔ -𝑦 ≤ 1))
38	10, 27, 37	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ ¬ 0 ≤ 𝑦) → ( -1 ≤ 𝑦 ↔ -𝑦 ≤ 1))
39	36, 38	mpbid 235	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ≤ 1)
40		elicc01 13610	. . . . . . . . . 10 ⊢ ( -𝑦 ∈ (0[,]1) ↔ ( -𝑦 ∈ ℝ ∧ 0 ≤ -𝑦 ∧ -𝑦 ≤ 1))
41	28, 34, 39, 40	syl3anbrc 1362	. . . . . . . . 9 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ∈ (0[,]1))
42	23	ffvelcdmi 7094	. . . . . . . . 9 ⊢ ( -𝑦 ∈ (0[,]1) → (𝐹‘ -𝑦) ∈ (0[,]+∞))
43	41, 42	syl 18	. . . . . . . 8 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝐹‘ -𝑦) ∈ (0[,]+∞))
44	8, 43	sselid 3911	. . . . . . 7 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝐹‘ -𝑦) ∈ ℝ*)
45	44	xnegcld 13443	. . . . . 6 ⊢ ((𝑦 ∈ ( -1[,]1) ∧ ¬ 0 ≤ 𝑦) → -e(𝐹‘ -𝑦) ∈ ℝ*)
46	26, 45	ifclda 4521	. . . . 5 ⊢ (𝑦 ∈ ( -1[,]1) → if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)) ∈ ℝ*)
47	7, 46	fmpti 7123	. . . 4 ⊢ 𝐺:( -1[,]1)⟶ℝ*
48		frn 6728	. . . . . 6 ⊢ (𝐺:( -1[,]1)⟶ℝ* → ran 𝐺 ⊆ ℝ*)
49	47, 48	ax-mp 5	. . . . 5 ⊢ ran 𝐺 ⊆ ℝ*
50		ssabral 3992	. . . . . . 7 ⊢ (ℝ* ⊆ {𝑧 ∣ ∃𝑦 ∈ ( -1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦))} ↔ ∀𝑧 ∈ ℝ* ∃𝑦 ∈ ( -1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)))
51		0le1 11852	. . . . . . . . . . . . 13 ⊢ 0 ≤ 1
52		le0neg2 11838	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ → (0 ≤ 1 ↔ -1 ≤ 0))
53	10, 52	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (0 ≤ 1 ↔ -1 ≤ 0)
54	51, 53	mpbi 233	. . . . . . . . . . . 12 ⊢ -1 ≤ 0
55		1le1 11957	. . . . . . . . . . . 12 ⊢ 1 ≤ 1
56		iccss 13558	. . . . . . . . . . . 12 ⊢ ((( -1 ∈ ℝ ∧ 1 ∈ ℝ) ∧ ( -1 ≤ 0 ∧ 1 ≤ 1)) → (0[,]1) ⊆ ( -1[,]1))
57	9, 10, 54, 55, 56	mp4an 706	. . . . . . . . . . 11 ⊢ (0[,]1) ⊆ ( -1[,]1)
58		elxrge0 13601	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (0[,]+∞) ↔ (𝑧 ∈ ℝ* ∧ 0 ≤ 𝑧))
59		f1ocnv 6848	. . . . . . . . . . . . . 14 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → ◡𝐹:(0[,]+∞)–1-1-onto→(0[,]1))
60		f1of 6835	. . . . . . . . . . . . . 14 ⊢ (◡𝐹:(0[,]+∞)–1-1-onto→(0[,]1) → ◡𝐹:(0[,]+∞)⟶(0[,]1))
61	21, 59, 60	mp2b 10	. . . . . . . . . . . . 13 ⊢ ◡𝐹:(0[,]+∞)⟶(0[,]1)
62	61	ffvelcdmi 7094	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (0[,]+∞) → (◡𝐹‘𝑧) ∈ (0[,]1))
63	58, 62	sylbir 238	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ* ∧ 0 ≤ 𝑧) → (◡𝐹‘𝑧) ∈ (0[,]1))
64	57, 63	sselid 3911	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ* ∧ 0 ≤ 𝑧) → (◡𝐹‘𝑧) ∈ ( -1[,]1))
65		elicc01 13610	. . . . . . . . . . . 12 ⊢ ((◡𝐹‘𝑧) ∈ (0[,]1) ↔ ((◡𝐹‘𝑧) ∈ ℝ ∧ 0 ≤ (◡𝐹‘𝑧) ∧ (◡𝐹‘𝑧) ≤ 1))
66	65	simp2bi 1164	. . . . . . . . . . 11 ⊢ ((◡𝐹‘𝑧) ∈ (0[,]1) → 0 ≤ (◡𝐹‘𝑧))
67	63, 66	syl 18	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ* ∧ 0 ≤ 𝑧) → 0 ≤ (◡𝐹‘𝑧))
68	58	biimpri 231	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ* ∧ 0 ≤ 𝑧) → 𝑧 ∈ (0[,]+∞))
69		f1ocnvfv2 7295	. . . . . . . . . . . 12 ⊢ ((𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ 𝑧 ∈ (0[,]+∞)) → (𝐹‘(◡𝐹‘𝑧)) = 𝑧)
70	21, 68, 69	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ* ∧ 0 ≤ 𝑧) → (𝐹‘(◡𝐹‘𝑧)) = 𝑧)
71	70	eqcomd 2769	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ* ∧ 0 ≤ 𝑧) → 𝑧 = (𝐹‘(◡𝐹‘𝑧)))
72		breq2 5110	. . . . . . . . . . . 12 ⊢ (𝑦 = (◡𝐹‘𝑧) → (0 ≤ 𝑦 ↔ 0 ≤ (◡𝐹‘𝑧)))
73		fveq2 6896	. . . . . . . . . . . . 13 ⊢ (𝑦 = (◡𝐹‘𝑧) → (𝐹‘𝑦) = (𝐹‘(◡𝐹‘𝑧)))
74	73	eqeq2d 2774	. . . . . . . . . . . 12 ⊢ (𝑦 = (◡𝐹‘𝑧) → (𝑧 = (𝐹‘𝑦) ↔ 𝑧 = (𝐹‘(◡𝐹‘𝑧))))
75	72, 74	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑦 = (◡𝐹‘𝑧) → ((0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) ↔ (0 ≤ (◡𝐹‘𝑧) ∧ 𝑧 = (𝐹‘(◡𝐹‘𝑧)))))
76	75	rspcev 3580	. . . . . . . . . 10 ⊢ (((◡𝐹‘𝑧) ∈ ( -1[,]1) ∧ (0 ≤ (◡𝐹‘𝑧) ∧ 𝑧 = (𝐹‘(◡𝐹‘𝑧)))) → ∃𝑦 ∈ ( -1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)))
77	64, 67, 71, 76	syl12anc 850	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ* ∧ 0 ≤ 𝑧) → ∃𝑦 ∈ ( -1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)))
78		iftrue 4491	. . . . . . . . . . . 12 ⊢ (0 ≤ 𝑦 → if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)) = (𝐹‘𝑦))
79	78	eqeq2d 2774	. . . . . . . . . . 11 ⊢ (0 ≤ 𝑦 → (𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)) ↔ 𝑧 = (𝐹‘𝑦)))
80	79	biimpar 483	. . . . . . . . . 10 ⊢ ((0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) → 𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)))
81	80	reximi 3104	. . . . . . . . 9 ⊢ (∃𝑦 ∈ ( -1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) → ∃𝑦 ∈ ( -1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)))
82	77, 81	syl 18	. . . . . . . 8 ⊢ ((𝑧 ∈ ℝ* ∧ 0 ≤ 𝑧) → ∃𝑦 ∈ ( -1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)))
83		xnegcl 13356	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ* → -e𝑧 ∈ ℝ*)
84	83	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → -e𝑧 ∈ ℝ*)
85		0xr 11369	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ*
86		xrletri 13295	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) → (0 ≤ 𝑧 ∨ 𝑧 ≤ 0))
87	85, 86	mpan 703	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℝ* → (0 ≤ 𝑧 ∨ 𝑧 ≤ 0))
88	87	ord 878	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℝ* → (¬ 0 ≤ 𝑧 → 𝑧 ≤ 0))
89		xle0neg1 13364	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℝ* → (𝑧 ≤ 0 ↔ 0 ≤ -e𝑧))
90	88, 89	sylibd 242	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ* → (¬ 0 ≤ 𝑧 → 0 ≤ -e𝑧))
91	90	imp 412	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → 0 ≤ -e𝑧)
92		elxrge0 13601	. . . . . . . . . . . . . . 15 ⊢ ( -e𝑧 ∈ (0[,]+∞) ↔ ( -e𝑧 ∈ ℝ* ∧ 0 ≤ -e𝑧))
93	84, 91, 92	sylanbrc 595	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → -e𝑧 ∈ (0[,]+∞))
94	61	ffvelcdmi 7094	. . . . . . . . . . . . . 14 ⊢ ( -e𝑧 ∈ (0[,]+∞) → (◡𝐹‘ -e𝑧) ∈ (0[,]1))
95	93, 94	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → (◡𝐹‘ -e𝑧) ∈ (0[,]1))
96	57, 95	sselid 3911	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → (◡𝐹‘ -e𝑧) ∈ ( -1[,]1))
97		iccssre 13573	. . . . . . . . . . . . . . 15 ⊢ (( -1 ∈ ℝ ∧ 1 ∈ ℝ) → ( -1[,]1) ⊆ ℝ)
98	9, 10, 97	mp2an 705	. . . . . . . . . . . . . 14 ⊢ ( -1[,]1) ⊆ ℝ
99	98, 96	sselid 3911	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → (◡𝐹‘ -e𝑧) ∈ ℝ)
100		iccneg 13616	. . . . . . . . . . . . . 14 ⊢ (( -1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (◡𝐹‘ -e𝑧) ∈ ℝ) → ((◡𝐹‘ -e𝑧) ∈ ( -1[,]1) ↔ -(◡𝐹‘ -e𝑧) ∈ ( -1[,] - -1)))
101	9, 10, 100	mp3an12 1480	. . . . . . . . . . . . 13 ⊢ ((◡𝐹‘ -e𝑧) ∈ ℝ → ((◡𝐹‘ -e𝑧) ∈ ( -1[,]1) ↔ -(◡𝐹‘ -e𝑧) ∈ ( -1[,] - -1)))
102	99, 101	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → ((◡𝐹‘ -e𝑧) ∈ ( -1[,]1) ↔ -(◡𝐹‘ -e𝑧) ∈ ( -1[,] - -1)))
103	96, 102	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → -(◡𝐹‘ -e𝑧) ∈ ( -1[,] - -1))
104		negneg1e1 12322	. . . . . . . . . . . 12 ⊢ - -1 = 1
105	104	oveq2i 7441	. . . . . . . . . . 11 ⊢ ( -1[,] - -1) = ( -1[,]1)
106	103, 105	eleqtrdi 2874	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → -(◡𝐹‘ -e𝑧) ∈ ( -1[,]1))
107		xle0neg2 13365	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℝ* → (0 ≤ 𝑧 ↔ -e𝑧 ≤ 0))
108	107	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℝ* → (¬ 0 ≤ 𝑧 ↔ ¬ -e𝑧 ≤ 0))
109	108	biimpa 482	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → ¬ -e𝑧 ≤ 0)
110		f1ocnvfv2 7295	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ -e𝑧 ∈ (0[,]+∞)) → (𝐹‘(◡𝐹‘ -e𝑧)) = -e𝑧)
111	21, 93, 110	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘(◡𝐹‘ -e𝑧)) = -e𝑧)
112		0elunit 13613	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ (0[,]1)
113		ax-1ne0 11282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ≠ 0
114		neeq2 3022	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 0 → (1 ≠ 𝑥 ↔ 1 ≠ 0))
115	113, 114	mpbiri 261	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 0 → 1 ≠ 𝑥)
116	115	necomd 3014	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → 𝑥 ≠ 1)
117		ifnefalse 4497	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ≠ 1 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) = (𝑥 / (1 − 𝑥)))
118	116, 117	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) = (𝑥 / (1 − 𝑥)))
119		id 23	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 0 → 𝑥 = 0)
120		oveq2 7438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 0 → (1 − 𝑥) = (1 − 0))
121		1m0e1 12475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 − 0) = 1
122	120, 121	eqtrdi 2814	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 0 → (1 − 𝑥) = 1)
123	119, 122	oveq12d 7448	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → (𝑥 / (1 − 𝑥)) = (0 / 1))
124		ax-1cn 11271	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℂ
125	124, 113	div0i 12064	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 / 1) = 0
126	123, 125	eqtrdi 2814	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → (𝑥 / (1 − 𝑥)) = 0)
127	118, 126	eqtrd 2798	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) = 0)
128		c0ex 11313	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
129	127, 19, 128	fvmpt 7004	. . . . . . . . . . . . . . . 16 ⊢ (0 ∈ (0[,]1) → (𝐹‘0) = 0)
130	112, 129	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘0) = 0
131	130	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘0) = 0)
132	111, 131	breq12d 5119	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → ((𝐹‘(◡𝐹‘ -e𝑧)) ≤ (𝐹‘0) ↔ -e𝑧 ≤ 0))
133	109, 132	mtbird 328	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → ¬ (𝐹‘(◡𝐹‘ -e𝑧)) ≤ (𝐹‘0))
134		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) = ((ordTop‘ ≤ ) ↾t (0[,]+∞))
135	19, 134	iccpnfhmeo 25281	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ 𝐹 ∈ (IIHomeo((ordTop‘ ≤ ) ↾t (0[,]+∞))))
136	135	simpli 489	. . . . . . . . . . . . . 14 ⊢ 𝐹 Isom < , < ((0[,]1), (0[,]+∞))
137		iccssxr 13574	. . . . . . . . . . . . . . 15 ⊢ (0[,]1) ⊆ ℝ*
138	137, 8	pm3.2i 476	. . . . . . . . . . . . . 14 ⊢ ((0[,]1) ⊆ ℝ* ∧ (0[,]+∞) ⊆ ℝ*)
139		leisorel 14618	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ ((0[,]1) ⊆ ℝ* ∧ (0[,]+∞) ⊆ ℝ*) ∧ ((◡𝐹‘ -e𝑧) ∈ (0[,]1) ∧ 0 ∈ (0[,]1))) → ((◡𝐹‘ -e𝑧) ≤ 0 ↔ (𝐹‘(◡𝐹‘ -e𝑧)) ≤ (𝐹‘0)))
140	136, 138, 139	mp3an12 1480	. . . . . . . . . . . . 13 ⊢ (((◡𝐹‘ -e𝑧) ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → ((◡𝐹‘ -e𝑧) ≤ 0 ↔ (𝐹‘(◡𝐹‘ -e𝑧)) ≤ (𝐹‘0)))
141	95, 112, 140	sylancl 598	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → ((◡𝐹‘ -e𝑧) ≤ 0 ↔ (𝐹‘(◡𝐹‘ -e𝑧)) ≤ (𝐹‘0)))
142	133, 141	mtbird 328	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → ¬ (◡𝐹‘ -e𝑧) ≤ 0)
143	99	le0neg1d 11900	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → ((◡𝐹‘ -e𝑧) ≤ 0 ↔ 0 ≤ -(◡𝐹‘ -e𝑧)))
144	142, 143	mtbid 327	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → ¬ 0 ≤ -(◡𝐹‘ -e𝑧))
145		unitssre 13643	. . . . . . . . . . . . . . . . 17 ⊢ (0[,]1) ⊆ ℝ
146	145, 95	sselid 3911	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → (◡𝐹‘ -e𝑧) ∈ ℝ)
147	146	recnd 11350	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → (◡𝐹‘ -e𝑧) ∈ ℂ)
148	147	negnegd 11673	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → - -(◡𝐹‘ -e𝑧) = (◡𝐹‘ -e𝑧))
149	148	fveq2d 6900	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘ - -(◡𝐹‘ -e𝑧)) = (𝐹‘(◡𝐹‘ -e𝑧)))
150	149, 111	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘ - -(◡𝐹‘ -e𝑧)) = -e𝑧)
151		xnegeq 13350	. . . . . . . . . . . 12 ⊢ ((𝐹‘ - -(◡𝐹‘ -e𝑧)) = -e𝑧 → -e(𝐹‘ - -(◡𝐹‘ -e𝑧)) = -e -e𝑧)
152	150, 151	syl 18	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → -e(𝐹‘ - -(◡𝐹‘ -e𝑧)) = -e -e𝑧)
153		xnegneg 13357	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ* → -e -e𝑧 = 𝑧)
154	153	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → -e -e𝑧 = 𝑧)
155	152, 154	eqtr2d 2799	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → 𝑧 = -e(𝐹‘ - -(◡𝐹‘ -e𝑧)))
156		breq2 5110	. . . . . . . . . . . . 13 ⊢ (𝑦 = -(◡𝐹‘ -e𝑧) → (0 ≤ 𝑦 ↔ 0 ≤ -(◡𝐹‘ -e𝑧)))
157	156	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑦 = -(◡𝐹‘ -e𝑧) → (¬ 0 ≤ 𝑦 ↔ ¬ 0 ≤ -(◡𝐹‘ -e𝑧)))
158		negeq 11562	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = -(◡𝐹‘ -e𝑧) → -𝑦 = - -(◡𝐹‘ -e𝑧))
159	158	fveq2d 6900	. . . . . . . . . . . . . 14 ⊢ (𝑦 = -(◡𝐹‘ -e𝑧) → (𝐹‘ -𝑦) = (𝐹‘ - -(◡𝐹‘ -e𝑧)))
160		xnegeq 13350	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘ -𝑦) = (𝐹‘ - -(◡𝐹‘ -e𝑧)) → -e(𝐹‘ -𝑦) = -e(𝐹‘ - -(◡𝐹‘ -e𝑧)))
161	159, 160	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑦 = -(◡𝐹‘ -e𝑧) → -e(𝐹‘ -𝑦) = -e(𝐹‘ - -(◡𝐹‘ -e𝑧)))
162	161	eqeq2d 2774	. . . . . . . . . . . 12 ⊢ (𝑦 = -(◡𝐹‘ -e𝑧) → (𝑧 = -e(𝐹‘ -𝑦) ↔ 𝑧 = -e(𝐹‘ - -(◡𝐹‘ -e𝑧))))
163	157, 162	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑦 = -(◡𝐹‘ -e𝑧) → ((¬ 0 ≤ 𝑦 ∧ 𝑧 = -e(𝐹‘ -𝑦)) ↔ (¬ 0 ≤ -(◡𝐹‘ -e𝑧) ∧ 𝑧 = -e(𝐹‘ - -(◡𝐹‘ -e𝑧)))))
164	163	rspcev 3580	. . . . . . . . . 10 ⊢ (( -(◡𝐹‘ -e𝑧) ∈ ( -1[,]1) ∧ (¬ 0 ≤ -(◡𝐹‘ -e𝑧) ∧ 𝑧 = -e(𝐹‘ - -(◡𝐹‘ -e𝑧)))) → ∃𝑦 ∈ ( -1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -e(𝐹‘ -𝑦)))
165	106, 144, 155, 164	syl12anc 850	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → ∃𝑦 ∈ ( -1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -e(𝐹‘ -𝑦)))
166		iffalse 4494	. . . . . . . . . . . 12 ⊢ (¬ 0 ≤ 𝑦 → if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)) = -e(𝐹‘ -𝑦))
167	166	eqeq2d 2774	. . . . . . . . . . 11 ⊢ (¬ 0 ≤ 𝑦 → (𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)) ↔ 𝑧 = -e(𝐹‘ -𝑦)))
168	167	biimpar 483	. . . . . . . . . 10 ⊢ ((¬ 0 ≤ 𝑦 ∧ 𝑧 = -e(𝐹‘ -𝑦)) → 𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)))
169	168	reximi 3104	. . . . . . . . 9 ⊢ (∃𝑦 ∈ ( -1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -e(𝐹‘ -𝑦)) → ∃𝑦 ∈ ( -1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)))
170	165, 169	syl 18	. . . . . . . 8 ⊢ ((𝑧 ∈ ℝ* ∧ ¬ 0 ≤ 𝑧) → ∃𝑦 ∈ ( -1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)))
171	82, 170	pm2.61dan 825	. . . . . . 7 ⊢ (𝑧 ∈ ℝ* → ∃𝑦 ∈ ( -1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)))
172	50, 171	mprgbir 3087	. . . . . 6 ⊢ ℝ* ⊆ {𝑧 ∣ ∃𝑦 ∈ ( -1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦))}
173	7	rnmpt 5944	. . . . . 6 ⊢ ran 𝐺 = {𝑧 ∣ ∃𝑦 ∈ ( -1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦))}
174	172, 173	sseqtrri 3962	. . . . 5 ⊢ ℝ* ⊆ ran 𝐺
175	49, 174	eqssi 3929	. . . 4 ⊢ ran 𝐺 = ℝ*
176		dffo2 6811	. . . 4 ⊢ (𝐺:( -1[,]1)–onto→ℝ* ↔ (𝐺:( -1[,]1)⟶ℝ* ∧ ran 𝐺 = ℝ*))
177	47, 175, 176	mpbir2an 724	. . 3 ⊢ 𝐺:( -1[,]1)–onto→ℝ*
178		breq1 5109	. . . . . . 7 ⊢ ((𝐹‘𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -e(𝐹‘ -𝑧)) → ((𝐹‘𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤)) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -e(𝐹‘ -𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤))))
179		breq1 5109	. . . . . . 7 ⊢ ( -e(𝐹‘ -𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -e(𝐹‘ -𝑧)) → ( -e(𝐹‘ -𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤)) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -e(𝐹‘ -𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤))))
180		simpl3 1212	. . . . . . . . 9 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 < 𝑤)
181		simpl1 1210	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ∈ ( -1[,]1))
182		simpr 490	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ≤ 𝑧)
183		breq2 5110	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (0 ≤ 𝑦 ↔ 0 ≤ 𝑧))
184		eleq1w 2847	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ (0[,]1) ↔ 𝑧 ∈ (0[,]1)))
185	183, 184	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → ((0 ≤ 𝑦 → 𝑦 ∈ (0[,]1)) ↔ (0 ≤ 𝑧 → 𝑧 ∈ (0[,]1))))
186	18	ex 418	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ( -1[,]1) → (0 ≤ 𝑦 → 𝑦 ∈ (0[,]1)))
187	185, 186	vtoclga 3540	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ( -1[,]1) → (0 ≤ 𝑧 → 𝑧 ∈ (0[,]1)))
188	181, 182, 187	sylc 66	. . . . . . . . . 10 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ∈ (0[,]1))
189		simpl2 1211	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ ( -1[,]1))
190	29	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ∈ ℝ)
191	98, 181	sselid 3911	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ∈ ℝ)
192	98, 189	sselid 3911	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ ℝ)
193	191, 192, 180	ltled 11471	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ≤ 𝑤)
194	190, 191, 192, 182, 193	letrd 11480	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ≤ 𝑤)
195		breq2 5110	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (0 ≤ 𝑦 ↔ 0 ≤ 𝑤))
196		eleq1w 2847	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (0[,]1) ↔ 𝑤 ∈ (0[,]1)))
197	195, 196	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → ((0 ≤ 𝑦 → 𝑦 ∈ (0[,]1)) ↔ (0 ≤ 𝑤 → 𝑤 ∈ (0[,]1))))
198	197, 186	vtoclga 3540	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ( -1[,]1) → (0 ≤ 𝑤 → 𝑤 ∈ (0[,]1)))
199	189, 194, 198	sylc 66	. . . . . . . . . 10 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ (0[,]1))
200		isorel 7344	. . . . . . . . . . 11 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1))) → (𝑧 < 𝑤 ↔ (𝐹‘𝑧) < (𝐹‘𝑤)))
201	136, 200	mpan 703	. . . . . . . . . 10 ⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) → (𝑧 < 𝑤 ↔ (𝐹‘𝑧) < (𝐹‘𝑤)))
202	188, 199, 201	syl2anc 596	. . . . . . . . 9 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → (𝑧 < 𝑤 ↔ (𝐹‘𝑧) < (𝐹‘𝑤)))
203	180, 202	mpbid 235	. . . . . . . 8 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → (𝐹‘𝑧) < (𝐹‘𝑤))
204	194	iftrued 4493	. . . . . . . 8 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤)) = (𝐹‘𝑤))
205	203, 204	breqtrrd 5136	. . . . . . 7 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → (𝐹‘𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤)))
206		breq2 5110	. . . . . . . 8 ⊢ ((𝐹‘𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤)) → ( -e(𝐹‘ -𝑧) < (𝐹‘𝑤) ↔ -e(𝐹‘ -𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤))))
207		breq2 5110	. . . . . . . 8 ⊢ ( -e(𝐹‘ -𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤)) → ( -e(𝐹‘ -𝑧) < -e(𝐹‘ -𝑤) ↔ -e(𝐹‘ -𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤))))
208		simpl1 1210	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → 𝑧 ∈ ( -1[,]1))
209		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → ¬ 0 ≤ 𝑧)
210	183	notbid 321	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → (¬ 0 ≤ 𝑦 ↔ ¬ 0 ≤ 𝑧))
211		negeq 11562	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑧 → -𝑦 = -𝑧)
212	211	eleq1d 2849	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → ( -𝑦 ∈ (0[,]1) ↔ -𝑧 ∈ (0[,]1)))
213	210, 212	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → ((¬ 0 ≤ 𝑦 → -𝑦 ∈ (0[,]1)) ↔ (¬ 0 ≤ 𝑧 → -𝑧 ∈ (0[,]1))))
214	41	ex 418	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ( -1[,]1) → (¬ 0 ≤ 𝑦 → -𝑦 ∈ (0[,]1)))
215	213, 214	vtoclga 3540	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ( -1[,]1) → (¬ 0 ≤ 𝑧 → -𝑧 ∈ (0[,]1)))
216	208, 209, 215	sylc 66	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → -𝑧 ∈ (0[,]1))
217	216	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -𝑧 ∈ (0[,]1))
218	23	ffvelcdmi 7094	. . . . . . . . . . . 12 ⊢ ( -𝑧 ∈ (0[,]1) → (𝐹‘ -𝑧) ∈ (0[,]+∞))
219	217, 218	syl 18	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘ -𝑧) ∈ (0[,]+∞))
220	8, 219	sselid 3911	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘ -𝑧) ∈ ℝ*)
221	220	xnegcld 13443	. . . . . . . . 9 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -e(𝐹‘ -𝑧) ∈ ℝ*)
222	85	a1i 11	. . . . . . . . 9 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 ∈ ℝ*)
223		simpll2 1232	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑤 ∈ ( -1[,]1))
224		simpr 490	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 ≤ 𝑤)
225	223, 224, 198	sylc 66	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑤 ∈ (0[,]1))
226	23	ffvelcdmi 7094	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (0[,]1) → (𝐹‘𝑤) ∈ (0[,]+∞))
227	225, 226	syl 18	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘𝑤) ∈ (0[,]+∞))
228	8, 227	sselid 3911	. . . . . . . . 9 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘𝑤) ∈ ℝ*)
229	209	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → ¬ 0 ≤ 𝑧)
230		simpll1 1231	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 ∈ ( -1[,]1))
231	98, 230	sselid 3911	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 ∈ ℝ)
232		ltnle 11402	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ ∧ 0 ∈ ℝ) → (𝑧 < 0 ↔ ¬ 0 ≤ 𝑧))
233	231, 29, 232	sylancl 598	. . . . . . . . . . . . . 14 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝑧 < 0 ↔ ¬ 0 ≤ 𝑧))
234	229, 233	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 < 0)
235	231	lt0neg1d 11898	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝑧 < 0 ↔ 0 < -𝑧))
236	234, 235	mpbid 235	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 < -𝑧)
237		isorel 7344	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (0 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1))) → (0 < -𝑧 ↔ (𝐹‘0) < (𝐹‘ -𝑧)))
238	136, 237	mpan 703	. . . . . . . . . . . . 13 ⊢ ((0 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1)) → (0 < -𝑧 ↔ (𝐹‘0) < (𝐹‘ -𝑧)))
239	112, 217, 238	sylancr 599	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (0 < -𝑧 ↔ (𝐹‘0) < (𝐹‘ -𝑧)))
240	236, 239	mpbid 235	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘0) < (𝐹‘ -𝑧))
241	130, 240	eqbrtrrid 5144	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 < (𝐹‘ -𝑧))
242		xlt0neg2 13363	. . . . . . . . . . 11 ⊢ ((𝐹‘ -𝑧) ∈ ℝ* → (0 < (𝐹‘ -𝑧) ↔ -e(𝐹‘ -𝑧) < 0))
243	220, 242	syl 18	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (0 < (𝐹‘ -𝑧) ↔ -e(𝐹‘ -𝑧) < 0))
244	241, 243	mpbid 235	. . . . . . . . 9 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -e(𝐹‘ -𝑧) < 0)
245		elxrge0 13601	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑤) ∈ (0[,]+∞) ↔ ((𝐹‘𝑤) ∈ ℝ* ∧ 0 ≤ (𝐹‘𝑤)))
246	245	simprbi 503	. . . . . . . . . 10 ⊢ ((𝐹‘𝑤) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝑤))
247	227, 246	syl 18	. . . . . . . . 9 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 ≤ (𝐹‘𝑤))
248	221, 222, 228, 244, 247	xrltletrd 13303	. . . . . . . 8 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -e(𝐹‘ -𝑧) < (𝐹‘𝑤))
249		simpll3 1233	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑧 < 𝑤)
250		simpll1 1231	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑧 ∈ ( -1[,]1))
251	98, 250	sselid 3911	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑧 ∈ ℝ)
252		simpll2 1232	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑤 ∈ ( -1[,]1))
253	98, 252	sselid 3911	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑤 ∈ ℝ)
254	251, 253	ltnegd 11907	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝑧 < 𝑤 ↔ -𝑤 < -𝑧))
255	249, 254	mpbid 235	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -𝑤 < -𝑧)
256		simpr 490	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → ¬ 0 ≤ 𝑤)
257	195	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (¬ 0 ≤ 𝑦 ↔ ¬ 0 ≤ 𝑤))
258		negeq 11562	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → -𝑦 = -𝑤)
259	258	eleq1d 2849	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → ( -𝑦 ∈ (0[,]1) ↔ -𝑤 ∈ (0[,]1)))
260	257, 259	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((¬ 0 ≤ 𝑦 → -𝑦 ∈ (0[,]1)) ↔ (¬ 0 ≤ 𝑤 → -𝑤 ∈ (0[,]1))))
261	260, 214	vtoclga 3540	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ( -1[,]1) → (¬ 0 ≤ 𝑤 → -𝑤 ∈ (0[,]1)))
262	252, 256, 261	sylc 66	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -𝑤 ∈ (0[,]1))
263	216	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -𝑧 ∈ (0[,]1))
264		isorel 7344	. . . . . . . . . . . 12 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ ( -𝑤 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1))) → ( -𝑤 < -𝑧 ↔ (𝐹‘ -𝑤) < (𝐹‘ -𝑧)))
265	136, 264	mpan 703	. . . . . . . . . . 11 ⊢ (( -𝑤 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1)) → ( -𝑤 < -𝑧 ↔ (𝐹‘ -𝑤) < (𝐹‘ -𝑧)))
266	262, 263, 265	syl2anc 596	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → ( -𝑤 < -𝑧 ↔ (𝐹‘ -𝑤) < (𝐹‘ -𝑧)))
267	255, 266	mpbid 235	. . . . . . . . 9 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘ -𝑤) < (𝐹‘ -𝑧))
268	23	ffvelcdmi 7094	. . . . . . . . . . . 12 ⊢ ( -𝑤 ∈ (0[,]1) → (𝐹‘ -𝑤) ∈ (0[,]+∞))
269	262, 268	syl 18	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘ -𝑤) ∈ (0[,]+∞))
270	8, 269	sselid 3911	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘ -𝑤) ∈ ℝ*)
271	263, 218	syl 18	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘ -𝑧) ∈ (0[,]+∞))
272	8, 271	sselid 3911	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘ -𝑧) ∈ ℝ*)
273		xltneg 13360	. . . . . . . . . 10 ⊢ (((𝐹‘ -𝑤) ∈ ℝ* ∧ (𝐹‘ -𝑧) ∈ ℝ*) → ((𝐹‘ -𝑤) < (𝐹‘ -𝑧) ↔ -e(𝐹‘ -𝑧) < -e(𝐹‘ -𝑤)))
274	270, 272, 273	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → ((𝐹‘ -𝑤) < (𝐹‘ -𝑧) ↔ -e(𝐹‘ -𝑧) < -e(𝐹‘ -𝑤)))
275	267, 274	mpbid 235	. . . . . . . 8 ⊢ ((((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -e(𝐹‘ -𝑧) < -e(𝐹‘ -𝑤))
276	206, 207, 248, 275	ifbothda 4524	. . . . . . 7 ⊢ (((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → -e(𝐹‘ -𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤)))
277	178, 179, 205, 276	ifbothda 4524	. . . . . 6 ⊢ ((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1) ∧ 𝑧 < 𝑤) → if(0 ≤ 𝑧, (𝐹‘𝑧), -e(𝐹‘ -𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤)))
278	277	3expia 1139	. . . . 5 ⊢ ((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1)) → (𝑧 < 𝑤 → if(0 ≤ 𝑧, (𝐹‘𝑧), -e(𝐹‘ -𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤))))
279		fveq2 6896	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
280	211	fveq2d 6900	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝐹‘ -𝑦) = (𝐹‘ -𝑧))
281		xnegeq 13350	. . . . . . . . 9 ⊢ ((𝐹‘ -𝑦) = (𝐹‘ -𝑧) → -e(𝐹‘ -𝑦) = -e(𝐹‘ -𝑧))
282	280, 281	syl 18	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → -e(𝐹‘ -𝑦) = -e(𝐹‘ -𝑧))
283	183, 279, 282	ifbieq12d 4514	. . . . . . 7 ⊢ (𝑦 = 𝑧 → if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)) = if(0 ≤ 𝑧, (𝐹‘𝑧), -e(𝐹‘ -𝑧)))
284		fvex 6909	. . . . . . . 8 ⊢ (𝐹‘𝑧) ∈ V
285		xnegex 13351	. . . . . . . 8 ⊢ -e(𝐹‘ -𝑧) ∈ V
286	284, 285	ifex 4536	. . . . . . 7 ⊢ if(0 ≤ 𝑧, (𝐹‘𝑧), -e(𝐹‘ -𝑧)) ∈ V
287	283, 7, 286	fvmpt 7004	. . . . . 6 ⊢ (𝑧 ∈ ( -1[,]1) → (𝐺‘𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -e(𝐹‘ -𝑧)))
288		fveq2 6896	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
289	258	fveq2d 6900	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝐹‘ -𝑦) = (𝐹‘ -𝑤))
290		xnegeq 13350	. . . . . . . . 9 ⊢ ((𝐹‘ -𝑦) = (𝐹‘ -𝑤) → -e(𝐹‘ -𝑦) = -e(𝐹‘ -𝑤))
291	289, 290	syl 18	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → -e(𝐹‘ -𝑦) = -e(𝐹‘ -𝑤))
292	195, 288, 291	ifbieq12d 4514	. . . . . . 7 ⊢ (𝑦 = 𝑤 → if(0 ≤ 𝑦, (𝐹‘𝑦), -e(𝐹‘ -𝑦)) = if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤)))
293		fvex 6909	. . . . . . . 8 ⊢ (𝐹‘𝑤) ∈ V
294		xnegex 13351	. . . . . . . 8 ⊢ -e(𝐹‘ -𝑤) ∈ V
295	293, 294	ifex 4536	. . . . . . 7 ⊢ if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤)) ∈ V
296	292, 7, 295	fvmpt 7004	. . . . . 6 ⊢ (𝑤 ∈ ( -1[,]1) → (𝐺‘𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤)))
297	287, 296	breqan12d 5122	. . . . 5 ⊢ ((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1)) → ((𝐺‘𝑧) < (𝐺‘𝑤) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -e(𝐹‘ -𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -e(𝐹‘ -𝑤))))
298	278, 297	sylibrd 262	. . . 4 ⊢ ((𝑧 ∈ ( -1[,]1) ∧ 𝑤 ∈ ( -1[,]1)) → (𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤)))
299	298	rgen2 3206	. . 3 ⊢ ∀𝑧 ∈ ( -1[,]1)∀𝑤 ∈ ( -1[,]1)(𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤))
300		soisoi 7346	. . 3 ⊢ ((( < Or ( -1[,]1) ∧ < Po ℝ*) ∧ (𝐺:( -1[,]1)–onto→ℝ* ∧ ∀𝑧 ∈ ( -1[,]1)∀𝑤 ∈ ( -1[,]1)(𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤)))) → 𝐺 Isom < , < (( -1[,]1), ℝ*))
301	4, 6, 177, 299, 300	mp4an 706	. 2 ⊢ 𝐺 Isom < , < (( -1[,]1), ℝ*)
302		letsr 18782	. . . . . 6 ⊢ ≤ ∈ TosetRel
303	302	elexi 3476	. . . . 5 ⊢ ≤ ∈ V
304	303	inex1 5281	. . . 4 ⊢ ( ≤ ∩ (( -1[,]1) × ( -1[,]1))) ∈ V
305		ssid 3935	. . . . . . 7 ⊢ ℝ* ⊆ ℝ*
306		leiso 14617	. . . . . . 7 ⊢ ((( -1[,]1) ⊆ ℝ* ∧ ℝ* ⊆ ℝ*) → (𝐺 Isom < , < (( -1[,]1), ℝ*) ↔ 𝐺 Isom ≤ , ≤ (( -1[,]1), ℝ*)))
307	1, 305, 306	mp2an 705	. . . . . 6 ⊢ (𝐺 Isom < , < (( -1[,]1), ℝ*) ↔ 𝐺 Isom ≤ , ≤ (( -1[,]1), ℝ*))
308	301, 307	mpbi 233	. . . . 5 ⊢ 𝐺 Isom ≤ , ≤ (( -1[,]1), ℝ*)
309		isores1 7352	. . . . 5 ⊢ (𝐺 Isom ≤ , ≤ (( -1[,]1), ℝ*) ↔ 𝐺 Isom ( ≤ ∩ (( -1[,]1) × ( -1[,]1))), ≤ (( -1[,]1), ℝ*))
310	308, 309	mpbi 233	. . . 4 ⊢ 𝐺 Isom ( ≤ ∩ (( -1[,]1) × ( -1[,]1))), ≤ (( -1[,]1), ℝ*)
311		tsrps 18776	. . . . . . . 8 ⊢ ( ≤ ∈ TosetRel → ≤ ∈ PosetRel)
312	302, 311	ax-mp 5	. . . . . . 7 ⊢ ≤ ∈ PosetRel
313		ledm 18779	. . . . . . . 8 ⊢ ℝ* = dom ≤
314	313	psssdm 18771	. . . . . . 7 ⊢ (( ≤ ∈ PosetRel ∧ ( -1[,]1) ⊆ ℝ*) → dom ( ≤ ∩ (( -1[,]1) × ( -1[,]1))) = ( -1[,]1))
315	312, 1, 314	mp2an 705	. . . . . 6 ⊢ dom ( ≤ ∩ (( -1[,]1) × ( -1[,]1))) = ( -1[,]1)
316	315	eqcomi 2772	. . . . 5 ⊢ ( -1[,]1) = dom ( ≤ ∩ (( -1[,]1) × ( -1[,]1)))
317	316, 313	ordthmeo 24136	. . . 4 ⊢ ((( ≤ ∩ (( -1[,]1) × ( -1[,]1))) ∈ V ∧ ≤ ∈ TosetRel ∧ 𝐺 Isom ( ≤ ∩ (( -1[,]1) × ( -1[,]1))), ≤ (( -1[,]1), ℝ*)) → 𝐺 ∈ ((ordTop‘( ≤ ∩ (( -1[,]1) × ( -1[,]1))))Homeo(ordTop‘ ≤ )))
318	304, 302, 310, 317	mp3an 1490	. . 3 ⊢ 𝐺 ∈ ((ordTop‘( ≤ ∩ (( -1[,]1) × ( -1[,]1))))Homeo(ordTop‘ ≤ ))
319		xrhmeo.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘ℂfld)
320		eqid 2763	. . . . . . 7 ⊢ (ordTop‘ ≤ ) = (ordTop‘ ≤ )
321	319, 320	xrrest2 25143	. . . . . 6 ⊢ (( -1[,]1) ⊆ ℝ → (𝐽 ↾t ( -1[,]1)) = ((ordTop‘ ≤ ) ↾t ( -1[,]1)))
322	98, 321	ax-mp 5	. . . . 5 ⊢ (𝐽 ↾t ( -1[,]1)) = ((ordTop‘ ≤ ) ↾t ( -1[,]1))
323		ordtresticc 23556	. . . . 5 ⊢ ((ordTop‘ ≤ ) ↾t ( -1[,]1)) = (ordTop‘( ≤ ∩ (( -1[,]1) × ( -1[,]1))))
324	322, 323	eqtri 2786	. . . 4 ⊢ (𝐽 ↾t ( -1[,]1)) = (ordTop‘( ≤ ∩ (( -1[,]1) × ( -1[,]1))))
325	324	oveq1i 7440	. . 3 ⊢ ((𝐽 ↾t ( -1[,]1))Homeo(ordTop‘ ≤ )) = ((ordTop‘( ≤ ∩ (( -1[,]1) × ( -1[,]1))))Homeo(ordTop‘ ≤ ))
326	318, 325	eleqtrri 2863	. 2 ⊢ 𝐺 ∈ ((𝐽 ↾t ( -1[,]1))Homeo(ordTop‘ ≤ ))
327	301, 326	pm3.2i 476	1 ⊢ (𝐺 Isom < , < (( -1[,]1), ℝ*) ∧ 𝐺 ∈ ((𝐽 ↾t ( -1[,]1))Homeo(ordTop‘ ≤ )))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1569   ∈ wcel 2146  {cab 2741   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  Vcvv 3454   ⊆ wss 3900   ∩ cin 4092  ifcif 4485   class class class wbr 5106   ↦ cmpt 5189   Po wpo 5561   Or wor 5562   × cxp 5653  ^◡ccnv 5654  dom cdm 5655  ran crn 5656  ⟶wf 6543  –onto→wfo 6545  –1-1-onto→wf1o 6546  ‘cfv 6547   Isom wiso 6548  (class class class)co 7430  ℝcr 11212  0cc0 11213  1c1 11214   + caddc 11216  +∞cpnf 11353  ℝ^*cxr 11355   < clt 11356   ≤ cle 11357   − cmin 11554   -cneg 11555   / cdiv 11986   -_ecxne 13251  [,]cicc 13492   ↾_t crest 17606  TopOpenctopn 17607  ordTopcordt 17686  PosetRelcps 18753   TosetRel ctsr 18754  ℂ_fldccnfld 21693  Homeochmeo 24087  IIcii 25211

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761  ax-cnex 11269  ax-resscn 11270  ax-1cn 11271  ax-icn 11272  ax-addcl 11273  ax-addrcl 11274  ax-mulcl 11275  ax-mulrcl 11276  ax-mulcom 11277  ax-addass 11278  ax-mulass 11279  ax-distr 11280  ax-i2m1 11281  ax-1ne0 11282  ax-1rid 11283  ax-rnegex 11284  ax-rrecex 11285  ax-cnre 11286  ax-pre-lttri 11287  ax-pre-lttrn 11288  ax-pre-ltadd 11289  ax-pre-mulgt0 11290  ax-pre-sup 11291

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6311  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-isom 6556  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7888  df-1st 8011  df-2nd 8012  df-frecs 8313  df-wrecs 8344  df-recs 8393  df-rdg 8432  df-1o 8490  df-2o 8491  df-er 8731  df-map 8863  df-en 8988  df-dom 8989  df-sdom 8990  df-fin 8991  df-fi 9416  df-sup 9447  df-inf 9448  df-pnf 11358  df-mnf 11359  df-xr 11360  df-ltxr 11361  df-le 11362  df-sub 11556  df-neg 11557  df-div 11987  df-nn 12349  df-2 12418  df-3 12419  df-4 12420  df-5 12421  df-6 12422  df-7 12423  df-8 12424  df-9 12425  df-n0 12620  df-z 12707  df-dec 12828  df-uz 12979  df-q 13089  df-rp 13134  df-xneg 13254  df-xadd 13255  df-xmul 13256  df-ioo 13493  df-ioc 13494  df-ico 13495  df-icc 13496  df-fz 13653  df-seq 14158  df-exp 14218  df-cj 15281  df-re 15282  df-im 15283  df-sqrt 15417  df-abs 15418  df-struct 17340  df-slot 17375  df-ndx 17387  df-base 17403  df-plusg 17456  df-mulr 17457  df-starv 17458  df-tset 17462  df-ple 17463  df-ds 17465  df-unif 17466  df-rest 17608  df-topn 17609  df-topgen 17629  df-ordt 17688  df-ps 18755  df-tsr 18756  df-psmet 21685  df-xmet 21686  df-met 21687  df-bl 21688  df-mopn 21689  df-cnfld 21694  df-top 23227  df-topon 23244  df-topsp 23266  df-bases 23279  df-cn 23560  df-hmeo 24089  df-xms 24654  df-ms 24655  df-ii 25213

This theorem is used by:  xrhmph  25283