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 24900

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 13452	. . . 4 ⊢ (-1[,]1) ⊆ ℝ^*
2		xrltso 13162	. . . 4 ⊢ < Or ℝ^*
3		soss 5586	. . . 4 ⊢ ((-1[,]1) ⊆ ℝ^* → ( < Or ℝ^* → < Or (-1[,]1)))
4	1, 2, 3	mp2 9	. . 3 ⊢ < Or (-1[,]1)
5		sopo 5585	. . . 4 ⊢ ( < Or ℝ^* → < Po ℝ^*)
6	2, 5	ax-mp 5	. . 3 ⊢ < Po ℝ^*
7		xrhmeo.g	. . . . 5 ⊢ 𝐺 = (𝑦 ∈ (-1[,]1) ↦ if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
8		iccssxr 13452	. . . . . . 7 ⊢ (0[,]+∞) ⊆ ℝ^*
9		neg1rr 12360	. . . . . . . . . . . 12 ⊢ -1 ∈ ℝ
10		1re 11240	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
11	9, 10	elicc2i 13434	. . . . . . . . . . 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 13488	. . . . . . . . 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 24898	. . . . . . . . . . 11 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ^◡𝐹 = (𝑣 ∈ (0[,]+∞) ↦ if(𝑣 = +∞, 1, (𝑣 / (1 + 𝑣)))))
21	20	simpli 483	. . . . . . . . . 10 ⊢ 𝐹:(0[,]1)–1-1-onto→(0[,]+∞)
22		f1of 6823	. . . . . . . . . 10 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → 𝐹:(0[,]1)⟶(0[,]+∞))
23	21, 22	ax-mp 5	. . . . . . . . 9 ⊢ 𝐹:(0[,]1)⟶(0[,]+∞)
24	23	ffvelcdmi 7078	. . . . . . . 8 ⊢ (𝑦 ∈ (0[,]1) → (𝐹‘𝑦) ∈ (0[,]+∞))
25	18, 24	syl 17	. . . . . . 7 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → (𝐹‘𝑦) ∈ (0[,]+∞))
26	8, 25	sselid 3961	. . . . . 6 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → (𝐹‘𝑦) ∈ ℝ^*)
27	12	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → 𝑦 ∈ ℝ)
28	27	renegcld 11669	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ∈ ℝ)
29		0re 11242	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
30		letric 11340	. . . . . . . . . . . . 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 11813	. . . . . . . . . . 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 11746	. . . . . . . . . . . 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 13488	. . . . . . . . . 10 ⊢ (-𝑦 ∈ (0[,]1) ↔ (-𝑦 ∈ ℝ ∧ 0 ≤ -𝑦 ∧ -𝑦 ≤ 1))
41	28, 34, 39, 40	syl3anbrc 1344	. . . . . . . . 9 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ∈ (0[,]1))
42	23	ffvelcdmi 7078	. . . . . . . . 9 ⊢ (-𝑦 ∈ (0[,]1) → (𝐹‘-𝑦) ∈ (0[,]+∞))
43	41, 42	syl 17	. . . . . . . 8 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝐹‘-𝑦) ∈ (0[,]+∞))
44	8, 43	sselid 3961	. . . . . . 7 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝐹‘-𝑦) ∈ ℝ^*)
45	44	xnegcld 13321	. . . . . 6 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -_𝑒(𝐹‘-𝑦) ∈ ℝ^*)
46	26, 45	ifclda 4541	. . . . 5 ⊢ (𝑦 ∈ (-1[,]1) → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ∈ ℝ^*)
47	7, 46	fmpti 7107	. . . 4 ⊢ 𝐺:(-1[,]1)⟶ℝ^*
48		frn 6718	. . . . . 6 ⊢ (𝐺:(-1[,]1)⟶ℝ^* → ran 𝐺 ⊆ ℝ^*)
49	47, 48	ax-mp 5	. . . . 5 ⊢ ran 𝐺 ⊆ ℝ^*
50		ssabral 4045	. . . . . . 7 ⊢ (ℝ^* ⊆ {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))} ↔ ∀𝑧 ∈ ℝ^* ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
51		0le1 11765	. . . . . . . . . . . . 13 ⊢ 0 ≤ 1
52		le0neg2 11751	. . . . . . . . . . . . . 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 11870	. . . . . . . . . . . 12 ⊢ 1 ≤ 1
56		iccss 13436	. . . . . . . . . . . 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 13479	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (0[,]+∞) ↔ (𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧))
59		f1ocnv 6835	. . . . . . . . . . . . . 14 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → ^◡𝐹:(0[,]+∞)–1-1-onto→(0[,]1))
60		f1of 6823	. . . . . . . . . . . . . 14 ⊢ (^◡𝐹:(0[,]+∞)–1-1-onto→(0[,]1) → ^◡𝐹:(0[,]+∞)⟶(0[,]1))
61	21, 59, 60	mp2b 10	. . . . . . . . . . . . 13 ⊢ ^◡𝐹:(0[,]+∞)⟶(0[,]1)
62	61	ffvelcdmi 7078	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (0[,]+∞) → (^◡𝐹‘𝑧) ∈ (0[,]1))
63	58, 62	sylbir 235	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (^◡𝐹‘𝑧) ∈ (0[,]1))
64	57, 63	sselid 3961	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (^◡𝐹‘𝑧) ∈ (-1[,]1))
65		elicc01 13488	. . . . . . . . . . . 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 7275	. . . . . . . . . . . 12 ⊢ ((𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ 𝑧 ∈ (0[,]+∞)) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
70	21, 68, 69	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
71	70	eqcomd 2742	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))
72		breq2 5128	. . . . . . . . . . . 12 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (0 ≤ 𝑦 ↔ 0 ≤ (^◡𝐹‘𝑧)))
73		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝐹‘𝑦) = (𝐹‘(^◡𝐹‘𝑧)))
74	73	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝑧 = (𝐹‘𝑦) ↔ 𝑧 = (𝐹‘(^◡𝐹‘𝑧))))
75	72, 74	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑦 = (^◡𝐹‘𝑧) → ((0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) ↔ (0 ≤ (^◡𝐹‘𝑧) ∧ 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))))
76	75	rspcev 3606	. . . . . . . . . 10 ⊢ (((^◡𝐹‘𝑧) ∈ (-1[,]1) ∧ (0 ≤ (^◡𝐹‘𝑧) ∧ 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))) → ∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)))
77	64, 67, 71, 76	syl12anc 836	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)))
78		iftrue 4511	. . . . . . . . . . . 12 ⊢ (0 ≤ 𝑦 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = (𝐹‘𝑦))
79	78	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (0 ≤ 𝑦 → (𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ↔ 𝑧 = (𝐹‘𝑦)))
80	79	biimpar 477	. . . . . . . . . 10 ⊢ ((0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) → 𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
81	80	reximi 3075	. . . . . . . . 9 ⊢ (∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
82	77, 81	syl 17	. . . . . . . 8 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
83		xnegcl 13234	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ^* → -_𝑒𝑧 ∈ ℝ^*)
84	83	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒𝑧 ∈ ℝ^*)
85		0xr 11287	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ^*
86		xrletri 13174	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) → (0 ≤ 𝑧 ∨ 𝑧 ≤ 0))
87	85, 86	mpan 690	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℝ^* → (0 ≤ 𝑧 ∨ 𝑧 ≤ 0))
88	87	ord 864	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 → 𝑧 ≤ 0))
89		xle0neg1 13242	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℝ^* → (𝑧 ≤ 0 ↔ 0 ≤ -_𝑒𝑧))
90	88, 89	sylibd 239	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 → 0 ≤ -_𝑒𝑧))
91	90	imp 406	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → 0 ≤ -_𝑒𝑧)
92		elxrge0 13479	. . . . . . . . . . . . . . 15 ⊢ (-_𝑒𝑧 ∈ (0[,]+∞) ↔ (-_𝑒𝑧 ∈ ℝ^* ∧ 0 ≤ -_𝑒𝑧))
93	84, 91, 92	sylanbrc 583	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒𝑧 ∈ (0[,]+∞))
94	61	ffvelcdmi 7078	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝑧 ∈ (0[,]+∞) → (^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1))
95	93, 94	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1))
96	57, 95	sselid 3961	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1))
97		iccssre 13451	. . . . . . . . . . . . . . 15 ⊢ ((-1 ∈ ℝ ∧ 1 ∈ ℝ) → (-1[,]1) ⊆ ℝ)
98	9, 10, 97	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (-1[,]1) ⊆ ℝ
99	98, 96	sselid 3961	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℝ)
100		iccneg 13494	. . . . . . . . . . . . . 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 12363	. . . . . . . . . . . 12 ⊢ --1 = 1
105	104	oveq2i 7421	. . . . . . . . . . 11 ⊢ (-1[,]--1) = (-1[,]1)
106	103, 105	eleqtrdi 2845	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1))
107		xle0neg2 13243	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℝ^* → (0 ≤ 𝑧 ↔ -_𝑒𝑧 ≤ 0))
108	107	notbid 318	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 ↔ ¬ -_𝑒𝑧 ≤ 0))
109	108	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ -_𝑒𝑧 ≤ 0)
110		f1ocnvfv2 7275	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ -_𝑒𝑧 ∈ (0[,]+∞)) → (𝐹‘(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
111	21, 93, 110	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
112		0elunit 13491	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ (0[,]1)
113		ax-1ne0 11203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ≠ 0
114		neeq2 2996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 0 → (1 ≠ 𝑥 ↔ 1 ≠ 0))
115	113, 114	mpbiri 258	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 0 → 1 ≠ 𝑥)
116	115	necomd 2988	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → 𝑥 ≠ 1)
117		ifnefalse 4517	. . . . . . . . . . . . . . . . . . 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 7418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 0 → (1 − 𝑥) = (1 − 0))
121		1m0e1 12366	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 − 0) = 1
122	120, 121	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 0 → (1 − 𝑥) = 1)
123	119, 122	oveq12d 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → (𝑥 / (1 − 𝑥)) = (0 / 1))
124		ax-1cn 11192	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℂ
125	124, 113	div0i 11980	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 / 1) = 0
126	123, 125	eqtrdi 2787	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → (𝑥 / (1 − 𝑥)) = 0)
127	118, 126	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) = 0)
128		c0ex 11234	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
129	127, 19, 128	fvmpt 6991	. . . . . . . . . . . . . . . 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 5137	. . . . . . . . . . . . 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 24899	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ 𝐹 ∈ (IIHomeo((ordTop‘ ≤ ) ↾_t (0[,]+∞))))
136	135	simpli 483	. . . . . . . . . . . . . 14 ⊢ 𝐹 Isom < , < ((0[,]1), (0[,]+∞))
137		iccssxr 13452	. . . . . . . . . . . . . . 15 ⊢ (0[,]1) ⊆ ℝ^*
138	137, 8	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ ((0[,]1) ⊆ ℝ^* ∧ (0[,]+∞) ⊆ ℝ^*)
139		leisorel 14483	. . . . . . . . . . . . . 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 11813	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
144	142, 143	mtbid 324	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧))
145		unitssre 13521	. . . . . . . . . . . . . . . . 17 ⊢ (0[,]1) ⊆ ℝ
146	145, 95	sselid 3961	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℝ)
147	146	recnd 11268	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℂ)
148	147	negnegd 11590	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → --(^◡𝐹‘-_𝑒𝑧) = (^◡𝐹‘-_𝑒𝑧))
149	148	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = (𝐹‘(^◡𝐹‘-_𝑒𝑧)))
150	149, 111	eqtrd 2771	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
151		xnegeq 13228	. . . . . . . . . . . 12 ⊢ ((𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧 → -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒-_𝑒𝑧)
152	150, 151	syl 17	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒-_𝑒𝑧)
153		xnegneg 13235	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ^* → -_𝑒-_𝑒𝑧 = 𝑧)
154	153	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒-_𝑒𝑧 = 𝑧)
155	152, 154	eqtr2d 2772	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
156		breq2 5128	. . . . . . . . . . . . 13 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (0 ≤ 𝑦 ↔ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
157	156	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (¬ 0 ≤ 𝑦 ↔ ¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
158		negeq 11479	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → -𝑦 = --(^◡𝐹‘-_𝑒𝑧))
159	158	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (𝐹‘-𝑦) = (𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
160		xnegeq 13228	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘-𝑦) = (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
161	159, 160	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
162	161	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (𝑧 = -_𝑒(𝐹‘-𝑦) ↔ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧))))
163	157, 162	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → ((¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)) ↔ (¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧) ∧ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))))
164	163	rspcev 3606	. . . . . . . . . 10 ⊢ ((-(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ∧ (¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧) ∧ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))) → ∃𝑦 ∈ (-1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)))
165	106, 144, 155, 164	syl12anc 836	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)))
166		iffalse 4514	. . . . . . . . . . . 12 ⊢ (¬ 0 ≤ 𝑦 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = -_𝑒(𝐹‘-𝑦))
167	166	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (¬ 0 ≤ 𝑦 → (𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ↔ 𝑧 = -_𝑒(𝐹‘-𝑦)))
168	167	biimpar 477	. . . . . . . . . 10 ⊢ ((¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)) → 𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
169	168	reximi 3075	. . . . . . . . 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 3059	. . . . . 6 ⊢ ℝ^* ⊆ {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))}
173	7	rnmpt 5942	. . . . . 6 ⊢ ran 𝐺 = {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))}
174	172, 173	sseqtrri 4013	. . . . 5 ⊢ ℝ^* ⊆ ran 𝐺
175	49, 174	eqssi 3980	. . . 4 ⊢ ran 𝐺 = ℝ^*
176		dffo2 6799	. . . 4 ⊢ (𝐺:(-1[,]1)–onto→ℝ^* ↔ (𝐺:(-1[,]1)⟶ℝ^* ∧ ran 𝐺 = ℝ^*))
177	47, 175, 176	mpbir2an 711	. . 3 ⊢ 𝐺:(-1[,]1)–onto→ℝ^*
178		breq1 5127	. . . . . . 7 ⊢ ((𝐹‘𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) → ((𝐹‘𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
179		breq1 5127	. . . . . . 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 5128	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (0 ≤ 𝑦 ↔ 0 ≤ 𝑧))
184		eleq1w 2818	. . . . . . . . . . . . 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 3561	. . . . . . . . . . 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 3961	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ∈ ℝ)
192	98, 189	sselid 3961	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ ℝ)
193	191, 192, 180	ltled 11388	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ≤ 𝑤)
194	190, 191, 192, 182, 193	letrd 11397	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ≤ 𝑤)
195		breq2 5128	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (0 ≤ 𝑦 ↔ 0 ≤ 𝑤))
196		eleq1w 2818	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (0[,]1) ↔ 𝑤 ∈ (0[,]1)))
197	195, 196	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → ((0 ≤ 𝑦 → 𝑦 ∈ (0[,]1)) ↔ (0 ≤ 𝑤 → 𝑤 ∈ (0[,]1))))
198	197, 186	vtoclga 3561	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (-1[,]1) → (0 ≤ 𝑤 → 𝑤 ∈ (0[,]1)))
199	189, 194, 198	sylc 65	. . . . . . . . . 10 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ (0[,]1))
200		isorel 7324	. . . . . . . . . . 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 4513	. . . . . . . 8 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) = (𝐹‘𝑤))
205	203, 204	breqtrrd 5152	. . . . . . 7 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → (𝐹‘𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
206		breq2 5128	. . . . . . . 8 ⊢ ((𝐹‘𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) → (-_𝑒(𝐹‘-𝑧) < (𝐹‘𝑤) ↔ -_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
207		breq2 5128	. . . . . . . 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 11479	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑧 → -𝑦 = -𝑧)
212	211	eleq1d 2820	. . . . . . . . . . . . . . . 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 3561	. . . . . . . . . . . . . 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 7078	. . . . . . . . . . . 12 ⊢ (-𝑧 ∈ (0[,]1) → (𝐹‘-𝑧) ∈ (0[,]+∞))
219	217, 218	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ (0[,]+∞))
220	8, 219	sselid 3961	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ ℝ^*)
221	220	xnegcld 13321	. . . . . . . . 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 7078	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (0[,]1) → (𝐹‘𝑤) ∈ (0[,]+∞))
227	225, 226	syl 17	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘𝑤) ∈ (0[,]+∞))
228	8, 227	sselid 3961	. . . . . . . . 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 3961	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 ∈ ℝ)
232		ltnle 11319	. . . . . . . . . . . . . . 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 11811	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝑧 < 0 ↔ 0 < -𝑧))
236	234, 235	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 < -𝑧)
237		isorel 7324	. . . . . . . . . . . . . 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 5160	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 < (𝐹‘-𝑧))
242		xlt0neg2 13241	. . . . . . . . . . 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 13479	. . . . . . . . . . 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 13182	. . . . . . . 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 3961	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑧 ∈ ℝ)
252		simpll2 1214	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑤 ∈ (-1[,]1))
253	98, 252	sselid 3961	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑤 ∈ ℝ)
254	251, 253	ltnegd 11820	. . . . . . . . . . 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 11479	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → -𝑦 = -𝑤)
259	258	eleq1d 2820	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (-𝑦 ∈ (0[,]1) ↔ -𝑤 ∈ (0[,]1)))
260	257, 259	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((¬ 0 ≤ 𝑦 → -𝑦 ∈ (0[,]1)) ↔ (¬ 0 ≤ 𝑤 → -𝑤 ∈ (0[,]1))))
261	260, 214	vtoclga 3561	. . . . . . . . . . . 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 7324	. . . . . . . . . . . 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 7078	. . . . . . . . . . . 12 ⊢ (-𝑤 ∈ (0[,]1) → (𝐹‘-𝑤) ∈ (0[,]+∞))
269	262, 268	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑤) ∈ (0[,]+∞))
270	8, 269	sselid 3961	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑤) ∈ ℝ^*)
271	263, 218	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ (0[,]+∞))
272	8, 271	sselid 3961	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ ℝ^*)
273		xltneg 13238	. . . . . . . . . 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 4544	. . . . . . 7 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → -_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
277	178, 179, 205, 276	ifbothda 4544	. . . . . 6 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) → if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
278	277	3expia 1121	. . . . 5 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → (𝑧 < 𝑤 → if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
279		fveq2 6881	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
280	211	fveq2d 6885	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝐹‘-𝑦) = (𝐹‘-𝑧))
281		xnegeq 13228	. . . . . . . . 9 ⊢ ((𝐹‘-𝑦) = (𝐹‘-𝑧) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑧))
282	280, 281	syl 17	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑧))
283	183, 279, 282	ifbieq12d 4534	. . . . . . 7 ⊢ (𝑦 = 𝑧 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)))
284		fvex 6894	. . . . . . . 8 ⊢ (𝐹‘𝑧) ∈ V
285		xnegex 13229	. . . . . . . 8 ⊢ -_𝑒(𝐹‘-𝑧) ∈ V
286	284, 285	ifex 4556	. . . . . . 7 ⊢ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) ∈ V
287	283, 7, 286	fvmpt 6991	. . . . . 6 ⊢ (𝑧 ∈ (-1[,]1) → (𝐺‘𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)))
288		fveq2 6881	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
289	258	fveq2d 6885	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝐹‘-𝑦) = (𝐹‘-𝑤))
290		xnegeq 13228	. . . . . . . . 9 ⊢ ((𝐹‘-𝑦) = (𝐹‘-𝑤) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑤))
291	289, 290	syl 17	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑤))
292	195, 288, 291	ifbieq12d 4534	. . . . . . 7 ⊢ (𝑦 = 𝑤 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
293		fvex 6894	. . . . . . . 8 ⊢ (𝐹‘𝑤) ∈ V
294		xnegex 13229	. . . . . . . 8 ⊢ -_𝑒(𝐹‘-𝑤) ∈ V
295	293, 294	ifex 4556	. . . . . . 7 ⊢ if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) ∈ V
296	292, 7, 295	fvmpt 6991	. . . . . 6 ⊢ (𝑤 ∈ (-1[,]1) → (𝐺‘𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
297	287, 296	breqan12d 5140	. . . . 5 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → ((𝐺‘𝑧) < (𝐺‘𝑤) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
298	278, 297	sylibrd 259	. . . 4 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → (𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤)))
299	298	rgen2 3185	. . 3 ⊢ ∀𝑧 ∈ (-1[,]1)∀𝑤 ∈ (-1[,]1)(𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤))
300		soisoi 7326	. . 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 18608	. . . . . 6 ⊢ ≤ ∈ TosetRel
303	302	elexi 3487	. . . . 5 ⊢ ≤ ∈ V
304	303	inex1 5292	. . . 4 ⊢ ( ≤ ∩ ((-1[,]1) × (-1[,]1))) ∈ V
305		ssid 3986	. . . . . . 7 ⊢ ℝ^* ⊆ ℝ^*
306		leiso 14482	. . . . . . 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 7332	. . . . 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 18602	. . . . . . . 8 ⊢ ( ≤ ∈ TosetRel → ≤ ∈ PosetRel)
312	302, 311	ax-mp 5	. . . . . . 7 ⊢ ≤ ∈ PosetRel
313		ledm 18605	. . . . . . . 8 ⊢ ℝ^* = dom ≤
314	313	psssdm 18597	. . . . . . 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 23745	. . . 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 2736	. . . . . . 7 ⊢ (ordTop‘ ≤ ) = (ordTop‘ ≤ )
321	319, 320	xrrest2 24753	. . . . . 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 23166	. . . . 5 ⊢ ((ordTop‘ ≤ ) ↾_t (-1[,]1)) = (ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))
324	322, 323	eqtri 2759	. . . 4 ⊢ (𝐽 ↾_t (-1[,]1)) = (ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))
325	324	oveq1i 7420	. . 3 ⊢ ((𝐽 ↾_t (-1[,]1))Homeo(ordTop‘ ≤ )) = ((ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))Homeo(ordTop‘ ≤ ))
326	318, 325	eleqtrri 2834	. 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 2714 ≠ wne 2933 ∀wral 3052 ∃wrex 3061 Vcvv 3464 ∩ cin 3930 ⊆ wss 3931 ifcif 4505 class class class wbr 5124 ↦ cmpt 5206 Po wpo 5564 Or wor 5565 × cxp 5657 ^◡ccnv 5658 dom cdm 5659 ran crn 5660 ⟶wf 6532 –onto→wfo 6534 –1-1-onto→wf1o 6535 ‘cfv 6536 Isom wiso 6537 (class class class)co 7410 ℝcr 11133 0cc0 11134 1c1 11135 + caddc 11137 +∞cpnf 11271 ℝ^*cxr 11273 < clt 11274 ≤ cle 11275 − cmin 11471 -cneg 11472 / cdiv 11899 -_𝑒cxne 13130 [,]cicc 13370 ↾_t crest 17439 TopOpenctopn 17440 ordTopcordt 17518 PosetRelcps 18579 TosetRel ctsr 18580 ℂ_fldccnfld 21320 Homeochmeo 23696 IIcii 24824

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 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

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 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-iin 4975 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-er 8724 df-map 8847 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fi 9428 df-sup 9459 df-inf 9460 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 df-9 12315 df-n0 12507 df-z 12594 df-dec 12714 df-uz 12858 df-q 12970 df-rp 13014 df-xneg 13133 df-xadd 13134 df-xmul 13135 df-ioo 13371 df-ioc 13372 df-ico 13373 df-icc 13374 df-fz 13530 df-seq 14025 df-exp 14085 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-struct 17171 df-slot 17206 df-ndx 17218 df-base 17234 df-plusg 17289 df-mulr 17290 df-starv 17291 df-tset 17295 df-ple 17296 df-ds 17298 df-unif 17299 df-rest 17441 df-topn 17442 df-topgen 17462 df-ordt 17520 df-ps 18581 df-tsr 18582 df-psmet 21312 df-xmet 21313 df-met 21314 df-bl 21315 df-mopn 21316 df-cnfld 21321 df-top 22837 df-topon 22854 df-topsp 22876 df-bases 22889 df-cn 23170 df-hmeo 23698 df-xms 24264 df-ms 24265 df-ii 24826

This theorem is referenced by: xrhmph 24901

W3C validator