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 24309

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 13347	. . . 4 ⊢ (-1[,]1) ⊆ ℝ^*
2		xrltso 13060	. . . 4 ⊢ < Or ℝ^*
3		soss 5565	. . . 4 ⊢ ((-1[,]1) ⊆ ℝ^* → ( < Or ℝ^* → < Or (-1[,]1)))
4	1, 2, 3	mp2 9	. . 3 ⊢ < Or (-1[,]1)
5		sopo 5564	. . . 4 ⊢ ( < Or ℝ^* → < Po ℝ^*)
6	2, 5	ax-mp 5	. . 3 ⊢ < Po ℝ^*
7		xrhmeo.g	. . . . 5 ⊢ 𝐺 = (𝑦 ∈ (-1[,]1) ↦ if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
8		iccssxr 13347	. . . . . . 7 ⊢ (0[,]+∞) ⊆ ℝ^*
9		neg1rr 12268	. . . . . . . . . . . 12 ⊢ -1 ∈ ℝ
10		1re 11155	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
11	9, 10	elicc2i 13330	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (-1[,]1) ↔ (𝑦 ∈ ℝ ∧ -1 ≤ 𝑦 ∧ 𝑦 ≤ 1))
12	11	simp1bi 1145	. . . . . . . . . 10 ⊢ (𝑦 ∈ (-1[,]1) → 𝑦 ∈ ℝ)
13	12	adantr 481	. . . . . . . . 9 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → 𝑦 ∈ ℝ)
14		simpr 485	. . . . . . . . 9 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → 0 ≤ 𝑦)
15	11	simp3bi 1147	. . . . . . . . . 10 ⊢ (𝑦 ∈ (-1[,]1) → 𝑦 ≤ 1)
16	15	adantr 481	. . . . . . . . 9 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → 𝑦 ≤ 1)
17		elicc01 13383	. . . . . . . . 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 24307	. . . . . . . . . . 11 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ^◡𝐹 = (𝑣 ∈ (0[,]+∞) ↦ if(𝑣 = +∞, 1, (𝑣 / (1 + 𝑣)))))
21	20	simpli 484	. . . . . . . . . 10 ⊢ 𝐹:(0[,]1)–1-1-onto→(0[,]+∞)
22		f1of 6784	. . . . . . . . . 10 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → 𝐹:(0[,]1)⟶(0[,]+∞))
23	21, 22	ax-mp 5	. . . . . . . . 9 ⊢ 𝐹:(0[,]1)⟶(0[,]+∞)
24	23	ffvelcdmi 7034	. . . . . . . 8 ⊢ (𝑦 ∈ (0[,]1) → (𝐹‘𝑦) ∈ (0[,]+∞))
25	18, 24	syl 17	. . . . . . 7 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → (𝐹‘𝑦) ∈ (0[,]+∞))
26	8, 25	sselid 3942	. . . . . 6 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → (𝐹‘𝑦) ∈ ℝ^*)
27	12	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → 𝑦 ∈ ℝ)
28	27	renegcld 11582	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ∈ ℝ)
29		0re 11157	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
30		letric 11255	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 ≤ 𝑦 ∨ 𝑦 ≤ 0))
31	29, 12, 30	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (-1[,]1) → (0 ≤ 𝑦 ∨ 𝑦 ≤ 0))
32	31	orcanai 1001	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → 𝑦 ≤ 0)
33	27	le0neg1d 11726	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝑦 ≤ 0 ↔ 0 ≤ -𝑦))
34	32, 33	mpbid 231	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → 0 ≤ -𝑦)
35	11	simp2bi 1146	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (-1[,]1) → -1 ≤ 𝑦)
36	35	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -1 ≤ 𝑦)
37		lenegcon1 11659	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (-1 ≤ 𝑦 ↔ -𝑦 ≤ 1))
38	10, 27, 37	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (-1 ≤ 𝑦 ↔ -𝑦 ≤ 1))
39	36, 38	mpbid 231	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ≤ 1)
40		elicc01 13383	. . . . . . . . . 10 ⊢ (-𝑦 ∈ (0[,]1) ↔ (-𝑦 ∈ ℝ ∧ 0 ≤ -𝑦 ∧ -𝑦 ≤ 1))
41	28, 34, 39, 40	syl3anbrc 1343	. . . . . . . . 9 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ∈ (0[,]1))
42	23	ffvelcdmi 7034	. . . . . . . . 9 ⊢ (-𝑦 ∈ (0[,]1) → (𝐹‘-𝑦) ∈ (0[,]+∞))
43	41, 42	syl 17	. . . . . . . 8 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝐹‘-𝑦) ∈ (0[,]+∞))
44	8, 43	sselid 3942	. . . . . . 7 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝐹‘-𝑦) ∈ ℝ^*)
45	44	xnegcld 13219	. . . . . 6 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -_𝑒(𝐹‘-𝑦) ∈ ℝ^*)
46	26, 45	ifclda 4521	. . . . 5 ⊢ (𝑦 ∈ (-1[,]1) → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ∈ ℝ^*)
47	7, 46	fmpti 7060	. . . 4 ⊢ 𝐺:(-1[,]1)⟶ℝ^*
48		frn 6675	. . . . . 6 ⊢ (𝐺:(-1[,]1)⟶ℝ^* → ran 𝐺 ⊆ ℝ^*)
49	47, 48	ax-mp 5	. . . . 5 ⊢ ran 𝐺 ⊆ ℝ^*
50		ssabral 4019	. . . . . . 7 ⊢ (ℝ^* ⊆ {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))} ↔ ∀𝑧 ∈ ℝ^* ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
51		0le1 11678	. . . . . . . . . . . . 13 ⊢ 0 ≤ 1
52		le0neg2 11664	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ → (0 ≤ 1 ↔ -1 ≤ 0))
53	10, 52	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (0 ≤ 1 ↔ -1 ≤ 0)
54	51, 53	mpbi 229	. . . . . . . . . . . 12 ⊢ -1 ≤ 0
55		1le1 11783	. . . . . . . . . . . 12 ⊢ 1 ≤ 1
56		iccss 13332	. . . . . . . . . . . 12 ⊢ (((-1 ∈ ℝ ∧ 1 ∈ ℝ) ∧ (-1 ≤ 0 ∧ 1 ≤ 1)) → (0[,]1) ⊆ (-1[,]1))
57	9, 10, 54, 55, 56	mp4an 691	. . . . . . . . . . 11 ⊢ (0[,]1) ⊆ (-1[,]1)
58		elxrge0 13374	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (0[,]+∞) ↔ (𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧))
59		f1ocnv 6796	. . . . . . . . . . . . . 14 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → ^◡𝐹:(0[,]+∞)–1-1-onto→(0[,]1))
60		f1of 6784	. . . . . . . . . . . . . 14 ⊢ (^◡𝐹:(0[,]+∞)–1-1-onto→(0[,]1) → ^◡𝐹:(0[,]+∞)⟶(0[,]1))
61	21, 59, 60	mp2b 10	. . . . . . . . . . . . 13 ⊢ ^◡𝐹:(0[,]+∞)⟶(0[,]1)
62	61	ffvelcdmi 7034	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (0[,]+∞) → (^◡𝐹‘𝑧) ∈ (0[,]1))
63	58, 62	sylbir 234	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (^◡𝐹‘𝑧) ∈ (0[,]1))
64	57, 63	sselid 3942	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (^◡𝐹‘𝑧) ∈ (-1[,]1))
65		elicc01 13383	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑧) ∈ (0[,]1) ↔ ((^◡𝐹‘𝑧) ∈ ℝ ∧ 0 ≤ (^◡𝐹‘𝑧) ∧ (^◡𝐹‘𝑧) ≤ 1))
66	65	simp2bi 1146	. . . . . . . . . . 11 ⊢ ((^◡𝐹‘𝑧) ∈ (0[,]1) → 0 ≤ (^◡𝐹‘𝑧))
67	63, 66	syl 17	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → 0 ≤ (^◡𝐹‘𝑧))
68	58	biimpri 227	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → 𝑧 ∈ (0[,]+∞))
69		f1ocnvfv2 7223	. . . . . . . . . . . 12 ⊢ ((𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ 𝑧 ∈ (0[,]+∞)) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
70	21, 68, 69	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
71	70	eqcomd 2742	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))
72		breq2 5109	. . . . . . . . . . . 12 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (0 ≤ 𝑦 ↔ 0 ≤ (^◡𝐹‘𝑧)))
73		fveq2 6842	. . . . . . . . . . . . 13 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝐹‘𝑦) = (𝐹‘(^◡𝐹‘𝑧)))
74	73	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝑧 = (𝐹‘𝑦) ↔ 𝑧 = (𝐹‘(^◡𝐹‘𝑧))))
75	72, 74	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑦 = (^◡𝐹‘𝑧) → ((0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) ↔ (0 ≤ (^◡𝐹‘𝑧) ∧ 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))))
76	75	rspcev 3581	. . . . . . . . . 10 ⊢ (((^◡𝐹‘𝑧) ∈ (-1[,]1) ∧ (0 ≤ (^◡𝐹‘𝑧) ∧ 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))) → ∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)))
77	64, 67, 71, 76	syl12anc 835	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)))
78		iftrue 4492	. . . . . . . . . . . 12 ⊢ (0 ≤ 𝑦 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = (𝐹‘𝑦))
79	78	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (0 ≤ 𝑦 → (𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ↔ 𝑧 = (𝐹‘𝑦)))
80	79	biimpar 478	. . . . . . . . . 10 ⊢ ((0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) → 𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
81	80	reximi 3087	. . . . . . . . 9 ⊢ (∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
82	77, 81	syl 17	. . . . . . . 8 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
83		xnegcl 13132	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ^* → -_𝑒𝑧 ∈ ℝ^*)
84	83	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒𝑧 ∈ ℝ^*)
85		0xr 11202	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ^*
86		xrletri 13072	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) → (0 ≤ 𝑧 ∨ 𝑧 ≤ 0))
87	85, 86	mpan 688	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℝ^* → (0 ≤ 𝑧 ∨ 𝑧 ≤ 0))
88	87	ord 862	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 → 𝑧 ≤ 0))
89		xle0neg1 13140	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℝ^* → (𝑧 ≤ 0 ↔ 0 ≤ -_𝑒𝑧))
90	88, 89	sylibd 238	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 → 0 ≤ -_𝑒𝑧))
91	90	imp 407	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → 0 ≤ -_𝑒𝑧)
92		elxrge0 13374	. . . . . . . . . . . . . . 15 ⊢ (-_𝑒𝑧 ∈ (0[,]+∞) ↔ (-_𝑒𝑧 ∈ ℝ^* ∧ 0 ≤ -_𝑒𝑧))
93	84, 91, 92	sylanbrc 583	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒𝑧 ∈ (0[,]+∞))
94	61	ffvelcdmi 7034	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝑧 ∈ (0[,]+∞) → (^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1))
95	93, 94	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1))
96	57, 95	sselid 3942	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1))
97		iccssre 13346	. . . . . . . . . . . . . . 15 ⊢ ((-1 ∈ ℝ ∧ 1 ∈ ℝ) → (-1[,]1) ⊆ ℝ)
98	9, 10, 97	mp2an 690	. . . . . . . . . . . . . 14 ⊢ (-1[,]1) ⊆ ℝ
99	98, 96	sselid 3942	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℝ)
100		iccneg 13389	. . . . . . . . . . . . . 14 ⊢ ((-1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (^◡𝐹‘-_𝑒𝑧) ∈ ℝ) → ((^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ↔ -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]--1)))
101	9, 10, 100	mp3an12 1451	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹‘-_𝑒𝑧) ∈ ℝ → ((^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ↔ -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]--1)))
102	99, 101	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ↔ -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]--1)))
103	96, 102	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]--1))
104		negneg1e1 12271	. . . . . . . . . . . 12 ⊢ --1 = 1
105	104	oveq2i 7368	. . . . . . . . . . 11 ⊢ (-1[,]--1) = (-1[,]1)
106	103, 105	eleqtrdi 2848	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1))
107		xle0neg2 13141	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℝ^* → (0 ≤ 𝑧 ↔ -_𝑒𝑧 ≤ 0))
108	107	notbid 317	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 ↔ ¬ -_𝑒𝑧 ≤ 0))
109	108	biimpa 477	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ -_𝑒𝑧 ≤ 0)
110		f1ocnvfv2 7223	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ -_𝑒𝑧 ∈ (0[,]+∞)) → (𝐹‘(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
111	21, 93, 110	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
112		0elunit 13386	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ (0[,]1)
113		ax-1ne0 11120	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ≠ 0
114		neeq2 3007	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 0 → (1 ≠ 𝑥 ↔ 1 ≠ 0))
115	113, 114	mpbiri 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 0 → 1 ≠ 𝑥)
116	115	necomd 2999	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → 𝑥 ≠ 1)
117		ifnefalse 4498	. . . . . . . . . . . . . . . . . . 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 7365	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 0 → (1 − 𝑥) = (1 − 0))
121		1m0e1 12274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 − 0) = 1
122	120, 121	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 0 → (1 − 𝑥) = 1)
123	119, 122	oveq12d 7375	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → (𝑥 / (1 − 𝑥)) = (0 / 1))
124		ax-1cn 11109	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℂ
125	124, 113	div0i 11889	. . . . . . . . . . . . . . . . . . 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 11149	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
129	127, 19, 128	fvmpt 6948	. . . . . . . . . . . . . . . 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 5118	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0) ↔ -_𝑒𝑧 ≤ 0))
133	109, 132	mtbird 324	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ (𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0))
134		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ ((ordTop‘ ≤ ) ↾_t (0[,]+∞)) = ((ordTop‘ ≤ ) ↾_t (0[,]+∞))
135	19, 134	iccpnfhmeo 24308	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ 𝐹 ∈ (IIHomeo((ordTop‘ ≤ ) ↾_t (0[,]+∞))))
136	135	simpli 484	. . . . . . . . . . . . . 14 ⊢ 𝐹 Isom < , < ((0[,]1), (0[,]+∞))
137		iccssxr 13347	. . . . . . . . . . . . . . 15 ⊢ (0[,]1) ⊆ ℝ^*
138	137, 8	pm3.2i 471	. . . . . . . . . . . . . 14 ⊢ ((0[,]1) ⊆ ℝ^* ∧ (0[,]+∞) ⊆ ℝ^*)
139		leisorel 14359	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ ((0[,]1) ⊆ ℝ^* ∧ (0[,]+∞) ⊆ ℝ^*) ∧ ((^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1) ∧ 0 ∈ (0[,]1))) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ (𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0)))
140	136, 138, 139	mp3an12 1451	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ (𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0)))
141	95, 112, 140	sylancl 586	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ (𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0)))
142	133, 141	mtbird 324	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ (^◡𝐹‘-_𝑒𝑧) ≤ 0)
143	99	le0neg1d 11726	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
144	142, 143	mtbid 323	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧))
145		unitssre 13416	. . . . . . . . . . . . . . . . 17 ⊢ (0[,]1) ⊆ ℝ
146	145, 95	sselid 3942	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℝ)
147	146	recnd 11183	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℂ)
148	147	negnegd 11503	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → --(^◡𝐹‘-_𝑒𝑧) = (^◡𝐹‘-_𝑒𝑧))
149	148	fveq2d 6846	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = (𝐹‘(^◡𝐹‘-_𝑒𝑧)))
150	149, 111	eqtrd 2776	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
151		xnegeq 13126	. . . . . . . . . . . 12 ⊢ ((𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧 → -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒-_𝑒𝑧)
152	150, 151	syl 17	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒-_𝑒𝑧)
153		xnegneg 13133	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ^* → -_𝑒-_𝑒𝑧 = 𝑧)
154	153	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒-_𝑒𝑧 = 𝑧)
155	152, 154	eqtr2d 2777	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
156		breq2 5109	. . . . . . . . . . . . 13 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (0 ≤ 𝑦 ↔ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
157	156	notbid 317	. . . . . . . . . . . 12 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (¬ 0 ≤ 𝑦 ↔ ¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
158		negeq 11393	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → -𝑦 = --(^◡𝐹‘-_𝑒𝑧))
159	158	fveq2d 6846	. . . . . . . . . . . . . 14 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (𝐹‘-𝑦) = (𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
160		xnegeq 13126	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘-𝑦) = (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
161	159, 160	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
162	161	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (𝑧 = -_𝑒(𝐹‘-𝑦) ↔ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧))))
163	157, 162	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → ((¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)) ↔ (¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧) ∧ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))))
164	163	rspcev 3581	. . . . . . . . . 10 ⊢ ((-(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ∧ (¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧) ∧ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))) → ∃𝑦 ∈ (-1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)))
165	106, 144, 155, 164	syl12anc 835	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)))
166		iffalse 4495	. . . . . . . . . . . 12 ⊢ (¬ 0 ≤ 𝑦 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = -_𝑒(𝐹‘-𝑦))
167	166	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (¬ 0 ≤ 𝑦 → (𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ↔ 𝑧 = -_𝑒(𝐹‘-𝑦)))
168	167	biimpar 478	. . . . . . . . . 10 ⊢ ((¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)) → 𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
169	168	reximi 3087	. . . . . . . . 9 ⊢ (∃𝑦 ∈ (-1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)) → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
170	165, 169	syl 17	. . . . . . . 8 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
171	82, 170	pm2.61dan 811	. . . . . . 7 ⊢ (𝑧 ∈ ℝ^* → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
172	50, 171	mprgbir 3071	. . . . . 6 ⊢ ℝ^* ⊆ {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))}
173	7	rnmpt 5910	. . . . . 6 ⊢ ran 𝐺 = {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))}
174	172, 173	sseqtrri 3981	. . . . 5 ⊢ ℝ^* ⊆ ran 𝐺
175	49, 174	eqssi 3960	. . . 4 ⊢ ran 𝐺 = ℝ^*
176		dffo2 6760	. . . 4 ⊢ (𝐺:(-1[,]1)–onto→ℝ^* ↔ (𝐺:(-1[,]1)⟶ℝ^* ∧ ran 𝐺 = ℝ^*))
177	47, 175, 176	mpbir2an 709	. . 3 ⊢ 𝐺:(-1[,]1)–onto→ℝ^*
178		breq1 5108	. . . . . . 7 ⊢ ((𝐹‘𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) → ((𝐹‘𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
179		breq1 5108	. . . . . . 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 485	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ≤ 𝑧)
183		breq2 5109	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (0 ≤ 𝑦 ↔ 0 ≤ 𝑧))
184		eleq1w 2820	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ (0[,]1) ↔ 𝑧 ∈ (0[,]1)))
185	183, 184	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → ((0 ≤ 𝑦 → 𝑦 ∈ (0[,]1)) ↔ (0 ≤ 𝑧 → 𝑧 ∈ (0[,]1))))
186	18	ex 413	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (-1[,]1) → (0 ≤ 𝑦 → 𝑦 ∈ (0[,]1)))
187	185, 186	vtoclga 3534	. . . . . . . . . . 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 3942	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ∈ ℝ)
192	98, 189	sselid 3942	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ ℝ)
193	191, 192, 180	ltled 11303	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ≤ 𝑤)
194	190, 191, 192, 182, 193	letrd 11312	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ≤ 𝑤)
195		breq2 5109	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (0 ≤ 𝑦 ↔ 0 ≤ 𝑤))
196		eleq1w 2820	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (0[,]1) ↔ 𝑤 ∈ (0[,]1)))
197	195, 196	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → ((0 ≤ 𝑦 → 𝑦 ∈ (0[,]1)) ↔ (0 ≤ 𝑤 → 𝑤 ∈ (0[,]1))))
198	197, 186	vtoclga 3534	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (-1[,]1) → (0 ≤ 𝑤 → 𝑤 ∈ (0[,]1)))
199	189, 194, 198	sylc 65	. . . . . . . . . 10 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ (0[,]1))
200		isorel 7271	. . . . . . . . . . 11 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1))) → (𝑧 < 𝑤 ↔ (𝐹‘𝑧) < (𝐹‘𝑤)))
201	136, 200	mpan 688	. . . . . . . . . 10 ⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) → (𝑧 < 𝑤 ↔ (𝐹‘𝑧) < (𝐹‘𝑤)))
202	188, 199, 201	syl2anc 584	. . . . . . . . 9 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → (𝑧 < 𝑤 ↔ (𝐹‘𝑧) < (𝐹‘𝑤)))
203	180, 202	mpbid 231	. . . . . . . 8 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → (𝐹‘𝑧) < (𝐹‘𝑤))
204	194	iftrued 4494	. . . . . . . 8 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) = (𝐹‘𝑤))
205	203, 204	breqtrrd 5133	. . . . . . 7 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → (𝐹‘𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
206		breq2 5109	. . . . . . . 8 ⊢ ((𝐹‘𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) → (-_𝑒(𝐹‘-𝑧) < (𝐹‘𝑤) ↔ -_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
207		breq2 5109	. . . . . . . 8 ⊢ (-_𝑒(𝐹‘-𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) → (-_𝑒(𝐹‘-𝑧) < -_𝑒(𝐹‘-𝑤) ↔ -_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
208		simpl1 1191	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → 𝑧 ∈ (-1[,]1))
209		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → ¬ 0 ≤ 𝑧)
210	183	notbid 317	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → (¬ 0 ≤ 𝑦 ↔ ¬ 0 ≤ 𝑧))
211		negeq 11393	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑧 → -𝑦 = -𝑧)
212	211	eleq1d 2822	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → (-𝑦 ∈ (0[,]1) ↔ -𝑧 ∈ (0[,]1)))
213	210, 212	imbi12d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → ((¬ 0 ≤ 𝑦 → -𝑦 ∈ (0[,]1)) ↔ (¬ 0 ≤ 𝑧 → -𝑧 ∈ (0[,]1))))
214	41	ex 413	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (-1[,]1) → (¬ 0 ≤ 𝑦 → -𝑦 ∈ (0[,]1)))
215	213, 214	vtoclga 3534	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (-1[,]1) → (¬ 0 ≤ 𝑧 → -𝑧 ∈ (0[,]1)))
216	208, 209, 215	sylc 65	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → -𝑧 ∈ (0[,]1))
217	216	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -𝑧 ∈ (0[,]1))
218	23	ffvelcdmi 7034	. . . . . . . . . . . 12 ⊢ (-𝑧 ∈ (0[,]1) → (𝐹‘-𝑧) ∈ (0[,]+∞))
219	217, 218	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ (0[,]+∞))
220	8, 219	sselid 3942	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ ℝ^*)
221	220	xnegcld 13219	. . . . . . . . 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 485	. . . . . . . . . . . 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 7034	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (0[,]1) → (𝐹‘𝑤) ∈ (0[,]+∞))
227	225, 226	syl 17	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘𝑤) ∈ (0[,]+∞))
228	8, 227	sselid 3942	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘𝑤) ∈ ℝ^*)
229	209	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → ¬ 0 ≤ 𝑧)
230		simpll1 1212	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 ∈ (-1[,]1))
231	98, 230	sselid 3942	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 ∈ ℝ)
232		ltnle 11234	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ ∧ 0 ∈ ℝ) → (𝑧 < 0 ↔ ¬ 0 ≤ 𝑧))
233	231, 29, 232	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝑧 < 0 ↔ ¬ 0 ≤ 𝑧))
234	229, 233	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 < 0)
235	231	lt0neg1d 11724	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝑧 < 0 ↔ 0 < -𝑧))
236	234, 235	mpbid 231	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 < -𝑧)
237		isorel 7271	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (0 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1))) → (0 < -𝑧 ↔ (𝐹‘0) < (𝐹‘-𝑧)))
238	136, 237	mpan 688	. . . . . . . . . . . . 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 231	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘0) < (𝐹‘-𝑧))
241	130, 240	eqbrtrrid 5141	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 < (𝐹‘-𝑧))
242		xlt0neg2 13139	. . . . . . . . . . 11 ⊢ ((𝐹‘-𝑧) ∈ ℝ^* → (0 < (𝐹‘-𝑧) ↔ -_𝑒(𝐹‘-𝑧) < 0))
243	220, 242	syl 17	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (0 < (𝐹‘-𝑧) ↔ -_𝑒(𝐹‘-𝑧) < 0))
244	241, 243	mpbid 231	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -_𝑒(𝐹‘-𝑧) < 0)
245		elxrge0 13374	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑤) ∈ (0[,]+∞) ↔ ((𝐹‘𝑤) ∈ ℝ^* ∧ 0 ≤ (𝐹‘𝑤)))
246	245	simprbi 497	. . . . . . . . . 10 ⊢ ((𝐹‘𝑤) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝑤))
247	227, 246	syl 17	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 ≤ (𝐹‘𝑤))
248	221, 222, 228, 244, 247	xrltletrd 13080	. . . . . . . 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 3942	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑧 ∈ ℝ)
252		simpll2 1213	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑤 ∈ (-1[,]1))
253	98, 252	sselid 3942	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑤 ∈ ℝ)
254	251, 253	ltnegd 11733	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝑧 < 𝑤 ↔ -𝑤 < -𝑧))
255	249, 254	mpbid 231	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -𝑤 < -𝑧)
256		simpr 485	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → ¬ 0 ≤ 𝑤)
257	195	notbid 317	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (¬ 0 ≤ 𝑦 ↔ ¬ 0 ≤ 𝑤))
258		negeq 11393	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → -𝑦 = -𝑤)
259	258	eleq1d 2822	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (-𝑦 ∈ (0[,]1) ↔ -𝑤 ∈ (0[,]1)))
260	257, 259	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((¬ 0 ≤ 𝑦 → -𝑦 ∈ (0[,]1)) ↔ (¬ 0 ≤ 𝑤 → -𝑤 ∈ (0[,]1))))
261	260, 214	vtoclga 3534	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ (-1[,]1) → (¬ 0 ≤ 𝑤 → -𝑤 ∈ (0[,]1)))
262	252, 256, 261	sylc 65	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -𝑤 ∈ (0[,]1))
263	216	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -𝑧 ∈ (0[,]1))
264		isorel 7271	. . . . . . . . . . . 12 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (-𝑤 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1))) → (-𝑤 < -𝑧 ↔ (𝐹‘-𝑤) < (𝐹‘-𝑧)))
265	136, 264	mpan 688	. . . . . . . . . . 11 ⊢ ((-𝑤 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1)) → (-𝑤 < -𝑧 ↔ (𝐹‘-𝑤) < (𝐹‘-𝑧)))
266	262, 263, 265	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (-𝑤 < -𝑧 ↔ (𝐹‘-𝑤) < (𝐹‘-𝑧)))
267	255, 266	mpbid 231	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑤) < (𝐹‘-𝑧))
268	23	ffvelcdmi 7034	. . . . . . . . . . . 12 ⊢ (-𝑤 ∈ (0[,]1) → (𝐹‘-𝑤) ∈ (0[,]+∞))
269	262, 268	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑤) ∈ (0[,]+∞))
270	8, 269	sselid 3942	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑤) ∈ ℝ^*)
271	263, 218	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ (0[,]+∞))
272	8, 271	sselid 3942	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ ℝ^*)
273		xltneg 13136	. . . . . . . . . 10 ⊢ (((𝐹‘-𝑤) ∈ ℝ^* ∧ (𝐹‘-𝑧) ∈ ℝ^*) → ((𝐹‘-𝑤) < (𝐹‘-𝑧) ↔ -_𝑒(𝐹‘-𝑧) < -_𝑒(𝐹‘-𝑤)))
274	270, 272, 273	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → ((𝐹‘-𝑤) < (𝐹‘-𝑧) ↔ -_𝑒(𝐹‘-𝑧) < -_𝑒(𝐹‘-𝑤)))
275	267, 274	mpbid 231	. . . . . . . 8 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -_𝑒(𝐹‘-𝑧) < -_𝑒(𝐹‘-𝑤))
276	206, 207, 248, 275	ifbothda 4524	. . . . . . 7 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → -_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
277	178, 179, 205, 276	ifbothda 4524	. . . . . 6 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) → if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
278	277	3expia 1121	. . . . 5 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → (𝑧 < 𝑤 → if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
279		fveq2 6842	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
280	211	fveq2d 6846	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝐹‘-𝑦) = (𝐹‘-𝑧))
281		xnegeq 13126	. . . . . . . . 9 ⊢ ((𝐹‘-𝑦) = (𝐹‘-𝑧) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑧))
282	280, 281	syl 17	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑧))
283	183, 279, 282	ifbieq12d 4514	. . . . . . 7 ⊢ (𝑦 = 𝑧 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)))
284		fvex 6855	. . . . . . . 8 ⊢ (𝐹‘𝑧) ∈ V
285		xnegex 13127	. . . . . . . 8 ⊢ -_𝑒(𝐹‘-𝑧) ∈ V
286	284, 285	ifex 4536	. . . . . . 7 ⊢ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) ∈ V
287	283, 7, 286	fvmpt 6948	. . . . . 6 ⊢ (𝑧 ∈ (-1[,]1) → (𝐺‘𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)))
288		fveq2 6842	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
289	258	fveq2d 6846	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝐹‘-𝑦) = (𝐹‘-𝑤))
290		xnegeq 13126	. . . . . . . . 9 ⊢ ((𝐹‘-𝑦) = (𝐹‘-𝑤) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑤))
291	289, 290	syl 17	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑤))
292	195, 288, 291	ifbieq12d 4514	. . . . . . 7 ⊢ (𝑦 = 𝑤 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
293		fvex 6855	. . . . . . . 8 ⊢ (𝐹‘𝑤) ∈ V
294		xnegex 13127	. . . . . . . 8 ⊢ -_𝑒(𝐹‘-𝑤) ∈ V
295	293, 294	ifex 4536	. . . . . . 7 ⊢ if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) ∈ V
296	292, 7, 295	fvmpt 6948	. . . . . 6 ⊢ (𝑤 ∈ (-1[,]1) → (𝐺‘𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
297	287, 296	breqan12d 5121	. . . . 5 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → ((𝐺‘𝑧) < (𝐺‘𝑤) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
298	278, 297	sylibrd 258	. . . 4 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → (𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤)))
299	298	rgen2 3194	. . 3 ⊢ ∀𝑧 ∈ (-1[,]1)∀𝑤 ∈ (-1[,]1)(𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤))
300		soisoi 7273	. . 3 ⊢ ((( < Or (-1[,]1) ∧ < Po ℝ^) ∧ (𝐺:(-1[,]1)–onto→ℝ^ ∧ ∀𝑧 ∈ (-1[,]1)∀𝑤 ∈ (-1[,]1)(𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤)))) → 𝐺 Isom < , < ((-1[,]1), ℝ^*))
301	4, 6, 177, 299, 300	mp4an 691	. 2 ⊢ 𝐺 Isom < , < ((-1[,]1), ℝ^*)
302		letsr 18482	. . . . . 6 ⊢ ≤ ∈ TosetRel
303	302	elexi 3464	. . . . 5 ⊢ ≤ ∈ V
304	303	inex1 5274	. . . 4 ⊢ ( ≤ ∩ ((-1[,]1) × (-1[,]1))) ∈ V
305		ssid 3966	. . . . . . 7 ⊢ ℝ^* ⊆ ℝ^*
306		leiso 14358	. . . . . . 7 ⊢ (((-1[,]1) ⊆ ℝ^* ∧ ℝ^* ⊆ ℝ^) → (𝐺 Isom < , < ((-1[,]1), ℝ^) ↔ 𝐺 Isom ≤ , ≤ ((-1[,]1), ℝ^*)))
307	1, 305, 306	mp2an 690	. . . . . 6 ⊢ (𝐺 Isom < , < ((-1[,]1), ℝ^) ↔ 𝐺 Isom ≤ , ≤ ((-1[,]1), ℝ^))
308	301, 307	mpbi 229	. . . . 5 ⊢ 𝐺 Isom ≤ , ≤ ((-1[,]1), ℝ^*)
309		isores1 7279	. . . . 5 ⊢ (𝐺 Isom ≤ , ≤ ((-1[,]1), ℝ^) ↔ 𝐺 Isom ( ≤ ∩ ((-1[,]1) × (-1[,]1))), ≤ ((-1[,]1), ℝ^))
310	308, 309	mpbi 229	. . . 4 ⊢ 𝐺 Isom ( ≤ ∩ ((-1[,]1) × (-1[,]1))), ≤ ((-1[,]1), ℝ^*)
311		tsrps 18476	. . . . . . . 8 ⊢ ( ≤ ∈ TosetRel → ≤ ∈ PosetRel)
312	302, 311	ax-mp 5	. . . . . . 7 ⊢ ≤ ∈ PosetRel
313		ledm 18479	. . . . . . . 8 ⊢ ℝ^* = dom ≤
314	313	psssdm 18471	. . . . . . 7 ⊢ (( ≤ ∈ PosetRel ∧ (-1[,]1) ⊆ ℝ^*) → dom ( ≤ ∩ ((-1[,]1) × (-1[,]1))) = (-1[,]1))
315	312, 1, 314	mp2an 690	. . . . . 6 ⊢ dom ( ≤ ∩ ((-1[,]1) × (-1[,]1))) = (-1[,]1)
316	315	eqcomi 2745	. . . . 5 ⊢ (-1[,]1) = dom ( ≤ ∩ ((-1[,]1) × (-1[,]1)))
317	316, 313	ordthmeo 23153	. . . 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 1461	. . 3 ⊢ 𝐺 ∈ ((ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))Homeo(ordTop‘ ≤ ))
319		xrhmeo.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
320		eqid 2736	. . . . . . 7 ⊢ (ordTop‘ ≤ ) = (ordTop‘ ≤ )
321	319, 320	xrrest2 24171	. . . . . 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 22574	. . . . 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 7367	. . 3 ⊢ ((𝐽 ↾_t (-1[,]1))Homeo(ordTop‘ ≤ )) = ((ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))Homeo(ordTop‘ ≤ ))
326	318, 325	eleqtrri 2837	. 2 ⊢ 𝐺 ∈ ((𝐽 ↾_t (-1[,]1))Homeo(ordTop‘ ≤ ))
327	301, 326	pm3.2i 471	1 ⊢ (𝐺 Isom < , < ((-1[,]1), ℝ^*) ∧ 𝐺 ∈ ((𝐽 ↾_t (-1[,]1))Homeo(ordTop‘ ≤ )))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 {cab 2713 ≠ wne 2943 ∀wral 3064 ∃wrex 3073 Vcvv 3445 ∩ cin 3909 ⊆ wss 3910 ifcif 4486 class class class wbr 5105 ↦ cmpt 5188 Po wpo 5543 Or wor 5544 × cxp 5631 ^◡ccnv 5632 dom cdm 5633 ran crn 5634 ⟶wf 6492 –onto→wfo 6494 –1-1-onto→wf1o 6495 ‘cfv 6496 Isom wiso 6497 (class class class)co 7357 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 +∞cpnf 11186 ℝ^*cxr 11188 < clt 11189 ≤ cle 11190 − cmin 11385 -cneg 11386 / cdiv 11812 -_𝑒cxne 13030 [,]cicc 13267 ↾_t crest 17302 TopOpenctopn 17303 ordTopcordt 17381 PosetRelcps 18453 TosetRel ctsr 18454 ℂ_fldccnfld 20796 Homeochmeo 23104 IIcii 24238

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-tp 4591 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-iin 4957 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-er 8648 df-map 8767 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fi 9347 df-sup 9378 df-inf 9379 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-4 12218 df-5 12219 df-6 12220 df-7 12221 df-8 12222 df-9 12223 df-n0 12414 df-z 12500 df-dec 12619 df-uz 12764 df-q 12874 df-rp 12916 df-xneg 13033 df-xadd 13034 df-xmul 13035 df-ioo 13268 df-ioc 13269 df-ico 13270 df-icc 13271 df-fz 13425 df-seq 13907 df-exp 13968 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-struct 17019 df-slot 17054 df-ndx 17066 df-base 17084 df-plusg 17146 df-mulr 17147 df-starv 17148 df-tset 17152 df-ple 17153 df-ds 17155 df-unif 17156 df-rest 17304 df-topn 17305 df-topgen 17325 df-ordt 17383 df-ps 18455 df-tsr 18456 df-psmet 20788 df-xmet 20789 df-met 20790 df-bl 20791 df-mopn 20792 df-cnfld 20797 df-top 22243 df-topon 22260 df-topsp 22282 df-bases 22296 df-cn 22578 df-hmeo 23106 df-xms 23673 df-ms 23674 df-ii 24240

This theorem is referenced by: xrhmph 24310

W3C validator