xrhmeo - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xrhmeo		Structured version Visualization version GIF version

Theorem xrhmeo 24877

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 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
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 13367	. . . 4 ⊢ (-1[,]1) ⊆ ℝ^*
2		xrltso 13077	. . . 4 ⊢ < Or ℝ^*
3		soss 5559	. . . 4 ⊢ ((-1[,]1) ⊆ ℝ^* → ( < Or ℝ^* → < Or (-1[,]1)))
4	1, 2, 3	mp2 9	. . 3 ⊢ < Or (-1[,]1)
5		sopo 5558	. . . 4 ⊢ ( < Or ℝ^* → < Po ℝ^*)
6	2, 5	ax-mp 5	. . 3 ⊢ < Po ℝ^*
7		xrhmeo.g	. . . . 5 ⊢ 𝐺 = (𝑦 ∈ (-1[,]1) ↦ if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
8		iccssxr 13367	. . . . . . 7 ⊢ (0[,]+∞) ⊆ ℝ^*
9		neg1rr 12148	. . . . . . . . . . . 12 ⊢ -1 ∈ ℝ
10		1re 11150	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
11	9, 10	elicc2i 13349	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (-1[,]1) ↔ (𝑦 ∈ ℝ ∧ -1 ≤ 𝑦 ∧ 𝑦 ≤ 1))
12	11	simp1bi 1145	. . . . . . . . . 10 ⊢ (𝑦 ∈ (-1[,]1) → 𝑦 ∈ ℝ)
13	12	adantr 480	. . . . . . . . 9 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → 𝑦 ∈ ℝ)
14		simpr 484	. . . . . . . . 9 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → 0 ≤ 𝑦)
15	11	simp3bi 1147	. . . . . . . . . 10 ⊢ (𝑦 ∈ (-1[,]1) → 𝑦 ≤ 1)
16	15	adantr 480	. . . . . . . . 9 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → 𝑦 ≤ 1)
17		elicc01 13403	. . . . . . . . 9 ⊢ (𝑦 ∈ (0[,]1) ↔ (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ∧ 𝑦 ≤ 1))
18	13, 14, 16, 17	syl3anbrc 1344	. . . . . . . 8 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → 𝑦 ∈ (0[,]1))
19		xrhmeo.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))
20	19	iccpnfcnv 24875	. . . . . . . . . . 11 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ^◡𝐹 = (𝑣 ∈ (0[,]+∞) ↦ if(𝑣 = +∞, 1, (𝑣 / (1 + 𝑣)))))
21	20	simpli 483	. . . . . . . . . 10 ⊢ 𝐹:(0[,]1)–1-1-onto→(0[,]+∞)
22		f1of 6782	. . . . . . . . . 10 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → 𝐹:(0[,]1)⟶(0[,]+∞))
23	21, 22	ax-mp 5	. . . . . . . . 9 ⊢ 𝐹:(0[,]1)⟶(0[,]+∞)
24	23	ffvelcdmi 7037	. . . . . . . 8 ⊢ (𝑦 ∈ (0[,]1) → (𝐹‘𝑦) ∈ (0[,]+∞))
25	18, 24	syl 17	. . . . . . 7 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → (𝐹‘𝑦) ∈ (0[,]+∞))
26	8, 25	sselid 3941	. . . . . 6 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → (𝐹‘𝑦) ∈ ℝ^*)
27	12	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → 𝑦 ∈ ℝ)
28	27	renegcld 11581	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ∈ ℝ)
29		0re 11152	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
30		letric 11250	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 ≤ 𝑦 ∨ 𝑦 ≤ 0))
31	29, 12, 30	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (-1[,]1) → (0 ≤ 𝑦 ∨ 𝑦 ≤ 0))
32	31	orcanai 1004	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → 𝑦 ≤ 0)
33	27	le0neg1d 11725	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝑦 ≤ 0 ↔ 0 ≤ -𝑦))
34	32, 33	mpbid 232	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → 0 ≤ -𝑦)
35	11	simp2bi 1146	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (-1[,]1) → -1 ≤ 𝑦)
36	35	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -1 ≤ 𝑦)
37		lenegcon1 11658	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (-1 ≤ 𝑦 ↔ -𝑦 ≤ 1))
38	10, 27, 37	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (-1 ≤ 𝑦 ↔ -𝑦 ≤ 1))
39	36, 38	mpbid 232	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ≤ 1)
40		elicc01 13403	. . . . . . . . . 10 ⊢ (-𝑦 ∈ (0[,]1) ↔ (-𝑦 ∈ ℝ ∧ 0 ≤ -𝑦 ∧ -𝑦 ≤ 1))
41	28, 34, 39, 40	syl3anbrc 1344	. . . . . . . . 9 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ∈ (0[,]1))
42	23	ffvelcdmi 7037	. . . . . . . . 9 ⊢ (-𝑦 ∈ (0[,]1) → (𝐹‘-𝑦) ∈ (0[,]+∞))
43	41, 42	syl 17	. . . . . . . 8 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝐹‘-𝑦) ∈ (0[,]+∞))
44	8, 43	sselid 3941	. . . . . . 7 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝐹‘-𝑦) ∈ ℝ^*)
45	44	xnegcld 13236	. . . . . 6 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -_𝑒(𝐹‘-𝑦) ∈ ℝ^*)
46	26, 45	ifclda 4520	. . . . 5 ⊢ (𝑦 ∈ (-1[,]1) → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ∈ ℝ^*)
47	7, 46	fmpti 7066	. . . 4 ⊢ 𝐺:(-1[,]1)⟶ℝ^*
48		frn 6677	. . . . . 6 ⊢ (𝐺:(-1[,]1)⟶ℝ^* → ran 𝐺 ⊆ ℝ^*)
49	47, 48	ax-mp 5	. . . . 5 ⊢ ran 𝐺 ⊆ ℝ^*
50		ssabral 4025	. . . . . . 7 ⊢ (ℝ^* ⊆ {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))} ↔ ∀𝑧 ∈ ℝ^* ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
51		0le1 11677	. . . . . . . . . . . . 13 ⊢ 0 ≤ 1
52		le0neg2 11663	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ → (0 ≤ 1 ↔ -1 ≤ 0))
53	10, 52	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (0 ≤ 1 ↔ -1 ≤ 0)
54	51, 53	mpbi 230	. . . . . . . . . . . 12 ⊢ -1 ≤ 0
55		1le1 11782	. . . . . . . . . . . 12 ⊢ 1 ≤ 1
56		iccss 13351	. . . . . . . . . . . 12 ⊢ (((-1 ∈ ℝ ∧ 1 ∈ ℝ) ∧ (-1 ≤ 0 ∧ 1 ≤ 1)) → (0[,]1) ⊆ (-1[,]1))
57	9, 10, 54, 55, 56	mp4an 693	. . . . . . . . . . 11 ⊢ (0[,]1) ⊆ (-1[,]1)
58		elxrge0 13394	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (0[,]+∞) ↔ (𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧))
59		f1ocnv 6794	. . . . . . . . . . . . . 14 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → ^◡𝐹:(0[,]+∞)–1-1-onto→(0[,]1))
60		f1of 6782	. . . . . . . . . . . . . 14 ⊢ (^◡𝐹:(0[,]+∞)–1-1-onto→(0[,]1) → ^◡𝐹:(0[,]+∞)⟶(0[,]1))
61	21, 59, 60	mp2b 10	. . . . . . . . . . . . 13 ⊢ ^◡𝐹:(0[,]+∞)⟶(0[,]1)
62	61	ffvelcdmi 7037	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (0[,]+∞) → (^◡𝐹‘𝑧) ∈ (0[,]1))
63	58, 62	sylbir 235	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (^◡𝐹‘𝑧) ∈ (0[,]1))
64	57, 63	sselid 3941	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (^◡𝐹‘𝑧) ∈ (-1[,]1))
65		elicc01 13403	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑧) ∈ (0[,]1) ↔ ((^◡𝐹‘𝑧) ∈ ℝ ∧ 0 ≤ (^◡𝐹‘𝑧) ∧ (^◡𝐹‘𝑧) ≤ 1))
66	65	simp2bi 1146	. . . . . . . . . . 11 ⊢ ((^◡𝐹‘𝑧) ∈ (0[,]1) → 0 ≤ (^◡𝐹‘𝑧))
67	63, 66	syl 17	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → 0 ≤ (^◡𝐹‘𝑧))
68	58	biimpri 228	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → 𝑧 ∈ (0[,]+∞))
69		f1ocnvfv2 7234	. . . . . . . . . . . 12 ⊢ ((𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ 𝑧 ∈ (0[,]+∞)) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
70	21, 68, 69	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
71	70	eqcomd 2735	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))
72		breq2 5106	. . . . . . . . . . . 12 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (0 ≤ 𝑦 ↔ 0 ≤ (^◡𝐹‘𝑧)))
73		fveq2 6840	. . . . . . . . . . . . 13 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝐹‘𝑦) = (𝐹‘(^◡𝐹‘𝑧)))
74	73	eqeq2d 2740	. . . . . . . . . . . 12 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝑧 = (𝐹‘𝑦) ↔ 𝑧 = (𝐹‘(^◡𝐹‘𝑧))))
75	72, 74	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑦 = (^◡𝐹‘𝑧) → ((0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) ↔ (0 ≤ (^◡𝐹‘𝑧) ∧ 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))))
76	75	rspcev 3585	. . . . . . . . . 10 ⊢ (((^◡𝐹‘𝑧) ∈ (-1[,]1) ∧ (0 ≤ (^◡𝐹‘𝑧) ∧ 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))) → ∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)))
77	64, 67, 71, 76	syl12anc 836	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)))
78		iftrue 4490	. . . . . . . . . . . 12 ⊢ (0 ≤ 𝑦 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = (𝐹‘𝑦))
79	78	eqeq2d 2740	. . . . . . . . . . 11 ⊢ (0 ≤ 𝑦 → (𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ↔ 𝑧 = (𝐹‘𝑦)))
80	79	biimpar 477	. . . . . . . . . 10 ⊢ ((0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) → 𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
81	80	reximi 3067	. . . . . . . . 9 ⊢ (∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
82	77, 81	syl 17	. . . . . . . 8 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
83		xnegcl 13149	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ^* → -_𝑒𝑧 ∈ ℝ^*)
84	83	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒𝑧 ∈ ℝ^*)
85		0xr 11197	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ^*
86		xrletri 13089	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) → (0 ≤ 𝑧 ∨ 𝑧 ≤ 0))
87	85, 86	mpan 690	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℝ^* → (0 ≤ 𝑧 ∨ 𝑧 ≤ 0))
88	87	ord 864	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 → 𝑧 ≤ 0))
89		xle0neg1 13157	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℝ^* → (𝑧 ≤ 0 ↔ 0 ≤ -_𝑒𝑧))
90	88, 89	sylibd 239	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 → 0 ≤ -_𝑒𝑧))
91	90	imp 406	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → 0 ≤ -_𝑒𝑧)
92		elxrge0 13394	. . . . . . . . . . . . . . 15 ⊢ (-_𝑒𝑧 ∈ (0[,]+∞) ↔ (-_𝑒𝑧 ∈ ℝ^* ∧ 0 ≤ -_𝑒𝑧))
93	84, 91, 92	sylanbrc 583	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒𝑧 ∈ (0[,]+∞))
94	61	ffvelcdmi 7037	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝑧 ∈ (0[,]+∞) → (^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1))
95	93, 94	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1))
96	57, 95	sselid 3941	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1))
97		iccssre 13366	. . . . . . . . . . . . . . 15 ⊢ ((-1 ∈ ℝ ∧ 1 ∈ ℝ) → (-1[,]1) ⊆ ℝ)
98	9, 10, 97	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (-1[,]1) ⊆ ℝ
99	98, 96	sselid 3941	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℝ)
100		iccneg 13409	. . . . . . . . . . . . . 14 ⊢ ((-1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (^◡𝐹‘-_𝑒𝑧) ∈ ℝ) → ((^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ↔ -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]--1)))
101	9, 10, 100	mp3an12 1453	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹‘-_𝑒𝑧) ∈ ℝ → ((^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ↔ -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]--1)))
102	99, 101	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ↔ -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]--1)))
103	96, 102	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]--1))
104		negneg1e1 12151	. . . . . . . . . . . 12 ⊢ --1 = 1
105	104	oveq2i 7380	. . . . . . . . . . 11 ⊢ (-1[,]--1) = (-1[,]1)
106	103, 105	eleqtrdi 2838	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1))
107		xle0neg2 13158	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℝ^* → (0 ≤ 𝑧 ↔ -_𝑒𝑧 ≤ 0))
108	107	notbid 318	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 ↔ ¬ -_𝑒𝑧 ≤ 0))
109	108	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ -_𝑒𝑧 ≤ 0)
110		f1ocnvfv2 7234	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ -_𝑒𝑧 ∈ (0[,]+∞)) → (𝐹‘(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
111	21, 93, 110	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
112		0elunit 13406	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ (0[,]1)
113		ax-1ne0 11113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ≠ 0
114		neeq2 2988	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 0 → (1 ≠ 𝑥 ↔ 1 ≠ 0))
115	113, 114	mpbiri 258	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 0 → 1 ≠ 𝑥)
116	115	necomd 2980	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → 𝑥 ≠ 1)
117		ifnefalse 4496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ≠ 1 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) = (𝑥 / (1 − 𝑥)))
118	116, 117	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) = (𝑥 / (1 − 𝑥)))
119		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 0 → 𝑥 = 0)
120		oveq2 7377	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 0 → (1 − 𝑥) = (1 − 0))
121		1m0e1 12278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 − 0) = 1
122	120, 121	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 0 → (1 − 𝑥) = 1)
123	119, 122	oveq12d 7387	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → (𝑥 / (1 − 𝑥)) = (0 / 1))
124		ax-1cn 11102	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℂ
125	124, 113	div0i 11892	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 / 1) = 0
126	123, 125	eqtrdi 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → (𝑥 / (1 − 𝑥)) = 0)
127	118, 126	eqtrd 2764	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) = 0)
128		c0ex 11144	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
129	127, 19, 128	fvmpt 6950	. . . . . . . . . . . . . . . 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 5115	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0) ↔ -_𝑒𝑧 ≤ 0))
133	109, 132	mtbird 325	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ (𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0))
134		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ ((ordTop‘ ≤ ) ↾_t (0[,]+∞)) = ((ordTop‘ ≤ ) ↾_t (0[,]+∞))
135	19, 134	iccpnfhmeo 24876	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ 𝐹 ∈ (IIHomeo((ordTop‘ ≤ ) ↾_t (0[,]+∞))))
136	135	simpli 483	. . . . . . . . . . . . . 14 ⊢ 𝐹 Isom < , < ((0[,]1), (0[,]+∞))
137		iccssxr 13367	. . . . . . . . . . . . . . 15 ⊢ (0[,]1) ⊆ ℝ^*
138	137, 8	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ ((0[,]1) ⊆ ℝ^* ∧ (0[,]+∞) ⊆ ℝ^*)
139		leisorel 14401	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ ((0[,]1) ⊆ ℝ^* ∧ (0[,]+∞) ⊆ ℝ^*) ∧ ((^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1) ∧ 0 ∈ (0[,]1))) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ (𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0)))
140	136, 138, 139	mp3an12 1453	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ (𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0)))
141	95, 112, 140	sylancl 586	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ (𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0)))
142	133, 141	mtbird 325	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ (^◡𝐹‘-_𝑒𝑧) ≤ 0)
143	99	le0neg1d 11725	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
144	142, 143	mtbid 324	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧))
145		unitssre 13436	. . . . . . . . . . . . . . . . 17 ⊢ (0[,]1) ⊆ ℝ
146	145, 95	sselid 3941	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℝ)
147	146	recnd 11178	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℂ)
148	147	negnegd 11500	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → --(^◡𝐹‘-_𝑒𝑧) = (^◡𝐹‘-_𝑒𝑧))
149	148	fveq2d 6844	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = (𝐹‘(^◡𝐹‘-_𝑒𝑧)))
150	149, 111	eqtrd 2764	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
151		xnegeq 13143	. . . . . . . . . . . 12 ⊢ ((𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧 → -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒-_𝑒𝑧)
152	150, 151	syl 17	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒-_𝑒𝑧)
153		xnegneg 13150	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ^* → -_𝑒-_𝑒𝑧 = 𝑧)
154	153	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒-_𝑒𝑧 = 𝑧)
155	152, 154	eqtr2d 2765	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
156		breq2 5106	. . . . . . . . . . . . 13 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (0 ≤ 𝑦 ↔ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
157	156	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (¬ 0 ≤ 𝑦 ↔ ¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
158		negeq 11389	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → -𝑦 = --(^◡𝐹‘-_𝑒𝑧))
159	158	fveq2d 6844	. . . . . . . . . . . . . 14 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (𝐹‘-𝑦) = (𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
160		xnegeq 13143	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘-𝑦) = (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
161	159, 160	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
162	161	eqeq2d 2740	. . . . . . . . . . . 12 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (𝑧 = -_𝑒(𝐹‘-𝑦) ↔ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧))))
163	157, 162	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → ((¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)) ↔ (¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧) ∧ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))))
164	163	rspcev 3585	. . . . . . . . . 10 ⊢ ((-(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ∧ (¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧) ∧ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))) → ∃𝑦 ∈ (-1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)))
165	106, 144, 155, 164	syl12anc 836	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)))
166		iffalse 4493	. . . . . . . . . . . 12 ⊢ (¬ 0 ≤ 𝑦 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = -_𝑒(𝐹‘-𝑦))
167	166	eqeq2d 2740	. . . . . . . . . . 11 ⊢ (¬ 0 ≤ 𝑦 → (𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ↔ 𝑧 = -_𝑒(𝐹‘-𝑦)))
168	167	biimpar 477	. . . . . . . . . 10 ⊢ ((¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)) → 𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
169	168	reximi 3067	. . . . . . . . 9 ⊢ (∃𝑦 ∈ (-1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)) → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
170	165, 169	syl 17	. . . . . . . 8 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
171	82, 170	pm2.61dan 812	. . . . . . 7 ⊢ (𝑧 ∈ ℝ^* → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
172	50, 171	mprgbir 3051	. . . . . 6 ⊢ ℝ^* ⊆ {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))}
173	7	rnmpt 5910	. . . . . 6 ⊢ ran 𝐺 = {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))}
174	172, 173	sseqtrri 3993	. . . . 5 ⊢ ℝ^* ⊆ ran 𝐺
175	49, 174	eqssi 3960	. . . 4 ⊢ ran 𝐺 = ℝ^*
176		dffo2 6758	. . . 4 ⊢ (𝐺:(-1[,]1)–onto→ℝ^* ↔ (𝐺:(-1[,]1)⟶ℝ^* ∧ ran 𝐺 = ℝ^*))
177	47, 175, 176	mpbir2an 711	. . 3 ⊢ 𝐺:(-1[,]1)–onto→ℝ^*
178		breq1 5105	. . . . . . 7 ⊢ ((𝐹‘𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) → ((𝐹‘𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
179		breq1 5105	. . . . . . 7 ⊢ (-_𝑒(𝐹‘-𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) → (-_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
180		simpl3 1194	. . . . . . . . 9 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 < 𝑤)
181		simpl1 1192	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ∈ (-1[,]1))
182		simpr 484	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ≤ 𝑧)
183		breq2 5106	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (0 ≤ 𝑦 ↔ 0 ≤ 𝑧))
184		eleq1w 2811	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ (0[,]1) ↔ 𝑧 ∈ (0[,]1)))
185	183, 184	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → ((0 ≤ 𝑦 → 𝑦 ∈ (0[,]1)) ↔ (0 ≤ 𝑧 → 𝑧 ∈ (0[,]1))))
186	18	ex 412	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (-1[,]1) → (0 ≤ 𝑦 → 𝑦 ∈ (0[,]1)))
187	185, 186	vtoclga 3540	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (-1[,]1) → (0 ≤ 𝑧 → 𝑧 ∈ (0[,]1)))
188	181, 182, 187	sylc 65	. . . . . . . . . 10 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ∈ (0[,]1))
189		simpl2 1193	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ (-1[,]1))
190	29	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ∈ ℝ)
191	98, 181	sselid 3941	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ∈ ℝ)
192	98, 189	sselid 3941	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ ℝ)
193	191, 192, 180	ltled 11298	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ≤ 𝑤)
194	190, 191, 192, 182, 193	letrd 11307	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ≤ 𝑤)
195		breq2 5106	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (0 ≤ 𝑦 ↔ 0 ≤ 𝑤))
196		eleq1w 2811	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (0[,]1) ↔ 𝑤 ∈ (0[,]1)))
197	195, 196	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → ((0 ≤ 𝑦 → 𝑦 ∈ (0[,]1)) ↔ (0 ≤ 𝑤 → 𝑤 ∈ (0[,]1))))
198	197, 186	vtoclga 3540	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (-1[,]1) → (0 ≤ 𝑤 → 𝑤 ∈ (0[,]1)))
199	189, 194, 198	sylc 65	. . . . . . . . . 10 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ (0[,]1))
200		isorel 7283	. . . . . . . . . . 11 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1))) → (𝑧 < 𝑤 ↔ (𝐹‘𝑧) < (𝐹‘𝑤)))
201	136, 200	mpan 690	. . . . . . . . . 10 ⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) → (𝑧 < 𝑤 ↔ (𝐹‘𝑧) < (𝐹‘𝑤)))
202	188, 199, 201	syl2anc 584	. . . . . . . . 9 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → (𝑧 < 𝑤 ↔ (𝐹‘𝑧) < (𝐹‘𝑤)))
203	180, 202	mpbid 232	. . . . . . . 8 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → (𝐹‘𝑧) < (𝐹‘𝑤))
204	194	iftrued 4492	. . . . . . . 8 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) = (𝐹‘𝑤))
205	203, 204	breqtrrd 5130	. . . . . . 7 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → (𝐹‘𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
206		breq2 5106	. . . . . . . 8 ⊢ ((𝐹‘𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) → (-_𝑒(𝐹‘-𝑧) < (𝐹‘𝑤) ↔ -_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
207		breq2 5106	. . . . . . . 8 ⊢ (-_𝑒(𝐹‘-𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) → (-_𝑒(𝐹‘-𝑧) < -_𝑒(𝐹‘-𝑤) ↔ -_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
208		simpl1 1192	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → 𝑧 ∈ (-1[,]1))
209		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → ¬ 0 ≤ 𝑧)
210	183	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → (¬ 0 ≤ 𝑦 ↔ ¬ 0 ≤ 𝑧))
211		negeq 11389	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑧 → -𝑦 = -𝑧)
212	211	eleq1d 2813	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → (-𝑦 ∈ (0[,]1) ↔ -𝑧 ∈ (0[,]1)))
213	210, 212	imbi12d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → ((¬ 0 ≤ 𝑦 → -𝑦 ∈ (0[,]1)) ↔ (¬ 0 ≤ 𝑧 → -𝑧 ∈ (0[,]1))))
214	41	ex 412	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (-1[,]1) → (¬ 0 ≤ 𝑦 → -𝑦 ∈ (0[,]1)))
215	213, 214	vtoclga 3540	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (-1[,]1) → (¬ 0 ≤ 𝑧 → -𝑧 ∈ (0[,]1)))
216	208, 209, 215	sylc 65	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → -𝑧 ∈ (0[,]1))
217	216	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -𝑧 ∈ (0[,]1))
218	23	ffvelcdmi 7037	. . . . . . . . . . . 12 ⊢ (-𝑧 ∈ (0[,]1) → (𝐹‘-𝑧) ∈ (0[,]+∞))
219	217, 218	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ (0[,]+∞))
220	8, 219	sselid 3941	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ ℝ^*)
221	220	xnegcld 13236	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -_𝑒(𝐹‘-𝑧) ∈ ℝ^*)
222	85	a1i 11	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 ∈ ℝ^*)
223		simpll2 1214	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑤 ∈ (-1[,]1))
224		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 ≤ 𝑤)
225	223, 224, 198	sylc 65	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑤 ∈ (0[,]1))
226	23	ffvelcdmi 7037	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (0[,]1) → (𝐹‘𝑤) ∈ (0[,]+∞))
227	225, 226	syl 17	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘𝑤) ∈ (0[,]+∞))
228	8, 227	sselid 3941	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘𝑤) ∈ ℝ^*)
229	209	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → ¬ 0 ≤ 𝑧)
230		simpll1 1213	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 ∈ (-1[,]1))
231	98, 230	sselid 3941	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 ∈ ℝ)
232		ltnle 11229	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ ∧ 0 ∈ ℝ) → (𝑧 < 0 ↔ ¬ 0 ≤ 𝑧))
233	231, 29, 232	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝑧 < 0 ↔ ¬ 0 ≤ 𝑧))
234	229, 233	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 < 0)
235	231	lt0neg1d 11723	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝑧 < 0 ↔ 0 < -𝑧))
236	234, 235	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 < -𝑧)
237		isorel 7283	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (0 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1))) → (0 < -𝑧 ↔ (𝐹‘0) < (𝐹‘-𝑧)))
238	136, 237	mpan 690	. . . . . . . . . . . . 13 ⊢ ((0 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1)) → (0 < -𝑧 ↔ (𝐹‘0) < (𝐹‘-𝑧)))
239	112, 217, 238	sylancr 587	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (0 < -𝑧 ↔ (𝐹‘0) < (𝐹‘-𝑧)))
240	236, 239	mpbid 232	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘0) < (𝐹‘-𝑧))
241	130, 240	eqbrtrrid 5138	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 < (𝐹‘-𝑧))
242		xlt0neg2 13156	. . . . . . . . . . 11 ⊢ ((𝐹‘-𝑧) ∈ ℝ^* → (0 < (𝐹‘-𝑧) ↔ -_𝑒(𝐹‘-𝑧) < 0))
243	220, 242	syl 17	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (0 < (𝐹‘-𝑧) ↔ -_𝑒(𝐹‘-𝑧) < 0))
244	241, 243	mpbid 232	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -_𝑒(𝐹‘-𝑧) < 0)
245		elxrge0 13394	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑤) ∈ (0[,]+∞) ↔ ((𝐹‘𝑤) ∈ ℝ^* ∧ 0 ≤ (𝐹‘𝑤)))
246	245	simprbi 496	. . . . . . . . . 10 ⊢ ((𝐹‘𝑤) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝑤))
247	227, 246	syl 17	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 ≤ (𝐹‘𝑤))
248	221, 222, 228, 244, 247	xrltletrd 13097	. . . . . . . 8 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -_𝑒(𝐹‘-𝑧) < (𝐹‘𝑤))
249		simpll3 1215	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑧 < 𝑤)
250		simpll1 1213	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑧 ∈ (-1[,]1))
251	98, 250	sselid 3941	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑧 ∈ ℝ)
252		simpll2 1214	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑤 ∈ (-1[,]1))
253	98, 252	sselid 3941	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑤 ∈ ℝ)
254	251, 253	ltnegd 11732	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝑧 < 𝑤 ↔ -𝑤 < -𝑧))
255	249, 254	mpbid 232	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -𝑤 < -𝑧)
256		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → ¬ 0 ≤ 𝑤)
257	195	notbid 318	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (¬ 0 ≤ 𝑦 ↔ ¬ 0 ≤ 𝑤))
258		negeq 11389	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → -𝑦 = -𝑤)
259	258	eleq1d 2813	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (-𝑦 ∈ (0[,]1) ↔ -𝑤 ∈ (0[,]1)))
260	257, 259	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((¬ 0 ≤ 𝑦 → -𝑦 ∈ (0[,]1)) ↔ (¬ 0 ≤ 𝑤 → -𝑤 ∈ (0[,]1))))
261	260, 214	vtoclga 3540	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ (-1[,]1) → (¬ 0 ≤ 𝑤 → -𝑤 ∈ (0[,]1)))
262	252, 256, 261	sylc 65	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -𝑤 ∈ (0[,]1))
263	216	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -𝑧 ∈ (0[,]1))
264		isorel 7283	. . . . . . . . . . . 12 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (-𝑤 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1))) → (-𝑤 < -𝑧 ↔ (𝐹‘-𝑤) < (𝐹‘-𝑧)))
265	136, 264	mpan 690	. . . . . . . . . . 11 ⊢ ((-𝑤 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1)) → (-𝑤 < -𝑧 ↔ (𝐹‘-𝑤) < (𝐹‘-𝑧)))
266	262, 263, 265	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (-𝑤 < -𝑧 ↔ (𝐹‘-𝑤) < (𝐹‘-𝑧)))
267	255, 266	mpbid 232	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑤) < (𝐹‘-𝑧))
268	23	ffvelcdmi 7037	. . . . . . . . . . . 12 ⊢ (-𝑤 ∈ (0[,]1) → (𝐹‘-𝑤) ∈ (0[,]+∞))
269	262, 268	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑤) ∈ (0[,]+∞))
270	8, 269	sselid 3941	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑤) ∈ ℝ^*)
271	263, 218	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ (0[,]+∞))
272	8, 271	sselid 3941	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ ℝ^*)
273		xltneg 13153	. . . . . . . . . 10 ⊢ (((𝐹‘-𝑤) ∈ ℝ^* ∧ (𝐹‘-𝑧) ∈ ℝ^*) → ((𝐹‘-𝑤) < (𝐹‘-𝑧) ↔ -_𝑒(𝐹‘-𝑧) < -_𝑒(𝐹‘-𝑤)))
274	270, 272, 273	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → ((𝐹‘-𝑤) < (𝐹‘-𝑧) ↔ -_𝑒(𝐹‘-𝑧) < -_𝑒(𝐹‘-𝑤)))
275	267, 274	mpbid 232	. . . . . . . 8 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -_𝑒(𝐹‘-𝑧) < -_𝑒(𝐹‘-𝑤))
276	206, 207, 248, 275	ifbothda 4523	. . . . . . 7 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → -_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
277	178, 179, 205, 276	ifbothda 4523	. . . . . 6 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) → if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
278	277	3expia 1121	. . . . 5 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → (𝑧 < 𝑤 → if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
279		fveq2 6840	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
280	211	fveq2d 6844	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝐹‘-𝑦) = (𝐹‘-𝑧))
281		xnegeq 13143	. . . . . . . . 9 ⊢ ((𝐹‘-𝑦) = (𝐹‘-𝑧) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑧))
282	280, 281	syl 17	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑧))
283	183, 279, 282	ifbieq12d 4513	. . . . . . 7 ⊢ (𝑦 = 𝑧 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)))
284		fvex 6853	. . . . . . . 8 ⊢ (𝐹‘𝑧) ∈ V
285		xnegex 13144	. . . . . . . 8 ⊢ -_𝑒(𝐹‘-𝑧) ∈ V
286	284, 285	ifex 4535	. . . . . . 7 ⊢ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) ∈ V
287	283, 7, 286	fvmpt 6950	. . . . . 6 ⊢ (𝑧 ∈ (-1[,]1) → (𝐺‘𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)))
288		fveq2 6840	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
289	258	fveq2d 6844	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝐹‘-𝑦) = (𝐹‘-𝑤))
290		xnegeq 13143	. . . . . . . . 9 ⊢ ((𝐹‘-𝑦) = (𝐹‘-𝑤) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑤))
291	289, 290	syl 17	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑤))
292	195, 288, 291	ifbieq12d 4513	. . . . . . 7 ⊢ (𝑦 = 𝑤 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
293		fvex 6853	. . . . . . . 8 ⊢ (𝐹‘𝑤) ∈ V
294		xnegex 13144	. . . . . . . 8 ⊢ -_𝑒(𝐹‘-𝑤) ∈ V
295	293, 294	ifex 4535	. . . . . . 7 ⊢ if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) ∈ V
296	292, 7, 295	fvmpt 6950	. . . . . 6 ⊢ (𝑤 ∈ (-1[,]1) → (𝐺‘𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
297	287, 296	breqan12d 5118	. . . . 5 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → ((𝐺‘𝑧) < (𝐺‘𝑤) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
298	278, 297	sylibrd 259	. . . 4 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → (𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤)))
299	298	rgen2 3175	. . 3 ⊢ ∀𝑧 ∈ (-1[,]1)∀𝑤 ∈ (-1[,]1)(𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤))
300		soisoi 7285	. . 3 ⊢ ((( < Or (-1[,]1) ∧ < Po ℝ^) ∧ (𝐺:(-1[,]1)–onto→ℝ^ ∧ ∀𝑧 ∈ (-1[,]1)∀𝑤 ∈ (-1[,]1)(𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤)))) → 𝐺 Isom < , < ((-1[,]1), ℝ^*))
301	4, 6, 177, 299, 300	mp4an 693	. 2 ⊢ 𝐺 Isom < , < ((-1[,]1), ℝ^*)
302		letsr 18534	. . . . . 6 ⊢ ≤ ∈ TosetRel
303	302	elexi 3467	. . . . 5 ⊢ ≤ ∈ V
304	303	inex1 5267	. . . 4 ⊢ ( ≤ ∩ ((-1[,]1) × (-1[,]1))) ∈ V
305		ssid 3966	. . . . . . 7 ⊢ ℝ^* ⊆ ℝ^*
306		leiso 14400	. . . . . . 7 ⊢ (((-1[,]1) ⊆ ℝ^* ∧ ℝ^* ⊆ ℝ^) → (𝐺 Isom < , < ((-1[,]1), ℝ^) ↔ 𝐺 Isom ≤ , ≤ ((-1[,]1), ℝ^*)))
307	1, 305, 306	mp2an 692	. . . . . 6 ⊢ (𝐺 Isom < , < ((-1[,]1), ℝ^) ↔ 𝐺 Isom ≤ , ≤ ((-1[,]1), ℝ^))
308	301, 307	mpbi 230	. . . . 5 ⊢ 𝐺 Isom ≤ , ≤ ((-1[,]1), ℝ^*)
309		isores1 7291	. . . . 5 ⊢ (𝐺 Isom ≤ , ≤ ((-1[,]1), ℝ^) ↔ 𝐺 Isom ( ≤ ∩ ((-1[,]1) × (-1[,]1))), ≤ ((-1[,]1), ℝ^))
310	308, 309	mpbi 230	. . . 4 ⊢ 𝐺 Isom ( ≤ ∩ ((-1[,]1) × (-1[,]1))), ≤ ((-1[,]1), ℝ^*)
311		tsrps 18528	. . . . . . . 8 ⊢ ( ≤ ∈ TosetRel → ≤ ∈ PosetRel)
312	302, 311	ax-mp 5	. . . . . . 7 ⊢ ≤ ∈ PosetRel
313		ledm 18531	. . . . . . . 8 ⊢ ℝ^* = dom ≤
314	313	psssdm 18523	. . . . . . 7 ⊢ (( ≤ ∈ PosetRel ∧ (-1[,]1) ⊆ ℝ^*) → dom ( ≤ ∩ ((-1[,]1) × (-1[,]1))) = (-1[,]1))
315	312, 1, 314	mp2an 692	. . . . . 6 ⊢ dom ( ≤ ∩ ((-1[,]1) × (-1[,]1))) = (-1[,]1)
316	315	eqcomi 2738	. . . . 5 ⊢ (-1[,]1) = dom ( ≤ ∩ ((-1[,]1) × (-1[,]1)))
317	316, 313	ordthmeo 23722	. . . 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 1463	. . 3 ⊢ 𝐺 ∈ ((ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))Homeo(ordTop‘ ≤ ))
319		xrhmeo.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
320		eqid 2729	. . . . . . 7 ⊢ (ordTop‘ ≤ ) = (ordTop‘ ≤ )
321	319, 320	xrrest2 24730	. . . . . 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 23143	. . . . 5 ⊢ ((ordTop‘ ≤ ) ↾_t (-1[,]1)) = (ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))
324	322, 323	eqtri 2752	. . . 4 ⊢ (𝐽 ↾_t (-1[,]1)) = (ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))
325	324	oveq1i 7379	. . 3 ⊢ ((𝐽 ↾_t (-1[,]1))Homeo(ordTop‘ ≤ )) = ((ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))Homeo(ordTop‘ ≤ ))
326	318, 325	eleqtrri 2827	. 2 ⊢ 𝐺 ∈ ((𝐽 ↾_t (-1[,]1))Homeo(ordTop‘ ≤ ))
327	301, 326	pm3.2i 470	1 ⊢ (𝐺 Isom < , < ((-1[,]1), ℝ^*) ∧ 𝐺 ∈ ((𝐽 ↾_t (-1[,]1))Homeo(ordTop‘ ≤ )))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 {cab 2707 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 Vcvv 3444 ∩ cin 3910 ⊆ wss 3911 ifcif 4484 class class class wbr 5102 ↦ cmpt 5183 Po wpo 5537 Or wor 5538 × cxp 5629 ^◡ccnv 5630 dom cdm 5631 ran crn 5632 ⟶wf 6495 –onto→wfo 6497 –1-1-onto→wf1o 6498 ‘cfv 6499 Isom wiso 6500 (class class class)co 7369 ℝcr 11043 0cc0 11044 1c1 11045 + caddc 11047 +∞cpnf 11181 ℝ^*cxr 11183 < clt 11184 ≤ cle 11185 − cmin 11381 -cneg 11382 / cdiv 11811 -_𝑒cxne 13045 [,]cicc 13285 ↾_t crest 17359 TopOpenctopn 17360 ordTopcordt 17438 PosetRelcps 18505 TosetRel ctsr 18506 ℂ_fldccnfld 21296 Homeochmeo 23673 IIcii 24801

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-2o 8412 df-er 8648 df-map 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fi 9338 df-sup 9369 df-inf 9370 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-4 12227 df-5 12228 df-6 12229 df-7 12230 df-8 12231 df-9 12232 df-n0 12419 df-z 12506 df-dec 12626 df-uz 12770 df-q 12884 df-rp 12928 df-xneg 13048 df-xadd 13049 df-xmul 13050 df-ioo 13286 df-ioc 13287 df-ico 13288 df-icc 13289 df-fz 13445 df-seq 13943 df-exp 14003 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-struct 17093 df-slot 17128 df-ndx 17140 df-base 17156 df-plusg 17209 df-mulr 17210 df-starv 17211 df-tset 17215 df-ple 17216 df-ds 17218 df-unif 17219 df-rest 17361 df-topn 17362 df-topgen 17382 df-ordt 17440 df-ps 18507 df-tsr 18508 df-psmet 21288 df-xmet 21289 df-met 21290 df-bl 21291 df-mopn 21292 df-cnfld 21297 df-top 22814 df-topon 22831 df-topsp 22853 df-bases 22866 df-cn 23147 df-hmeo 23675 df-xms 24241 df-ms 24242 df-ii 24803

This theorem is referenced by: xrhmph 24878

W3C validator