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 24978

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 13471	. . . 4 ⊢ (-1[,]1) ⊆ ℝ^*
2		xrltso 13184	. . . 4 ⊢ < Or ℝ^*
3		soss 5611	. . . 4 ⊢ ((-1[,]1) ⊆ ℝ^* → ( < Or ℝ^* → < Or (-1[,]1)))
4	1, 2, 3	mp2 9	. . 3 ⊢ < Or (-1[,]1)
5		sopo 5610	. . . 4 ⊢ ( < Or ℝ^* → < Po ℝ^*)
6	2, 5	ax-mp 5	. . 3 ⊢ < Po ℝ^*
7		xrhmeo.g	. . . . 5 ⊢ 𝐺 = (𝑦 ∈ (-1[,]1) ↦ if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
8		iccssxr 13471	. . . . . . 7 ⊢ (0[,]+∞) ⊆ ℝ^*
9		neg1rr 12382	. . . . . . . . . . . 12 ⊢ -1 ∈ ℝ
10		1re 11262	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
11	9, 10	elicc2i 13454	. . . . . . . . . . 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 13507	. . . . . . . . 9 ⊢ (𝑦 ∈ (0[,]1) ↔ (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ∧ 𝑦 ≤ 1))
18	13, 14, 16, 17	syl3anbrc 1343	. . . . . . . 8 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → 𝑦 ∈ (0[,]1))
19		xrhmeo.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))
20	19	iccpnfcnv 24976	. . . . . . . . . . 11 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ^◡𝐹 = (𝑣 ∈ (0[,]+∞) ↦ if(𝑣 = +∞, 1, (𝑣 / (1 + 𝑣)))))
21	20	simpli 483	. . . . . . . . . 10 ⊢ 𝐹:(0[,]1)–1-1-onto→(0[,]+∞)
22		f1of 6847	. . . . . . . . . 10 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → 𝐹:(0[,]1)⟶(0[,]+∞))
23	21, 22	ax-mp 5	. . . . . . . . 9 ⊢ 𝐹:(0[,]1)⟶(0[,]+∞)
24	23	ffvelcdmi 7102	. . . . . . . 8 ⊢ (𝑦 ∈ (0[,]1) → (𝐹‘𝑦) ∈ (0[,]+∞))
25	18, 24	syl 17	. . . . . . 7 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → (𝐹‘𝑦) ∈ (0[,]+∞))
26	8, 25	sselid 3980	. . . . . 6 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → (𝐹‘𝑦) ∈ ℝ^*)
27	12	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → 𝑦 ∈ ℝ)
28	27	renegcld 11691	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ∈ ℝ)
29		0re 11264	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
30		letric 11362	. . . . . . . . . . . . 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 11835	. . . . . . . . . . 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 11768	. . . . . . . . . . . 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 13507	. . . . . . . . . 10 ⊢ (-𝑦 ∈ (0[,]1) ↔ (-𝑦 ∈ ℝ ∧ 0 ≤ -𝑦 ∧ -𝑦 ≤ 1))
41	28, 34, 39, 40	syl3anbrc 1343	. . . . . . . . 9 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ∈ (0[,]1))
42	23	ffvelcdmi 7102	. . . . . . . . 9 ⊢ (-𝑦 ∈ (0[,]1) → (𝐹‘-𝑦) ∈ (0[,]+∞))
43	41, 42	syl 17	. . . . . . . 8 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝐹‘-𝑦) ∈ (0[,]+∞))
44	8, 43	sselid 3980	. . . . . . 7 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝐹‘-𝑦) ∈ ℝ^*)
45	44	xnegcld 13343	. . . . . 6 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -_𝑒(𝐹‘-𝑦) ∈ ℝ^*)
46	26, 45	ifclda 4560	. . . . 5 ⊢ (𝑦 ∈ (-1[,]1) → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ∈ ℝ^*)
47	7, 46	fmpti 7131	. . . 4 ⊢ 𝐺:(-1[,]1)⟶ℝ^*
48		frn 6742	. . . . . 6 ⊢ (𝐺:(-1[,]1)⟶ℝ^* → ran 𝐺 ⊆ ℝ^*)
49	47, 48	ax-mp 5	. . . . 5 ⊢ ran 𝐺 ⊆ ℝ^*
50		ssabral 4064	. . . . . . 7 ⊢ (ℝ^* ⊆ {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))} ↔ ∀𝑧 ∈ ℝ^* ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
51		0le1 11787	. . . . . . . . . . . . 13 ⊢ 0 ≤ 1
52		le0neg2 11773	. . . . . . . . . . . . . 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 11892	. . . . . . . . . . . 12 ⊢ 1 ≤ 1
56		iccss 13456	. . . . . . . . . . . 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 13498	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (0[,]+∞) ↔ (𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧))
59		f1ocnv 6859	. . . . . . . . . . . . . 14 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → ^◡𝐹:(0[,]+∞)–1-1-onto→(0[,]1))
60		f1of 6847	. . . . . . . . . . . . . 14 ⊢ (^◡𝐹:(0[,]+∞)–1-1-onto→(0[,]1) → ^◡𝐹:(0[,]+∞)⟶(0[,]1))
61	21, 59, 60	mp2b 10	. . . . . . . . . . . . 13 ⊢ ^◡𝐹:(0[,]+∞)⟶(0[,]1)
62	61	ffvelcdmi 7102	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (0[,]+∞) → (^◡𝐹‘𝑧) ∈ (0[,]1))
63	58, 62	sylbir 235	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (^◡𝐹‘𝑧) ∈ (0[,]1))
64	57, 63	sselid 3980	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (^◡𝐹‘𝑧) ∈ (-1[,]1))
65		elicc01 13507	. . . . . . . . . . . 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 7298	. . . . . . . . . . . 12 ⊢ ((𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ 𝑧 ∈ (0[,]+∞)) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
70	21, 68, 69	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
71	70	eqcomd 2742	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))
72		breq2 5146	. . . . . . . . . . . 12 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (0 ≤ 𝑦 ↔ 0 ≤ (^◡𝐹‘𝑧)))
73		fveq2 6905	. . . . . . . . . . . . 13 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝐹‘𝑦) = (𝐹‘(^◡𝐹‘𝑧)))
74	73	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝑧 = (𝐹‘𝑦) ↔ 𝑧 = (𝐹‘(^◡𝐹‘𝑧))))
75	72, 74	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑦 = (^◡𝐹‘𝑧) → ((0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) ↔ (0 ≤ (^◡𝐹‘𝑧) ∧ 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))))
76	75	rspcev 3621	. . . . . . . . . 10 ⊢ (((^◡𝐹‘𝑧) ∈ (-1[,]1) ∧ (0 ≤ (^◡𝐹‘𝑧) ∧ 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))) → ∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)))
77	64, 67, 71, 76	syl12anc 836	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)))
78		iftrue 4530	. . . . . . . . . . . 12 ⊢ (0 ≤ 𝑦 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = (𝐹‘𝑦))
79	78	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (0 ≤ 𝑦 → (𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ↔ 𝑧 = (𝐹‘𝑦)))
80	79	biimpar 477	. . . . . . . . . 10 ⊢ ((0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) → 𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
81	80	reximi 3083	. . . . . . . . 9 ⊢ (∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
82	77, 81	syl 17	. . . . . . . 8 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
83		xnegcl 13256	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ^* → -_𝑒𝑧 ∈ ℝ^*)
84	83	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒𝑧 ∈ ℝ^*)
85		0xr 11309	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ^*
86		xrletri 13196	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) → (0 ≤ 𝑧 ∨ 𝑧 ≤ 0))
87	85, 86	mpan 690	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℝ^* → (0 ≤ 𝑧 ∨ 𝑧 ≤ 0))
88	87	ord 864	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 → 𝑧 ≤ 0))
89		xle0neg1 13264	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℝ^* → (𝑧 ≤ 0 ↔ 0 ≤ -_𝑒𝑧))
90	88, 89	sylibd 239	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 → 0 ≤ -_𝑒𝑧))
91	90	imp 406	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → 0 ≤ -_𝑒𝑧)
92		elxrge0 13498	. . . . . . . . . . . . . . 15 ⊢ (-_𝑒𝑧 ∈ (0[,]+∞) ↔ (-_𝑒𝑧 ∈ ℝ^* ∧ 0 ≤ -_𝑒𝑧))
93	84, 91, 92	sylanbrc 583	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒𝑧 ∈ (0[,]+∞))
94	61	ffvelcdmi 7102	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝑧 ∈ (0[,]+∞) → (^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1))
95	93, 94	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1))
96	57, 95	sselid 3980	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1))
97		iccssre 13470	. . . . . . . . . . . . . . 15 ⊢ ((-1 ∈ ℝ ∧ 1 ∈ ℝ) → (-1[,]1) ⊆ ℝ)
98	9, 10, 97	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (-1[,]1) ⊆ ℝ
99	98, 96	sselid 3980	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℝ)
100		iccneg 13513	. . . . . . . . . . . . . 14 ⊢ ((-1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (^◡𝐹‘-_𝑒𝑧) ∈ ℝ) → ((^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ↔ -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]--1)))
101	9, 10, 100	mp3an12 1452	. . . . . . . . . . . . 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 12385	. . . . . . . . . . . 12 ⊢ --1 = 1
105	104	oveq2i 7443	. . . . . . . . . . 11 ⊢ (-1[,]--1) = (-1[,]1)
106	103, 105	eleqtrdi 2850	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1))
107		xle0neg2 13265	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℝ^* → (0 ≤ 𝑧 ↔ -_𝑒𝑧 ≤ 0))
108	107	notbid 318	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 ↔ ¬ -_𝑒𝑧 ≤ 0))
109	108	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ -_𝑒𝑧 ≤ 0)
110		f1ocnvfv2 7298	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ -_𝑒𝑧 ∈ (0[,]+∞)) → (𝐹‘(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
111	21, 93, 110	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
112		0elunit 13510	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ (0[,]1)
113		ax-1ne0 11225	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ≠ 0
114		neeq2 3003	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 0 → (1 ≠ 𝑥 ↔ 1 ≠ 0))
115	113, 114	mpbiri 258	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 0 → 1 ≠ 𝑥)
116	115	necomd 2995	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → 𝑥 ≠ 1)
117		ifnefalse 4536	. . . . . . . . . . . . . . . . . . 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 7440	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 0 → (1 − 𝑥) = (1 − 0))
121		1m0e1 12388	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 − 0) = 1
122	120, 121	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 0 → (1 − 𝑥) = 1)
123	119, 122	oveq12d 7450	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → (𝑥 / (1 − 𝑥)) = (0 / 1))
124		ax-1cn 11214	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℂ
125	124, 113	div0i 12002	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 / 1) = 0
126	123, 125	eqtrdi 2792	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → (𝑥 / (1 − 𝑥)) = 0)
127	118, 126	eqtrd 2776	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) = 0)
128		c0ex 11256	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
129	127, 19, 128	fvmpt 7015	. . . . . . . . . . . . . . . 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 5155	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0) ↔ -_𝑒𝑧 ≤ 0))
133	109, 132	mtbird 325	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ (𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0))
134		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ ((ordTop‘ ≤ ) ↾_t (0[,]+∞)) = ((ordTop‘ ≤ ) ↾_t (0[,]+∞))
135	19, 134	iccpnfhmeo 24977	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ 𝐹 ∈ (IIHomeo((ordTop‘ ≤ ) ↾_t (0[,]+∞))))
136	135	simpli 483	. . . . . . . . . . . . . 14 ⊢ 𝐹 Isom < , < ((0[,]1), (0[,]+∞))
137		iccssxr 13471	. . . . . . . . . . . . . . 15 ⊢ (0[,]1) ⊆ ℝ^*
138	137, 8	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ ((0[,]1) ⊆ ℝ^* ∧ (0[,]+∞) ⊆ ℝ^*)
139		leisorel 14500	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ ((0[,]1) ⊆ ℝ^* ∧ (0[,]+∞) ⊆ ℝ^*) ∧ ((^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1) ∧ 0 ∈ (0[,]1))) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ (𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0)))
140	136, 138, 139	mp3an12 1452	. . . . . . . . . . . . 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 11835	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
144	142, 143	mtbid 324	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧))
145		unitssre 13540	. . . . . . . . . . . . . . . . 17 ⊢ (0[,]1) ⊆ ℝ
146	145, 95	sselid 3980	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℝ)
147	146	recnd 11290	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℂ)
148	147	negnegd 11612	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → --(^◡𝐹‘-_𝑒𝑧) = (^◡𝐹‘-_𝑒𝑧))
149	148	fveq2d 6909	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = (𝐹‘(^◡𝐹‘-_𝑒𝑧)))
150	149, 111	eqtrd 2776	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
151		xnegeq 13250	. . . . . . . . . . . 12 ⊢ ((𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧 → -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒-_𝑒𝑧)
152	150, 151	syl 17	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒-_𝑒𝑧)
153		xnegneg 13257	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ^* → -_𝑒-_𝑒𝑧 = 𝑧)
154	153	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒-_𝑒𝑧 = 𝑧)
155	152, 154	eqtr2d 2777	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
156		breq2 5146	. . . . . . . . . . . . 13 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (0 ≤ 𝑦 ↔ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
157	156	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (¬ 0 ≤ 𝑦 ↔ ¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
158		negeq 11501	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → -𝑦 = --(^◡𝐹‘-_𝑒𝑧))
159	158	fveq2d 6909	. . . . . . . . . . . . . 14 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (𝐹‘-𝑦) = (𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
160		xnegeq 13250	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘-𝑦) = (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
161	159, 160	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
162	161	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (𝑧 = -_𝑒(𝐹‘-𝑦) ↔ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧))))
163	157, 162	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → ((¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)) ↔ (¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧) ∧ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))))
164	163	rspcev 3621	. . . . . . . . . 10 ⊢ ((-(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ∧ (¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧) ∧ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))) → ∃𝑦 ∈ (-1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)))
165	106, 144, 155, 164	syl12anc 836	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)))
166		iffalse 4533	. . . . . . . . . . . 12 ⊢ (¬ 0 ≤ 𝑦 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = -_𝑒(𝐹‘-𝑦))
167	166	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (¬ 0 ≤ 𝑦 → (𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ↔ 𝑧 = -_𝑒(𝐹‘-𝑦)))
168	167	biimpar 477	. . . . . . . . . 10 ⊢ ((¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)) → 𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
169	168	reximi 3083	. . . . . . . . 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 3067	. . . . . 6 ⊢ ℝ^* ⊆ {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))}
173	7	rnmpt 5967	. . . . . 6 ⊢ ran 𝐺 = {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))}
174	172, 173	sseqtrri 4032	. . . . 5 ⊢ ℝ^* ⊆ ran 𝐺
175	49, 174	eqssi 3999	. . . 4 ⊢ ran 𝐺 = ℝ^*
176		dffo2 6823	. . . 4 ⊢ (𝐺:(-1[,]1)–onto→ℝ^* ↔ (𝐺:(-1[,]1)⟶ℝ^* ∧ ran 𝐺 = ℝ^*))
177	47, 175, 176	mpbir2an 711	. . 3 ⊢ 𝐺:(-1[,]1)–onto→ℝ^*
178		breq1 5145	. . . . . . 7 ⊢ ((𝐹‘𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) → ((𝐹‘𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
179		breq1 5145	. . . . . . 7 ⊢ (-_𝑒(𝐹‘-𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) → (-_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
180		simpl3 1193	. . . . . . . . 9 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 < 𝑤)
181		simpl1 1191	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ∈ (-1[,]1))
182		simpr 484	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ≤ 𝑧)
183		breq2 5146	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (0 ≤ 𝑦 ↔ 0 ≤ 𝑧))
184		eleq1w 2823	. . . . . . . . . . . . 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 3576	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (-1[,]1) → (0 ≤ 𝑧 → 𝑧 ∈ (0[,]1)))
188	181, 182, 187	sylc 65	. . . . . . . . . 10 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ∈ (0[,]1))
189		simpl2 1192	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ (-1[,]1))
190	29	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ∈ ℝ)
191	98, 181	sselid 3980	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ∈ ℝ)
192	98, 189	sselid 3980	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ ℝ)
193	191, 192, 180	ltled 11410	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ≤ 𝑤)
194	190, 191, 192, 182, 193	letrd 11419	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ≤ 𝑤)
195		breq2 5146	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (0 ≤ 𝑦 ↔ 0 ≤ 𝑤))
196		eleq1w 2823	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (0[,]1) ↔ 𝑤 ∈ (0[,]1)))
197	195, 196	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → ((0 ≤ 𝑦 → 𝑦 ∈ (0[,]1)) ↔ (0 ≤ 𝑤 → 𝑤 ∈ (0[,]1))))
198	197, 186	vtoclga 3576	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (-1[,]1) → (0 ≤ 𝑤 → 𝑤 ∈ (0[,]1)))
199	189, 194, 198	sylc 65	. . . . . . . . . 10 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ (0[,]1))
200		isorel 7347	. . . . . . . . . . 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 4532	. . . . . . . 8 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) = (𝐹‘𝑤))
205	203, 204	breqtrrd 5170	. . . . . . 7 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → (𝐹‘𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
206		breq2 5146	. . . . . . . 8 ⊢ ((𝐹‘𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) → (-_𝑒(𝐹‘-𝑧) < (𝐹‘𝑤) ↔ -_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
207		breq2 5146	. . . . . . . 8 ⊢ (-_𝑒(𝐹‘-𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) → (-_𝑒(𝐹‘-𝑧) < -_𝑒(𝐹‘-𝑤) ↔ -_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
208		simpl1 1191	. . . . . . . . . . . . . 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 11501	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑧 → -𝑦 = -𝑧)
212	211	eleq1d 2825	. . . . . . . . . . . . . . . 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 3576	. . . . . . . . . . . . . 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 7102	. . . . . . . . . . . 12 ⊢ (-𝑧 ∈ (0[,]1) → (𝐹‘-𝑧) ∈ (0[,]+∞))
219	217, 218	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ (0[,]+∞))
220	8, 219	sselid 3980	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ ℝ^*)
221	220	xnegcld 13343	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -_𝑒(𝐹‘-𝑧) ∈ ℝ^*)
222	85	a1i 11	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 ∈ ℝ^*)
223		simpll2 1213	. . . . . . . . . . . 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 7102	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (0[,]1) → (𝐹‘𝑤) ∈ (0[,]+∞))
227	225, 226	syl 17	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘𝑤) ∈ (0[,]+∞))
228	8, 227	sselid 3980	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘𝑤) ∈ ℝ^*)
229	209	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → ¬ 0 ≤ 𝑧)
230		simpll1 1212	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 ∈ (-1[,]1))
231	98, 230	sselid 3980	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 ∈ ℝ)
232		ltnle 11341	. . . . . . . . . . . . . . 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 11833	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝑧 < 0 ↔ 0 < -𝑧))
236	234, 235	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 < -𝑧)
237		isorel 7347	. . . . . . . . . . . . . 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 5178	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 < (𝐹‘-𝑧))
242		xlt0neg2 13263	. . . . . . . . . . 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 13498	. . . . . . . . . . 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 13204	. . . . . . . 8 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -_𝑒(𝐹‘-𝑧) < (𝐹‘𝑤))
249		simpll3 1214	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑧 < 𝑤)
250		simpll1 1212	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑧 ∈ (-1[,]1))
251	98, 250	sselid 3980	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑧 ∈ ℝ)
252		simpll2 1213	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑤 ∈ (-1[,]1))
253	98, 252	sselid 3980	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑤 ∈ ℝ)
254	251, 253	ltnegd 11842	. . . . . . . . . . 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 11501	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → -𝑦 = -𝑤)
259	258	eleq1d 2825	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (-𝑦 ∈ (0[,]1) ↔ -𝑤 ∈ (0[,]1)))
260	257, 259	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((¬ 0 ≤ 𝑦 → -𝑦 ∈ (0[,]1)) ↔ (¬ 0 ≤ 𝑤 → -𝑤 ∈ (0[,]1))))
261	260, 214	vtoclga 3576	. . . . . . . . . . . 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 7347	. . . . . . . . . . . 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 7102	. . . . . . . . . . . 12 ⊢ (-𝑤 ∈ (0[,]1) → (𝐹‘-𝑤) ∈ (0[,]+∞))
269	262, 268	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑤) ∈ (0[,]+∞))
270	8, 269	sselid 3980	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑤) ∈ ℝ^*)
271	263, 218	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ (0[,]+∞))
272	8, 271	sselid 3980	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ ℝ^*)
273		xltneg 13260	. . . . . . . . . 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 4563	. . . . . . 7 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → -_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
277	178, 179, 205, 276	ifbothda 4563	. . . . . 6 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) → if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
278	277	3expia 1121	. . . . 5 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → (𝑧 < 𝑤 → if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
279		fveq2 6905	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
280	211	fveq2d 6909	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝐹‘-𝑦) = (𝐹‘-𝑧))
281		xnegeq 13250	. . . . . . . . 9 ⊢ ((𝐹‘-𝑦) = (𝐹‘-𝑧) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑧))
282	280, 281	syl 17	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑧))
283	183, 279, 282	ifbieq12d 4553	. . . . . . 7 ⊢ (𝑦 = 𝑧 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)))
284		fvex 6918	. . . . . . . 8 ⊢ (𝐹‘𝑧) ∈ V
285		xnegex 13251	. . . . . . . 8 ⊢ -_𝑒(𝐹‘-𝑧) ∈ V
286	284, 285	ifex 4575	. . . . . . 7 ⊢ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) ∈ V
287	283, 7, 286	fvmpt 7015	. . . . . 6 ⊢ (𝑧 ∈ (-1[,]1) → (𝐺‘𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)))
288		fveq2 6905	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
289	258	fveq2d 6909	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝐹‘-𝑦) = (𝐹‘-𝑤))
290		xnegeq 13250	. . . . . . . . 9 ⊢ ((𝐹‘-𝑦) = (𝐹‘-𝑤) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑤))
291	289, 290	syl 17	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑤))
292	195, 288, 291	ifbieq12d 4553	. . . . . . 7 ⊢ (𝑦 = 𝑤 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
293		fvex 6918	. . . . . . . 8 ⊢ (𝐹‘𝑤) ∈ V
294		xnegex 13251	. . . . . . . 8 ⊢ -_𝑒(𝐹‘-𝑤) ∈ V
295	293, 294	ifex 4575	. . . . . . 7 ⊢ if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) ∈ V
296	292, 7, 295	fvmpt 7015	. . . . . 6 ⊢ (𝑤 ∈ (-1[,]1) → (𝐺‘𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
297	287, 296	breqan12d 5158	. . . . 5 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → ((𝐺‘𝑧) < (𝐺‘𝑤) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
298	278, 297	sylibrd 259	. . . 4 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → (𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤)))
299	298	rgen2 3198	. . 3 ⊢ ∀𝑧 ∈ (-1[,]1)∀𝑤 ∈ (-1[,]1)(𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤))
300		soisoi 7349	. . 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 18639	. . . . . 6 ⊢ ≤ ∈ TosetRel
303	302	elexi 3502	. . . . 5 ⊢ ≤ ∈ V
304	303	inex1 5316	. . . 4 ⊢ ( ≤ ∩ ((-1[,]1) × (-1[,]1))) ∈ V
305		ssid 4005	. . . . . . 7 ⊢ ℝ^* ⊆ ℝ^*
306		leiso 14499	. . . . . . 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 7355	. . . . 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 18633	. . . . . . . 8 ⊢ ( ≤ ∈ TosetRel → ≤ ∈ PosetRel)
312	302, 311	ax-mp 5	. . . . . . 7 ⊢ ≤ ∈ PosetRel
313		ledm 18636	. . . . . . . 8 ⊢ ℝ^* = dom ≤
314	313	psssdm 18628	. . . . . . 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 2745	. . . . 5 ⊢ (-1[,]1) = dom ( ≤ ∩ ((-1[,]1) × (-1[,]1)))
317	316, 313	ordthmeo 23811	. . . 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 1462	. . 3 ⊢ 𝐺 ∈ ((ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))Homeo(ordTop‘ ≤ ))
319		xrhmeo.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
320		eqid 2736	. . . . . . 7 ⊢ (ordTop‘ ≤ ) = (ordTop‘ ≤ )
321	319, 320	xrrest2 24831	. . . . . 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 23232	. . . . 5 ⊢ ((ordTop‘ ≤ ) ↾_t (-1[,]1)) = (ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))
324	322, 323	eqtri 2764	. . . 4 ⊢ (𝐽 ↾_t (-1[,]1)) = (ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))
325	324	oveq1i 7442	. . 3 ⊢ ((𝐽 ↾_t (-1[,]1))Homeo(ordTop‘ ≤ )) = ((ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))Homeo(ordTop‘ ≤ ))
326	318, 325	eleqtrri 2839	. 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 1539 ∈ wcel 2107 {cab 2713 ≠ wne 2939 ∀wral 3060 ∃wrex 3069 Vcvv 3479 ∩ cin 3949 ⊆ wss 3950 ifcif 4524 class class class wbr 5142 ↦ cmpt 5224 Po wpo 5589 Or wor 5590 × cxp 5682 ^◡ccnv 5683 dom cdm 5684 ran crn 5685 ⟶wf 6556 –onto→wfo 6558 –1-1-onto→wf1o 6559 ‘cfv 6560 Isom wiso 6561 (class class class)co 7432 ℝcr 11155 0cc0 11156 1c1 11157 + caddc 11159 +∞cpnf 11293 ℝ^*cxr 11295 < clt 11296 ≤ cle 11297 − cmin 11493 -cneg 11494 / cdiv 11921 -_𝑒cxne 13152 [,]cicc 13391 ↾_t crest 17466 TopOpenctopn 17467 ordTopcordt 17545 PosetRelcps 18610 TosetRel ctsr 18611 ℂ_fldccnfld 21365 Homeochmeo 23762 IIcii 24902

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5278 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 ax-cnex 11212 ax-resscn 11213 ax-1cn 11214 ax-icn 11215 ax-addcl 11216 ax-addrcl 11217 ax-mulcl 11218 ax-mulrcl 11219 ax-mulcom 11220 ax-addass 11221 ax-mulass 11222 ax-distr 11223 ax-i2m1 11224 ax-1ne0 11225 ax-1rid 11226 ax-rnegex 11227 ax-rrecex 11228 ax-cnre 11229 ax-pre-lttri 11230 ax-pre-lttrn 11231 ax-pre-ltadd 11232 ax-pre-mulgt0 11233 ax-pre-sup 11234

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-tp 4630 df-op 4632 df-uni 4907 df-int 4946 df-iun 4992 df-iin 4993 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-isom 6569 df-riota 7389 df-ov 7435 df-oprab 7436 df-mpo 7437 df-om 7889 df-1st 8015 df-2nd 8016 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-rdg 8451 df-1o 8507 df-2o 8508 df-er 8746 df-map 8869 df-en 8987 df-dom 8988 df-sdom 8989 df-fin 8990 df-fi 9452 df-sup 9483 df-inf 9484 df-pnf 11298 df-mnf 11299 df-xr 11300 df-ltxr 11301 df-le 11302 df-sub 11495 df-neg 11496 df-div 11922 df-nn 12268 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12529 df-z 12616 df-dec 12736 df-uz 12880 df-q 12992 df-rp 13036 df-xneg 13155 df-xadd 13156 df-xmul 13157 df-ioo 13392 df-ioc 13393 df-ico 13394 df-icc 13395 df-fz 13549 df-seq 14044 df-exp 14104 df-cj 15139 df-re 15140 df-im 15141 df-sqrt 15275 df-abs 15276 df-struct 17185 df-slot 17220 df-ndx 17232 df-base 17249 df-plusg 17311 df-mulr 17312 df-starv 17313 df-tset 17317 df-ple 17318 df-ds 17320 df-unif 17321 df-rest 17468 df-topn 17469 df-topgen 17489 df-ordt 17547 df-ps 18612 df-tsr 18613 df-psmet 21357 df-xmet 21358 df-met 21359 df-bl 21360 df-mopn 21361 df-cnfld 21366 df-top 22901 df-topon 22918 df-topsp 22940 df-bases 22954 df-cn 23236 df-hmeo 23764 df-xms 24331 df-ms 24332 df-ii 24904

This theorem is referenced by: xrhmph 24979

W3C validator