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 23552

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 12822	. . . 4 ⊢ (-1[,]1) ⊆ ℝ^*
2		xrltso 12537	. . . 4 ⊢ < Or ℝ^*
3		soss 5495	. . . 4 ⊢ ((-1[,]1) ⊆ ℝ^* → ( < Or ℝ^* → < Or (-1[,]1)))
4	1, 2, 3	mp2 9	. . 3 ⊢ < Or (-1[,]1)
5		sopo 5494	. . . 4 ⊢ ( < Or ℝ^* → < Po ℝ^*)
6	2, 5	ax-mp 5	. . 3 ⊢ < Po ℝ^*
7		xrhmeo.g	. . . . 5 ⊢ 𝐺 = (𝑦 ∈ (-1[,]1) ↦ if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
8		iccssxr 12822	. . . . . . 7 ⊢ (0[,]+∞) ⊆ ℝ^*
9		neg1rr 11755	. . . . . . . . . . . 12 ⊢ -1 ∈ ℝ
10		1re 10643	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
11	9, 10	elicc2i 12805	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (-1[,]1) ↔ (𝑦 ∈ ℝ ∧ -1 ≤ 𝑦 ∧ 𝑦 ≤ 1))
12	11	simp1bi 1141	. . . . . . . . . 10 ⊢ (𝑦 ∈ (-1[,]1) → 𝑦 ∈ ℝ)
13	12	adantr 483	. . . . . . . . 9 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → 𝑦 ∈ ℝ)
14		simpr 487	. . . . . . . . 9 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → 0 ≤ 𝑦)
15	11	simp3bi 1143	. . . . . . . . . 10 ⊢ (𝑦 ∈ (-1[,]1) → 𝑦 ≤ 1)
16	15	adantr 483	. . . . . . . . 9 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → 𝑦 ≤ 1)
17		elicc01 12857	. . . . . . . . 9 ⊢ (𝑦 ∈ (0[,]1) ↔ (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ∧ 𝑦 ≤ 1))
18	13, 14, 16, 17	syl3anbrc 1339	. . . . . . . 8 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → 𝑦 ∈ (0[,]1))
19		xrhmeo.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))
20	19	iccpnfcnv 23550	. . . . . . . . . . 11 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ^◡𝐹 = (𝑣 ∈ (0[,]+∞) ↦ if(𝑣 = +∞, 1, (𝑣 / (1 + 𝑣)))))
21	20	simpli 486	. . . . . . . . . 10 ⊢ 𝐹:(0[,]1)–1-1-onto→(0[,]+∞)
22		f1of 6617	. . . . . . . . . 10 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → 𝐹:(0[,]1)⟶(0[,]+∞))
23	21, 22	ax-mp 5	. . . . . . . . 9 ⊢ 𝐹:(0[,]1)⟶(0[,]+∞)
24	23	ffvelrni 6852	. . . . . . . 8 ⊢ (𝑦 ∈ (0[,]1) → (𝐹‘𝑦) ∈ (0[,]+∞))
25	18, 24	syl 17	. . . . . . 7 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → (𝐹‘𝑦) ∈ (0[,]+∞))
26	8, 25	sseldi 3967	. . . . . 6 ⊢ ((𝑦 ∈ (-1[,]1) ∧ 0 ≤ 𝑦) → (𝐹‘𝑦) ∈ ℝ^*)
27	12	adantr 483	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → 𝑦 ∈ ℝ)
28	27	renegcld 11069	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ∈ ℝ)
29		0re 10645	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
30		letric 10742	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 ≤ 𝑦 ∨ 𝑦 ≤ 0))
31	29, 12, 30	sylancr 589	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (-1[,]1) → (0 ≤ 𝑦 ∨ 𝑦 ≤ 0))
32	31	orcanai 999	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → 𝑦 ≤ 0)
33	27	le0neg1d 11213	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝑦 ≤ 0 ↔ 0 ≤ -𝑦))
34	32, 33	mpbid 234	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → 0 ≤ -𝑦)
35	11	simp2bi 1142	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (-1[,]1) → -1 ≤ 𝑦)
36	35	adantr 483	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -1 ≤ 𝑦)
37		lenegcon1 11146	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (-1 ≤ 𝑦 ↔ -𝑦 ≤ 1))
38	10, 27, 37	sylancr 589	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (-1 ≤ 𝑦 ↔ -𝑦 ≤ 1))
39	36, 38	mpbid 234	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ≤ 1)
40		elicc01 12857	. . . . . . . . . 10 ⊢ (-𝑦 ∈ (0[,]1) ↔ (-𝑦 ∈ ℝ ∧ 0 ≤ -𝑦 ∧ -𝑦 ≤ 1))
41	28, 34, 39, 40	syl3anbrc 1339	. . . . . . . . 9 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -𝑦 ∈ (0[,]1))
42	23	ffvelrni 6852	. . . . . . . . 9 ⊢ (-𝑦 ∈ (0[,]1) → (𝐹‘-𝑦) ∈ (0[,]+∞))
43	41, 42	syl 17	. . . . . . . 8 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝐹‘-𝑦) ∈ (0[,]+∞))
44	8, 43	sseldi 3967	. . . . . . 7 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → (𝐹‘-𝑦) ∈ ℝ^*)
45	44	xnegcld 12696	. . . . . 6 ⊢ ((𝑦 ∈ (-1[,]1) ∧ ¬ 0 ≤ 𝑦) → -_𝑒(𝐹‘-𝑦) ∈ ℝ^*)
46	26, 45	ifclda 4503	. . . . 5 ⊢ (𝑦 ∈ (-1[,]1) → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ∈ ℝ^*)
47	7, 46	fmpti 6878	. . . 4 ⊢ 𝐺:(-1[,]1)⟶ℝ^*
48		frn 6522	. . . . . 6 ⊢ (𝐺:(-1[,]1)⟶ℝ^* → ran 𝐺 ⊆ ℝ^*)
49	47, 48	ax-mp 5	. . . . 5 ⊢ ran 𝐺 ⊆ ℝ^*
50		ssabral 4044	. . . . . . 7 ⊢ (ℝ^* ⊆ {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))} ↔ ∀𝑧 ∈ ℝ^* ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
51		0le1 11165	. . . . . . . . . . . . 13 ⊢ 0 ≤ 1
52		le0neg2 11151	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ → (0 ≤ 1 ↔ -1 ≤ 0))
53	10, 52	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (0 ≤ 1 ↔ -1 ≤ 0)
54	51, 53	mpbi 232	. . . . . . . . . . . 12 ⊢ -1 ≤ 0
55		1le1 11270	. . . . . . . . . . . 12 ⊢ 1 ≤ 1
56		iccss 12807	. . . . . . . . . . . 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 12848	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (0[,]+∞) ↔ (𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧))
59		f1ocnv 6629	. . . . . . . . . . . . . 14 ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) → ^◡𝐹:(0[,]+∞)–1-1-onto→(0[,]1))
60		f1of 6617	. . . . . . . . . . . . . 14 ⊢ (^◡𝐹:(0[,]+∞)–1-1-onto→(0[,]1) → ^◡𝐹:(0[,]+∞)⟶(0[,]1))
61	21, 59, 60	mp2b 10	. . . . . . . . . . . . 13 ⊢ ^◡𝐹:(0[,]+∞)⟶(0[,]1)
62	61	ffvelrni 6852	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (0[,]+∞) → (^◡𝐹‘𝑧) ∈ (0[,]1))
63	58, 62	sylbir 237	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (^◡𝐹‘𝑧) ∈ (0[,]1))
64	57, 63	sseldi 3967	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (^◡𝐹‘𝑧) ∈ (-1[,]1))
65		elicc01 12857	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑧) ∈ (0[,]1) ↔ ((^◡𝐹‘𝑧) ∈ ℝ ∧ 0 ≤ (^◡𝐹‘𝑧) ∧ (^◡𝐹‘𝑧) ≤ 1))
66	65	simp2bi 1142	. . . . . . . . . . 11 ⊢ ((^◡𝐹‘𝑧) ∈ (0[,]1) → 0 ≤ (^◡𝐹‘𝑧))
67	63, 66	syl 17	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → 0 ≤ (^◡𝐹‘𝑧))
68	58	biimpri 230	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → 𝑧 ∈ (0[,]+∞))
69		f1ocnvfv2 7036	. . . . . . . . . . . 12 ⊢ ((𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ 𝑧 ∈ (0[,]+∞)) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
70	21, 68, 69	sylancr 589	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
71	70	eqcomd 2829	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))
72		breq2 5072	. . . . . . . . . . . 12 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (0 ≤ 𝑦 ↔ 0 ≤ (^◡𝐹‘𝑧)))
73		fveq2 6672	. . . . . . . . . . . . 13 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝐹‘𝑦) = (𝐹‘(^◡𝐹‘𝑧)))
74	73	eqeq2d 2834	. . . . . . . . . . . 12 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝑧 = (𝐹‘𝑦) ↔ 𝑧 = (𝐹‘(^◡𝐹‘𝑧))))
75	72, 74	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑦 = (^◡𝐹‘𝑧) → ((0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) ↔ (0 ≤ (^◡𝐹‘𝑧) ∧ 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))))
76	75	rspcev 3625	. . . . . . . . . 10 ⊢ (((^◡𝐹‘𝑧) ∈ (-1[,]1) ∧ (0 ≤ (^◡𝐹‘𝑧) ∧ 𝑧 = (𝐹‘(^◡𝐹‘𝑧)))) → ∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)))
77	64, 67, 71, 76	syl12anc 834	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)))
78		iftrue 4475	. . . . . . . . . . . 12 ⊢ (0 ≤ 𝑦 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = (𝐹‘𝑦))
79	78	eqeq2d 2834	. . . . . . . . . . 11 ⊢ (0 ≤ 𝑦 → (𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ↔ 𝑧 = (𝐹‘𝑦)))
80	79	biimpar 480	. . . . . . . . . 10 ⊢ ((0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) → 𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
81	80	reximi 3245	. . . . . . . . 9 ⊢ (∃𝑦 ∈ (-1[,]1)(0 ≤ 𝑦 ∧ 𝑧 = (𝐹‘𝑦)) → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
82	77, 81	syl 17	. . . . . . . 8 ⊢ ((𝑧 ∈ ℝ^* ∧ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
83		xnegcl 12609	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ^* → -_𝑒𝑧 ∈ ℝ^*)
84	83	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒𝑧 ∈ ℝ^*)
85		0xr 10690	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℝ^*
86		xrletri 12549	. . . . . . . . . . . . . . . . . . 19 ⊢ ((0 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) → (0 ≤ 𝑧 ∨ 𝑧 ≤ 0))
87	85, 86	mpan 688	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℝ^* → (0 ≤ 𝑧 ∨ 𝑧 ≤ 0))
88	87	ord 860	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 → 𝑧 ≤ 0))
89		xle0neg1 12617	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℝ^* → (𝑧 ≤ 0 ↔ 0 ≤ -_𝑒𝑧))
90	88, 89	sylibd 241	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 → 0 ≤ -_𝑒𝑧))
91	90	imp 409	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → 0 ≤ -_𝑒𝑧)
92		elxrge0 12848	. . . . . . . . . . . . . . 15 ⊢ (-_𝑒𝑧 ∈ (0[,]+∞) ↔ (-_𝑒𝑧 ∈ ℝ^* ∧ 0 ≤ -_𝑒𝑧))
93	84, 91, 92	sylanbrc 585	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒𝑧 ∈ (0[,]+∞))
94	61	ffvelrni 6852	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝑧 ∈ (0[,]+∞) → (^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1))
95	93, 94	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1))
96	57, 95	sseldi 3967	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1))
97		iccssre 12821	. . . . . . . . . . . . . . 15 ⊢ ((-1 ∈ ℝ ∧ 1 ∈ ℝ) → (-1[,]1) ⊆ ℝ)
98	9, 10, 97	mp2an 690	. . . . . . . . . . . . . 14 ⊢ (-1[,]1) ⊆ ℝ
99	98, 96	sseldi 3967	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℝ)
100		iccneg 12861	. . . . . . . . . . . . . 14 ⊢ ((-1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (^◡𝐹‘-_𝑒𝑧) ∈ ℝ) → ((^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ↔ -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]--1)))
101	9, 10, 100	mp3an12 1447	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹‘-_𝑒𝑧) ∈ ℝ → ((^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ↔ -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]--1)))
102	99, 101	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ↔ -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]--1)))
103	96, 102	mpbid 234	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]--1))
104		negneg1e1 11758	. . . . . . . . . . . 12 ⊢ --1 = 1
105	104	oveq2i 7169	. . . . . . . . . . 11 ⊢ (-1[,]--1) = (-1[,]1)
106	103, 105	eleqtrdi 2925	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1))
107		xle0neg2 12618	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℝ^* → (0 ≤ 𝑧 ↔ -_𝑒𝑧 ≤ 0))
108	107	notbid 320	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℝ^* → (¬ 0 ≤ 𝑧 ↔ ¬ -_𝑒𝑧 ≤ 0))
109	108	biimpa 479	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ -_𝑒𝑧 ≤ 0)
110		f1ocnvfv2 7036	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ -_𝑒𝑧 ∈ (0[,]+∞)) → (𝐹‘(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
111	21, 93, 110	sylancr 589	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
112		0elunit 12858	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ (0[,]1)
113		ax-1ne0 10608	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ≠ 0
114		neeq2 3081	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 0 → (1 ≠ 𝑥 ↔ 1 ≠ 0))
115	113, 114	mpbiri 260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 0 → 1 ≠ 𝑥)
116	115	necomd 3073	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → 𝑥 ≠ 1)
117		ifnefalse 4481	. . . . . . . . . . . . . . . . . . 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 7166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 0 → (1 − 𝑥) = (1 − 0))
121		1m0e1 11761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 − 0) = 1
122	120, 121	syl6eq 2874	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 0 → (1 − 𝑥) = 1)
123	119, 122	oveq12d 7176	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 0 → (𝑥 / (1 − 𝑥)) = (0 / 1))
124		ax-1cn 10597	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℂ
125	124, 113	div0i 11376	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 / 1) = 0
126	123, 125	syl6eq 2874	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 0 → (𝑥 / (1 − 𝑥)) = 0)
127	118, 126	eqtrd 2858	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) = 0)
128		c0ex 10637	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
129	127, 19, 128	fvmpt 6770	. . . . . . . . . . . . . . . 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 5081	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0) ↔ -_𝑒𝑧 ≤ 0))
133	109, 132	mtbird 327	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ (𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0))
134		eqid 2823	. . . . . . . . . . . . . . . 16 ⊢ ((ordTop‘ ≤ ) ↾_t (0[,]+∞)) = ((ordTop‘ ≤ ) ↾_t (0[,]+∞))
135	19, 134	iccpnfhmeo 23551	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ 𝐹 ∈ (IIHomeo((ordTop‘ ≤ ) ↾_t (0[,]+∞))))
136	135	simpli 486	. . . . . . . . . . . . . 14 ⊢ 𝐹 Isom < , < ((0[,]1), (0[,]+∞))
137		iccssxr 12822	. . . . . . . . . . . . . . 15 ⊢ (0[,]1) ⊆ ℝ^*
138	137, 8	pm3.2i 473	. . . . . . . . . . . . . 14 ⊢ ((0[,]1) ⊆ ℝ^* ∧ (0[,]+∞) ⊆ ℝ^*)
139		leisorel 13821	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ ((0[,]1) ⊆ ℝ^* ∧ (0[,]+∞) ⊆ ℝ^*) ∧ ((^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1) ∧ 0 ∈ (0[,]1))) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ (𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0)))
140	136, 138, 139	mp3an12 1447	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘-_𝑒𝑧) ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ (𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0)))
141	95, 112, 140	sylancl 588	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ (𝐹‘(^◡𝐹‘-_𝑒𝑧)) ≤ (𝐹‘0)))
142	133, 141	mtbird 327	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ (^◡𝐹‘-_𝑒𝑧) ≤ 0)
143	99	le0neg1d 11213	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ((^◡𝐹‘-_𝑒𝑧) ≤ 0 ↔ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
144	142, 143	mtbid 326	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧))
145		unitssre 12888	. . . . . . . . . . . . . . . . 17 ⊢ (0[,]1) ⊆ ℝ
146	145, 95	sseldi 3967	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℝ)
147	146	recnd 10671	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (^◡𝐹‘-_𝑒𝑧) ∈ ℂ)
148	147	negnegd 10990	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → --(^◡𝐹‘-_𝑒𝑧) = (^◡𝐹‘-_𝑒𝑧))
149	148	fveq2d 6676	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = (𝐹‘(^◡𝐹‘-_𝑒𝑧)))
150	149, 111	eqtrd 2858	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧)
151		xnegeq 12603	. . . . . . . . . . . 12 ⊢ ((𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒𝑧 → -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒-_𝑒𝑧)
152	150, 151	syl 17	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)) = -_𝑒-_𝑒𝑧)
153		xnegneg 12610	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℝ^* → -_𝑒-_𝑒𝑧 = 𝑧)
154	153	adantr 483	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → -_𝑒-_𝑒𝑧 = 𝑧)
155	152, 154	eqtr2d 2859	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
156		breq2 5072	. . . . . . . . . . . . 13 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (0 ≤ 𝑦 ↔ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
157	156	notbid 320	. . . . . . . . . . . 12 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (¬ 0 ≤ 𝑦 ↔ ¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧)))
158		negeq 10880	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → -𝑦 = --(^◡𝐹‘-_𝑒𝑧))
159	158	fveq2d 6676	. . . . . . . . . . . . . 14 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (𝐹‘-𝑦) = (𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
160		xnegeq 12603	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘-𝑦) = (𝐹‘--(^◡𝐹‘-_𝑒𝑧)) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
161	159, 160	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))
162	161	eqeq2d 2834	. . . . . . . . . . . 12 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → (𝑧 = -_𝑒(𝐹‘-𝑦) ↔ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧))))
163	157, 162	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑦 = -(^◡𝐹‘-_𝑒𝑧) → ((¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)) ↔ (¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧) ∧ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))))
164	163	rspcev 3625	. . . . . . . . . 10 ⊢ ((-(^◡𝐹‘-_𝑒𝑧) ∈ (-1[,]1) ∧ (¬ 0 ≤ -(^◡𝐹‘-_𝑒𝑧) ∧ 𝑧 = -_𝑒(𝐹‘--(^◡𝐹‘-_𝑒𝑧)))) → ∃𝑦 ∈ (-1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)))
165	106, 144, 155, 164	syl12anc 834	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ^* ∧ ¬ 0 ≤ 𝑧) → ∃𝑦 ∈ (-1[,]1)(¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)))
166		iffalse 4478	. . . . . . . . . . . 12 ⊢ (¬ 0 ≤ 𝑦 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = -_𝑒(𝐹‘-𝑦))
167	166	eqeq2d 2834	. . . . . . . . . . 11 ⊢ (¬ 0 ≤ 𝑦 → (𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) ↔ 𝑧 = -_𝑒(𝐹‘-𝑦)))
168	167	biimpar 480	. . . . . . . . . 10 ⊢ ((¬ 0 ≤ 𝑦 ∧ 𝑧 = -_𝑒(𝐹‘-𝑦)) → 𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)))
169	168	reximi 3245	. . . . . . . . 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 3155	. . . . . 6 ⊢ ℝ^* ⊆ {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))}
173	7	rnmpt 5829	. . . . . 6 ⊢ ran 𝐺 = {𝑧 ∣ ∃𝑦 ∈ (-1[,]1)𝑧 = if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦))}
174	172, 173	sseqtrri 4006	. . . . 5 ⊢ ℝ^* ⊆ ran 𝐺
175	49, 174	eqssi 3985	. . . 4 ⊢ ran 𝐺 = ℝ^*
176		dffo2 6596	. . . 4 ⊢ (𝐺:(-1[,]1)–onto→ℝ^* ↔ (𝐺:(-1[,]1)⟶ℝ^* ∧ ran 𝐺 = ℝ^*))
177	47, 175, 176	mpbir2an 709	. . 3 ⊢ 𝐺:(-1[,]1)–onto→ℝ^*
178		breq1 5071	. . . . . . 7 ⊢ ((𝐹‘𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) → ((𝐹‘𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
179		breq1 5071	. . . . . . 7 ⊢ (-_𝑒(𝐹‘-𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) → (-_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
180		simpl3 1189	. . . . . . . . 9 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 < 𝑤)
181		simpl1 1187	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ∈ (-1[,]1))
182		simpr 487	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ≤ 𝑧)
183		breq2 5072	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (0 ≤ 𝑦 ↔ 0 ≤ 𝑧))
184		eleq1w 2897	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ (0[,]1) ↔ 𝑧 ∈ (0[,]1)))
185	183, 184	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → ((0 ≤ 𝑦 → 𝑦 ∈ (0[,]1)) ↔ (0 ≤ 𝑧 → 𝑧 ∈ (0[,]1))))
186	18	ex 415	. . . . . . . . . . . 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 1188	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ (-1[,]1))
190	29	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ∈ ℝ)
191	98, 181	sseldi 3967	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ∈ ℝ)
192	98, 189	sseldi 3967	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑤 ∈ ℝ)
193	191, 192, 180	ltled 10790	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 𝑧 ≤ 𝑤)
194	190, 191, 192, 182, 193	letrd 10799	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → 0 ≤ 𝑤)
195		breq2 5072	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (0 ≤ 𝑦 ↔ 0 ≤ 𝑤))
196		eleq1w 2897	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ (0[,]1) ↔ 𝑤 ∈ (0[,]1)))
197	195, 196	imbi12d 347	. . . . . . . . . . . 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 7081	. . . . . . . . . . 11 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1))) → (𝑧 < 𝑤 ↔ (𝐹‘𝑧) < (𝐹‘𝑤)))
201	136, 200	mpan 688	. . . . . . . . . 10 ⊢ ((𝑧 ∈ (0[,]1) ∧ 𝑤 ∈ (0[,]1)) → (𝑧 < 𝑤 ↔ (𝐹‘𝑧) < (𝐹‘𝑤)))
202	188, 199, 201	syl2anc 586	. . . . . . . . 9 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → (𝑧 < 𝑤 ↔ (𝐹‘𝑧) < (𝐹‘𝑤)))
203	180, 202	mpbid 234	. . . . . . . 8 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → (𝐹‘𝑧) < (𝐹‘𝑤))
204	194	iftrued 4477	. . . . . . . 8 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) = (𝐹‘𝑤))
205	203, 204	breqtrrd 5096	. . . . . . 7 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ 0 ≤ 𝑧) → (𝐹‘𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
206		breq2 5072	. . . . . . . 8 ⊢ ((𝐹‘𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) → (-_𝑒(𝐹‘-𝑧) < (𝐹‘𝑤) ↔ -_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
207		breq2 5072	. . . . . . . 8 ⊢ (-_𝑒(𝐹‘-𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) → (-_𝑒(𝐹‘-𝑧) < -_𝑒(𝐹‘-𝑤) ↔ -_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
208		simpl1 1187	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → 𝑧 ∈ (-1[,]1))
209		simpr 487	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → ¬ 0 ≤ 𝑧)
210	183	notbid 320	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → (¬ 0 ≤ 𝑦 ↔ ¬ 0 ≤ 𝑧))
211		negeq 10880	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑧 → -𝑦 = -𝑧)
212	211	eleq1d 2899	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → (-𝑦 ∈ (0[,]1) ↔ -𝑧 ∈ (0[,]1)))
213	210, 212	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → ((¬ 0 ≤ 𝑦 → -𝑦 ∈ (0[,]1)) ↔ (¬ 0 ≤ 𝑧 → -𝑧 ∈ (0[,]1))))
214	41	ex 415	. . . . . . . . . . . . . . 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 483	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -𝑧 ∈ (0[,]1))
218	23	ffvelrni 6852	. . . . . . . . . . . 12 ⊢ (-𝑧 ∈ (0[,]1) → (𝐹‘-𝑧) ∈ (0[,]+∞))
219	217, 218	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ (0[,]+∞))
220	8, 219	sseldi 3967	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ ℝ^*)
221	220	xnegcld 12696	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -_𝑒(𝐹‘-𝑧) ∈ ℝ^*)
222	85	a1i 11	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 ∈ ℝ^*)
223		simpll2 1209	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑤 ∈ (-1[,]1))
224		simpr 487	. . . . . . . . . . . 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	ffvelrni 6852	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (0[,]1) → (𝐹‘𝑤) ∈ (0[,]+∞))
227	225, 226	syl 17	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘𝑤) ∈ (0[,]+∞))
228	8, 227	sseldi 3967	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘𝑤) ∈ ℝ^*)
229	209	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → ¬ 0 ≤ 𝑧)
230		simpll1 1208	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 ∈ (-1[,]1))
231	98, 230	sseldi 3967	. . . . . . . . . . . . . . 15 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 ∈ ℝ)
232		ltnle 10722	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ ∧ 0 ∈ ℝ) → (𝑧 < 0 ↔ ¬ 0 ≤ 𝑧))
233	231, 29, 232	sylancl 588	. . . . . . . . . . . . . 14 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝑧 < 0 ↔ ¬ 0 ≤ 𝑧))
234	229, 233	mpbird 259	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 𝑧 < 0)
235	231	lt0neg1d 11211	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝑧 < 0 ↔ 0 < -𝑧))
236	234, 235	mpbid 234	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 < -𝑧)
237		isorel 7081	. . . . . . . . . . . . . 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 589	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (0 < -𝑧 ↔ (𝐹‘0) < (𝐹‘-𝑧)))
240	236, 239	mpbid 234	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (𝐹‘0) < (𝐹‘-𝑧))
241	130, 240	eqbrtrrid 5104	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 < (𝐹‘-𝑧))
242		xlt0neg2 12616	. . . . . . . . . . 11 ⊢ ((𝐹‘-𝑧) ∈ ℝ^* → (0 < (𝐹‘-𝑧) ↔ -_𝑒(𝐹‘-𝑧) < 0))
243	220, 242	syl 17	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → (0 < (𝐹‘-𝑧) ↔ -_𝑒(𝐹‘-𝑧) < 0))
244	241, 243	mpbid 234	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -_𝑒(𝐹‘-𝑧) < 0)
245		elxrge0 12848	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑤) ∈ (0[,]+∞) ↔ ((𝐹‘𝑤) ∈ ℝ^* ∧ 0 ≤ (𝐹‘𝑤)))
246	245	simprbi 499	. . . . . . . . . 10 ⊢ ((𝐹‘𝑤) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝑤))
247	227, 246	syl 17	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → 0 ≤ (𝐹‘𝑤))
248	221, 222, 228, 244, 247	xrltletrd 12557	. . . . . . . 8 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ 0 ≤ 𝑤) → -_𝑒(𝐹‘-𝑧) < (𝐹‘𝑤))
249		simpll3 1210	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑧 < 𝑤)
250		simpll1 1208	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑧 ∈ (-1[,]1))
251	98, 250	sseldi 3967	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑧 ∈ ℝ)
252		simpll2 1209	. . . . . . . . . . . . 13 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑤 ∈ (-1[,]1))
253	98, 252	sseldi 3967	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → 𝑤 ∈ ℝ)
254	251, 253	ltnegd 11220	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝑧 < 𝑤 ↔ -𝑤 < -𝑧))
255	249, 254	mpbid 234	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -𝑤 < -𝑧)
256		simpr 487	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → ¬ 0 ≤ 𝑤)
257	195	notbid 320	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (¬ 0 ≤ 𝑦 ↔ ¬ 0 ≤ 𝑤))
258		negeq 10880	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 → -𝑦 = -𝑤)
259	258	eleq1d 2899	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (-𝑦 ∈ (0[,]1) ↔ -𝑤 ∈ (0[,]1)))
260	257, 259	imbi12d 347	. . . . . . . . . . . . 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 483	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -𝑧 ∈ (0[,]1))
264		isorel 7081	. . . . . . . . . . . 12 ⊢ ((𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ (-𝑤 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1))) → (-𝑤 < -𝑧 ↔ (𝐹‘-𝑤) < (𝐹‘-𝑧)))
265	136, 264	mpan 688	. . . . . . . . . . 11 ⊢ ((-𝑤 ∈ (0[,]1) ∧ -𝑧 ∈ (0[,]1)) → (-𝑤 < -𝑧 ↔ (𝐹‘-𝑤) < (𝐹‘-𝑧)))
266	262, 263, 265	syl2anc 586	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (-𝑤 < -𝑧 ↔ (𝐹‘-𝑤) < (𝐹‘-𝑧)))
267	255, 266	mpbid 234	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑤) < (𝐹‘-𝑧))
268	23	ffvelrni 6852	. . . . . . . . . . . 12 ⊢ (-𝑤 ∈ (0[,]1) → (𝐹‘-𝑤) ∈ (0[,]+∞))
269	262, 268	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑤) ∈ (0[,]+∞))
270	8, 269	sseldi 3967	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑤) ∈ ℝ^*)
271	263, 218	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ (0[,]+∞))
272	8, 271	sseldi 3967	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → (𝐹‘-𝑧) ∈ ℝ^*)
273		xltneg 12613	. . . . . . . . . 10 ⊢ (((𝐹‘-𝑤) ∈ ℝ^* ∧ (𝐹‘-𝑧) ∈ ℝ^*) → ((𝐹‘-𝑤) < (𝐹‘-𝑧) ↔ -_𝑒(𝐹‘-𝑧) < -_𝑒(𝐹‘-𝑤)))
274	270, 272, 273	syl2anc 586	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → ((𝐹‘-𝑤) < (𝐹‘-𝑧) ↔ -_𝑒(𝐹‘-𝑧) < -_𝑒(𝐹‘-𝑤)))
275	267, 274	mpbid 234	. . . . . . . 8 ⊢ ((((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) ∧ ¬ 0 ≤ 𝑤) → -_𝑒(𝐹‘-𝑧) < -_𝑒(𝐹‘-𝑤))
276	206, 207, 248, 275	ifbothda 4506	. . . . . . 7 ⊢ (((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) ∧ ¬ 0 ≤ 𝑧) → -_𝑒(𝐹‘-𝑧) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
277	178, 179, 205, 276	ifbothda 4506	. . . . . 6 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1) ∧ 𝑧 < 𝑤) → if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
278	277	3expia 1117	. . . . 5 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → (𝑧 < 𝑤 → if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
279		fveq2 6672	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
280	211	fveq2d 6676	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝐹‘-𝑦) = (𝐹‘-𝑧))
281		xnegeq 12603	. . . . . . . . 9 ⊢ ((𝐹‘-𝑦) = (𝐹‘-𝑧) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑧))
282	280, 281	syl 17	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑧))
283	183, 279, 282	ifbieq12d 4496	. . . . . . 7 ⊢ (𝑦 = 𝑧 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)))
284		fvex 6685	. . . . . . . 8 ⊢ (𝐹‘𝑧) ∈ V
285		xnegex 12604	. . . . . . . 8 ⊢ -_𝑒(𝐹‘-𝑧) ∈ V
286	284, 285	ifex 4517	. . . . . . 7 ⊢ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) ∈ V
287	283, 7, 286	fvmpt 6770	. . . . . 6 ⊢ (𝑧 ∈ (-1[,]1) → (𝐺‘𝑧) = if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)))
288		fveq2 6672	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
289	258	fveq2d 6676	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝐹‘-𝑦) = (𝐹‘-𝑤))
290		xnegeq 12603	. . . . . . . . 9 ⊢ ((𝐹‘-𝑦) = (𝐹‘-𝑤) → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑤))
291	289, 290	syl 17	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → -_𝑒(𝐹‘-𝑦) = -_𝑒(𝐹‘-𝑤))
292	195, 288, 291	ifbieq12d 4496	. . . . . . 7 ⊢ (𝑦 = 𝑤 → if(0 ≤ 𝑦, (𝐹‘𝑦), -_𝑒(𝐹‘-𝑦)) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
293		fvex 6685	. . . . . . . 8 ⊢ (𝐹‘𝑤) ∈ V
294		xnegex 12604	. . . . . . . 8 ⊢ -_𝑒(𝐹‘-𝑤) ∈ V
295	293, 294	ifex 4517	. . . . . . 7 ⊢ if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)) ∈ V
296	292, 7, 295	fvmpt 6770	. . . . . 6 ⊢ (𝑤 ∈ (-1[,]1) → (𝐺‘𝑤) = if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤)))
297	287, 296	breqan12d 5084	. . . . 5 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → ((𝐺‘𝑧) < (𝐺‘𝑤) ↔ if(0 ≤ 𝑧, (𝐹‘𝑧), -_𝑒(𝐹‘-𝑧)) < if(0 ≤ 𝑤, (𝐹‘𝑤), -_𝑒(𝐹‘-𝑤))))
298	278, 297	sylibrd 261	. . . 4 ⊢ ((𝑧 ∈ (-1[,]1) ∧ 𝑤 ∈ (-1[,]1)) → (𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤)))
299	298	rgen2 3205	. . 3 ⊢ ∀𝑧 ∈ (-1[,]1)∀𝑤 ∈ (-1[,]1)(𝑧 < 𝑤 → (𝐺‘𝑧) < (𝐺‘𝑤))
300		soisoi 7083	. . 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 17839	. . . . . 6 ⊢ ≤ ∈ TosetRel
303	302	elexi 3515	. . . . 5 ⊢ ≤ ∈ V
304	303	inex1 5223	. . . 4 ⊢ ( ≤ ∩ ((-1[,]1) × (-1[,]1))) ∈ V
305		ssid 3991	. . . . . . 7 ⊢ ℝ^* ⊆ ℝ^*
306		leiso 13820	. . . . . . 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 232	. . . . 5 ⊢ 𝐺 Isom ≤ , ≤ ((-1[,]1), ℝ^*)
309		isores1 7089	. . . . 5 ⊢ (𝐺 Isom ≤ , ≤ ((-1[,]1), ℝ^) ↔ 𝐺 Isom ( ≤ ∩ ((-1[,]1) × (-1[,]1))), ≤ ((-1[,]1), ℝ^))
310	308, 309	mpbi 232	. . . 4 ⊢ 𝐺 Isom ( ≤ ∩ ((-1[,]1) × (-1[,]1))), ≤ ((-1[,]1), ℝ^*)
311		tsrps 17833	. . . . . . . 8 ⊢ ( ≤ ∈ TosetRel → ≤ ∈ PosetRel)
312	302, 311	ax-mp 5	. . . . . . 7 ⊢ ≤ ∈ PosetRel
313		ledm 17836	. . . . . . . 8 ⊢ ℝ^* = dom ≤
314	313	psssdm 17828	. . . . . . 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 2832	. . . . 5 ⊢ (-1[,]1) = dom ( ≤ ∩ ((-1[,]1) × (-1[,]1)))
317	316, 313	ordthmeo 22412	. . . 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 1457	. . 3 ⊢ 𝐺 ∈ ((ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))Homeo(ordTop‘ ≤ ))
319		xrhmeo.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
320		eqid 2823	. . . . . . 7 ⊢ (ordTop‘ ≤ ) = (ordTop‘ ≤ )
321	319, 320	xrrest2 23418	. . . . . 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 21833	. . . . 5 ⊢ ((ordTop‘ ≤ ) ↾_t (-1[,]1)) = (ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))
324	322, 323	eqtri 2846	. . . 4 ⊢ (𝐽 ↾_t (-1[,]1)) = (ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))
325	324	oveq1i 7168	. . 3 ⊢ ((𝐽 ↾_t (-1[,]1))Homeo(ordTop‘ ≤ )) = ((ordTop‘( ≤ ∩ ((-1[,]1) × (-1[,]1))))Homeo(ordTop‘ ≤ ))
326	318, 325	eleqtrri 2914	. 2 ⊢ 𝐺 ∈ ((𝐽 ↾_t (-1[,]1))Homeo(ordTop‘ ≤ ))
327	301, 326	pm3.2i 473	1 ⊢ (𝐺 Isom < , < ((-1[,]1), ℝ^*) ∧ 𝐺 ∈ ((𝐽 ↾_t (-1[,]1))Homeo(ordTop‘ ≤ )))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 {cab 2801 ≠ wne 3018 ∀wral 3140 ∃wrex 3141 Vcvv 3496 ∩ cin 3937 ⊆ wss 3938 ifcif 4469 class class class wbr 5068 ↦ cmpt 5148 Po wpo 5474 Or wor 5475 × cxp 5555 ^◡ccnv 5556 dom cdm 5557 ran crn 5558 ⟶wf 6353 –onto→wfo 6355 –1-1-onto→wf1o 6356 ‘cfv 6357 Isom wiso 6358 (class class class)co 7158 ℝcr 10538 0cc0 10539 1c1 10540 + caddc 10542 +∞cpnf 10674 ℝ^*cxr 10676 < clt 10677 ≤ cle 10678 − cmin 10872 -cneg 10873 / cdiv 11299 -_𝑒cxne 12507 [,]cicc 12744 ↾_t crest 16696 TopOpenctopn 16697 ordTopcordt 16774 PosetRelcps 17810 TosetRel ctsr 17811 ℂ_fldccnfld 20547 Homeochmeo 22363 IIcii 23485

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616 ax-pre-sup 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-iin 4924 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-isom 6366 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-om 7583 df-1st 7691 df-2nd 7692 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-oadd 8108 df-er 8291 df-map 8410 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-fi 8877 df-sup 8908 df-inf 8909 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-div 11300 df-nn 11641 df-2 11703 df-3 11704 df-4 11705 df-5 11706 df-6 11707 df-7 11708 df-8 11709 df-9 11710 df-n0 11901 df-z 11985 df-dec 12102 df-uz 12247 df-q 12352 df-rp 12393 df-xneg 12510 df-xadd 12511 df-xmul 12512 df-ioo 12745 df-ioc 12746 df-ico 12747 df-icc 12748 df-fz 12896 df-seq 13373 df-exp 13433 df-cj 14460 df-re 14461 df-im 14462 df-sqrt 14596 df-abs 14597 df-struct 16487 df-ndx 16488 df-slot 16489 df-base 16491 df-plusg 16580 df-mulr 16581 df-starv 16582 df-tset 16586 df-ple 16587 df-ds 16589 df-unif 16590 df-rest 16698 df-topn 16699 df-topgen 16719 df-ordt 16776 df-ps 17812 df-tsr 17813 df-psmet 20539 df-xmet 20540 df-met 20541 df-bl 20542 df-mopn 20543 df-cnfld 20548 df-top 21504 df-topon 21521 df-topsp 21543 df-bases 21556 df-cn 21837 df-hmeo 22365 df-xms 22932 df-ms 22933 df-ii 23487

This theorem is referenced by: xrhmph 23553

W3C validator