xrge0iifcnv

Description: Define a bijection from [ 0 , 1 ] onto [ 0 , +oo ] . (Contributed by Thierry Arnoux, 29-Mar-2017)

		Ref	Expression
	Hypothesis	xrge0iifhmeo.1	$⊢ F = (x \in [0, 1] ⟼ if (x = 0, +∞, - \log x))$
	Assertion	xrge0iifcnv	$⊢ (F : [0, 1] \underset{1-1 onto}{⟶} [0, +∞] \land F^{-1} = (y \in [0, +∞] ⟼ if (y = +∞, 0, e^{- y})))$

Proof

Step	Hyp	Ref	Expression
1		xrge0iifhmeo.1	$⊢ F = (x \in [0, 1] ⟼ if (x = 0, +∞, - \log x))$
2		0xr	$⊢ 0 \in ℝ^{*}$
3		pnfxr	$⊢ +∞ \in ℝ^{*}$
4		0lepnf	$⊢ 0 \leq +∞$
5		ubicc2	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land 0 \leq +∞) \to +∞ \in [0, +∞]$
6	2 3 4 5	mp3an	$⊢ +∞ \in [0, +∞]$
7	6	a1i	$⊢ (x \in [0, 1] \land x = 0) \to +∞ \in [0, +∞]$
8		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
9		uncom	$⊢ \{0\} \cup (0, 1] = (0, 1] \cup \{0\}$
10		1xr	$⊢ 1 \in ℝ^{*}$
11		0le1	$⊢ 0 \leq 1$
12		snunioc	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{} \land 0 \leq 1) \to \{0\} \cup (0, 1] = [0, 1]$
13	2 10 11 12	mp3an	$⊢ \{0\} \cup (0, 1] = [0, 1]$
14	9 13	eqtr3i	$⊢ (0, 1] \cup \{0\} = [0, 1]$
15	14	eleq2i	$⊢ x \in ((0, 1] \cup \{0\}) \leftrightarrow x \in [0, 1]$
16		elun	$⊢ x \in ((0, 1] \cup \{0\}) \leftrightarrow (x \in (0, 1] \lor x \in \{0\})$
17	15 16	bitr3i	$⊢ x \in [0, 1] \leftrightarrow (x \in (0, 1] \lor x \in \{0\})$
18		pm2.53	$⊢ (x \in (0, 1] \lor x \in \{0\}) \to (\neg x \in (0, 1] \to x \in \{0\})$
19	17 18	sylbi	$⊢ x \in [0, 1] \to (\neg x \in (0, 1] \to x \in \{0\})$
20		elsni	$⊢ x \in \{0\} \to x = 0$
21	19 20	syl6	$⊢ x \in [0, 1] \to (\neg x \in (0, 1] \to x = 0)$
22	21	con1d	$⊢ x \in [0, 1] \to (\neg x = 0 \to x \in (0, 1])$
23	22	imp	$⊢ (x \in [0, 1] \land \neg x = 0) \to x \in (0, 1]$
24		0le0	$⊢ 0 \leq 0$
25		1re	$⊢ 1 \in ℝ$
26		ltpnf	$⊢ 1 \in ℝ \to 1 < +∞$
27	25 26	ax-mp	$⊢ 1 < +∞$
28		iocssioo	$⊢ ((0 \in ℝ^{} \land +∞ \in ℝ^{}) \land (0 \leq 0 \land 1 < +∞)) \to (0, 1] \subseteq (0, +∞)$
29	2 3 24 27 28	mp4an	$⊢ (0, 1] \subseteq (0, +∞)$
30		ioorp	$⊢ (0, +∞) = ℝ^{+}$
31	29 30	sseqtri	$⊢ (0, 1] \subseteq ℝ^{+}$
32	31	sseli	$⊢ x \in (0, 1] \to x \in ℝ^{+}$
33	32	relogcld	$⊢ x \in (0, 1] \to \log x \in ℝ$
34	33	renegcld	$⊢ x \in (0, 1] \to - \log x \in ℝ$
35	34	rexrd	$⊢ x \in (0, 1] \to - \log x \in ℝ^{*}$
36		elioc1	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{}) \to (x \in (0, 1] \leftrightarrow (x \in ℝ^{*} \land 0 < x \land x \leq 1))$
37	2 10 36	mp2an	$⊢ x \in (0, 1] \leftrightarrow (x \in ℝ^{*} \land 0 < x \land x \leq 1)$
38	37	simp3bi	$⊢ x \in (0, 1] \to x \leq 1$
39		1rp	$⊢ 1 \in ℝ^{+}$
40	39	a1i	$⊢ x \in (0, 1] \to 1 \in ℝ^{+}$
41	32 40	logled	$⊢ x \in (0, 1] \to (x \leq 1 \leftrightarrow \log x \leq \log 1)$
42	38 41	mpbid	$⊢ x \in (0, 1] \to \log x \leq \log 1$
43		log1	$⊢ \log 1 = 0$
44	42 43	breqtrdi	$⊢ x \in (0, 1] \to \log x \leq 0$
45	33	le0neg1d	$⊢ x \in (0, 1] \to (\log x \leq 0 \leftrightarrow 0 \leq - \log x)$
46	44 45	mpbid	$⊢ x \in (0, 1] \to 0 \leq - \log x$
47		ltpnf	$⊢ - \log x \in ℝ \to - \log x < +∞$
48	34 47	syl	$⊢ x \in (0, 1] \to - \log x < +∞$
49		elico1	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{}) \to (- \log x \in [0, +∞) \leftrightarrow (- \log x \in ℝ^{*} \land 0 \leq - \log x \land - \log x < +∞))$
50	2 3 49	mp2an	$⊢ - \log x \in [0, +∞) \leftrightarrow (- \log x \in ℝ^{*} \land 0 \leq - \log x \land - \log x < +∞)$
51	35 46 48 50	syl3anbrc	$⊢ x \in (0, 1] \to - \log x \in [0, +∞)$
52	23 51	syl	$⊢ (x \in [0, 1] \land \neg x = 0) \to - \log x \in [0, +∞)$
53	8 52	sseldi	$⊢ (x \in [0, 1] \land \neg x = 0) \to - \log x \in [0, +∞]$
54	7 53	ifclda	$⊢ x \in [0, 1] \to if (x = 0, +∞, - \log x) \in [0, +∞]$
55	54	adantl	$⊢ (⊤ \land x \in [0, 1]) \to if (x = 0, +∞, - \log x) \in [0, +∞]$
56		0elunit	$⊢ 0 \in [0, 1]$
57	56	a1i	$⊢ (y \in [0, +∞] \land y = +∞) \to 0 \in [0, 1]$
58		iocssicc	$⊢ (0, 1] \subseteq [0, 1]$
59		snunico	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land 0 \leq +∞) \to [0, +∞) \cup \{+∞\} = [0, +∞]$
60	2 3 4 59	mp3an	$⊢ [0, +∞) \cup \{+∞\} = [0, +∞]$
61	60	eleq2i	$⊢ y \in ([0, +∞) \cup \{+∞\}) \leftrightarrow y \in [0, +∞]$
62		elun	$⊢ y \in ([0, +∞) \cup \{+∞\}) \leftrightarrow (y \in [0, +∞) \lor y \in \{+∞\})$
63	61 62	bitr3i	$⊢ y \in [0, +∞] \leftrightarrow (y \in [0, +∞) \lor y \in \{+∞\})$
64		pm2.53	$⊢ (y \in [0, +∞) \lor y \in \{+∞\}) \to (\neg y \in [0, +∞) \to y \in \{+∞\})$
65	63 64	sylbi	$⊢ y \in [0, +∞] \to (\neg y \in [0, +∞) \to y \in \{+∞\})$
66		elsni	$⊢ y \in \{+∞\} \to y = +∞$
67	65 66	syl6	$⊢ y \in [0, +∞] \to (\neg y \in [0, +∞) \to y = +∞)$
68	67	con1d	$⊢ y \in [0, +∞] \to (\neg y = +∞ \to y \in [0, +∞))$
69	68	imp	$⊢ (y \in [0, +∞] \land \neg y = +∞) \to y \in [0, +∞)$
70		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
71	70	sseli	$⊢ y \in [0, +∞) \to y \in ℝ$
72	71	renegcld	$⊢ y \in [0, +∞) \to - y \in ℝ$
73	72	reefcld	$⊢ y \in [0, +∞) \to e^{- y} \in ℝ$
74	73	rexrd	$⊢ y \in [0, +∞) \to e^{- y} \in ℝ^{*}$
75		efgt0	$⊢ - y \in ℝ \to 0 < e^{- y}$
76	72 75	syl	$⊢ y \in [0, +∞) \to 0 < e^{- y}$
77		elico1	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{}) \to (y \in [0, +∞) \leftrightarrow (y \in ℝ^{*} \land 0 \leq y \land y < +∞))$
78	2 3 77	mp2an	$⊢ y \in [0, +∞) \leftrightarrow (y \in ℝ^{*} \land 0 \leq y \land y < +∞)$
79	78	simp2bi	$⊢ y \in [0, +∞) \to 0 \leq y$
80	71	le0neg2d	$⊢ y \in [0, +∞) \to (0 \leq y \leftrightarrow - y \leq 0)$
81	79 80	mpbid	$⊢ y \in [0, +∞) \to - y \leq 0$
82		0re	$⊢ 0 \in ℝ$
83		efle	$⊢ (- y \in ℝ \land 0 \in ℝ) \to (- y \leq 0 \leftrightarrow e^{- y} \leq e^{0})$
84	72 82 83	sylancl	$⊢ y \in [0, +∞) \to (- y \leq 0 \leftrightarrow e^{- y} \leq e^{0})$
85	81 84	mpbid	$⊢ y \in [0, +∞) \to e^{- y} \leq e^{0}$
86		ef0	$⊢ e^{0} = 1$
87	85 86	breqtrdi	$⊢ y \in [0, +∞) \to e^{- y} \leq 1$
88		elioc1	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{}) \to (e^{- y} \in (0, 1] \leftrightarrow (e^{- y} \in ℝ^{*} \land 0 < e^{- y} \land e^{- y} \leq 1))$
89	2 10 88	mp2an	$⊢ e^{- y} \in (0, 1] \leftrightarrow (e^{- y} \in ℝ^{*} \land 0 < e^{- y} \land e^{- y} \leq 1)$
90	74 76 87 89	syl3anbrc	$⊢ y \in [0, +∞) \to e^{- y} \in (0, 1]$
91	69 90	syl	$⊢ (y \in [0, +∞] \land \neg y = +∞) \to e^{- y} \in (0, 1]$
92	58 91	sseldi	$⊢ (y \in [0, +∞] \land \neg y = +∞) \to e^{- y} \in [0, 1]$
93	57 92	ifclda	$⊢ y \in [0, +∞] \to if (y = +∞, 0, e^{- y}) \in [0, 1]$
94	93	adantl	$⊢ (⊤ \land y \in [0, +∞]) \to if (y = +∞, 0, e^{- y}) \in [0, 1]$
95		eqeq2	$⊢ 0 = if (y = +∞, 0, e^{- y}) \to (x = 0 \leftrightarrow x = if (y = +∞, 0, e^{- y}))$
96	95	bibi1d	$⊢ 0 = if (y = +∞, 0, e^{- y}) \to ((x = 0 \leftrightarrow y = if (x = 0, +∞, - \log x)) \leftrightarrow (x = if (y = +∞, 0, e^{- y}) \leftrightarrow y = if (x = 0, +∞, - \log x)))$
97		eqeq2	$⊢ e^{- y} = if (y = +∞, 0, e^{- y}) \to (x = e^{- y} \leftrightarrow x = if (y = +∞, 0, e^{- y}))$
98	97	bibi1d	$⊢ e^{- y} = if (y = +∞, 0, e^{- y}) \to ((x = e^{- y} \leftrightarrow y = if (x = 0, +∞, - \log x)) \leftrightarrow (x = if (y = +∞, 0, e^{- y}) \leftrightarrow y = if (x = 0, +∞, - \log x)))$
99		simpr	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land y = +∞) \to y = +∞$
100		iftrue	$⊢ x = 0 \to if (x = 0, +∞, - \log x) = +∞$
101	100	eqeq2d	$⊢ x = 0 \to (y = if (x = 0, +∞, - \log x) \leftrightarrow y = +∞)$
102	99 101	syl5ibrcom	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land y = +∞) \to (x = 0 \to y = if (x = 0, +∞, - \log x))$
103		ubico	$⊢ (0 \in ℝ \land +∞ \in ℝ^{*}) \to \neg +∞ \in [0, +∞)$
104	82 3 103	mp2an	$⊢ \neg +∞ \in [0, +∞)$
105	104	nelir	$⊢ +∞ \notin [0, +∞)$
106		neleq1	$⊢ y = +∞ \to (y \notin [0, +∞) \leftrightarrow +∞ \notin [0, +∞))$
107	106	adantl	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land y = +∞) \to (y \notin [0, +∞) \leftrightarrow +∞ \notin [0, +∞))$
108	105 107	mpbiri	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land y = +∞) \to y \notin [0, +∞)$
109		neleq1	$⊢ y = if (x = 0, +∞, - \log x) \to (y \notin [0, +∞) \leftrightarrow if (x = 0, +∞, - \log x) \notin [0, +∞))$
110	108 109	syl5ibcom	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land y = +∞) \to (y = if (x = 0, +∞, - \log x) \to if (x = 0, +∞, - \log x) \notin [0, +∞))$
111		df-nel	$⊢ if (x = 0, +∞, - \log x) \notin [0, +∞) \leftrightarrow \neg if (x = 0, +∞, - \log x) \in [0, +∞)$
112		iffalse	$⊢ \neg x = 0 \to if (x = 0, +∞, - \log x) = - \log x$
113	112	adantl	$⊢ (x \in [0, 1] \land \neg x = 0) \to if (x = 0, +∞, - \log x) = - \log x$
114	113 52	eqeltrd	$⊢ (x \in [0, 1] \land \neg x = 0) \to if (x = 0, +∞, - \log x) \in [0, +∞)$
115	114	ex	$⊢ x \in [0, 1] \to (\neg x = 0 \to if (x = 0, +∞, - \log x) \in [0, +∞))$
116	115	ad2antrr	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land y = +∞) \to (\neg x = 0 \to if (x = 0, +∞, - \log x) \in [0, +∞))$
117	116	con1d	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land y = +∞) \to (\neg if (x = 0, +∞, - \log x) \in [0, +∞) \to x = 0)$
118	111 117	syl5bi	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land y = +∞) \to (if (x = 0, +∞, - \log x) \notin [0, +∞) \to x = 0)$
119	110 118	syld	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land y = +∞) \to (y = if (x = 0, +∞, - \log x) \to x = 0)$
120	102 119	impbid	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land y = +∞) \to (x = 0 \leftrightarrow y = if (x = 0, +∞, - \log x))$
121		eqeq2	$⊢ +∞ = if (x = 0, +∞, - \log x) \to (y = +∞ \leftrightarrow y = if (x = 0, +∞, - \log x))$
122	121	bibi2d	$⊢ +∞ = if (x = 0, +∞, - \log x) \to ((x = e^{- y} \leftrightarrow y = +∞) \leftrightarrow (x = e^{- y} \leftrightarrow y = if (x = 0, +∞, - \log x)))$
123		eqeq2	$⊢ - \log x = if (x = 0, +∞, - \log x) \to (y = - \log x \leftrightarrow y = if (x = 0, +∞, - \log x))$
124	123	bibi2d	$⊢ - \log x = if (x = 0, +∞, - \log x) \to ((x = e^{- y} \leftrightarrow y = - \log x) \leftrightarrow (x = e^{- y} \leftrightarrow y = if (x = 0, +∞, - \log x)))$
125	82	a1i	$⊢ (y \in [0, +∞] \land \neg y = +∞) \to 0 \in ℝ$
126	69 76	syl	$⊢ (y \in [0, +∞] \land \neg y = +∞) \to 0 < e^{- y}$
127	125 126	ltned	$⊢ (y \in [0, +∞] \land \neg y = +∞) \to 0 \neq e^{- y}$
128	127	adantll	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land \neg y = +∞) \to 0 \neq e^{- y}$
129	128	neneqd	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land \neg y = +∞) \to \neg 0 = e^{- y}$
130		eqeq1	$⊢ x = 0 \to (x = e^{- y} \leftrightarrow 0 = e^{- y})$
131	130	notbid	$⊢ x = 0 \to (\neg x = e^{- y} \leftrightarrow \neg 0 = e^{- y})$
132	129 131	syl5ibrcom	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land \neg y = +∞) \to (x = 0 \to \neg x = e^{- y})$
133	132	imp	$⊢ (((x \in [0, 1] \land y \in [0, +∞]) \land \neg y = +∞) \land x = 0) \to \neg x = e^{- y}$
134		simplr	$⊢ (((x \in [0, 1] \land y \in [0, +∞]) \land \neg y = +∞) \land x = 0) \to \neg y = +∞$
135	133 134	2falsed	$⊢ (((x \in [0, 1] \land y \in [0, +∞]) \land \neg y = +∞) \land x = 0) \to (x = e^{- y} \leftrightarrow y = +∞)$
136		eqcom	$⊢ x = e^{- y} \leftrightarrow e^{- y} = x$
137	136	a1i	$⊢ (x \in (0, 1] \land y \in [0, +∞)) \to (x = e^{- y} \leftrightarrow e^{- y} = x)$
138		relogeftb	$⊢ (x \in ℝ^{+} \land - y \in ℝ) \to (\log x = - y \leftrightarrow e^{- y} = x)$
139	32 72 138	syl2an	$⊢ (x \in (0, 1] \land y \in [0, +∞)) \to (\log x = - y \leftrightarrow e^{- y} = x)$
140	33	recnd	$⊢ x \in (0, 1] \to \log x \in ℂ$
141	71	recnd	$⊢ y \in [0, +∞) \to y \in ℂ$
142		negcon2	$⊢ (\log x \in ℂ \land y \in ℂ) \to (\log x = - y \leftrightarrow y = - \log x)$
143	140 141 142	syl2an	$⊢ (x \in (0, 1] \land y \in [0, +∞)) \to (\log x = - y \leftrightarrow y = - \log x)$
144	137 139 143	3bitr2d	$⊢ (x \in (0, 1] \land y \in [0, +∞)) \to (x = e^{- y} \leftrightarrow y = - \log x)$
145	23 69 144	syl2an	$⊢ ((x \in [0, 1] \land \neg x = 0) \land (y \in [0, +∞] \land \neg y = +∞)) \to (x = e^{- y} \leftrightarrow y = - \log x)$
146	145	an4s	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land (\neg x = 0 \land \neg y = +∞)) \to (x = e^{- y} \leftrightarrow y = - \log x)$
147	146	anass1rs	$⊢ (((x \in [0, 1] \land y \in [0, +∞]) \land \neg y = +∞) \land \neg x = 0) \to (x = e^{- y} \leftrightarrow y = - \log x)$
148	122 124 135 147	ifbothda	$⊢ ((x \in [0, 1] \land y \in [0, +∞]) \land \neg y = +∞) \to (x = e^{- y} \leftrightarrow y = if (x = 0, +∞, - \log x))$
149	96 98 120 148	ifbothda	$⊢ (x \in [0, 1] \land y \in [0, +∞]) \to (x = if (y = +∞, 0, e^{- y}) \leftrightarrow y = if (x = 0, +∞, - \log x))$
150	149	adantl	$⊢ (⊤ \land (x \in [0, 1] \land y \in [0, +∞])) \to (x = if (y = +∞, 0, e^{- y}) \leftrightarrow y = if (x = 0, +∞, - \log x))$
151	1 55 94 150	f1ocnv2d	$⊢ ⊤ \to (F : [0, 1] \underset{1-1 onto}{⟶} [0, +∞] \land F^{-1} = (y \in [0, +∞] ⟼ if (y = +∞, 0, e^{- y})))$
152	151	mptru	$⊢ (F : [0, 1] \underset{1-1 onto}{⟶} [0, +∞] \land F^{-1} = (y \in [0, +∞] ⟼ if (y = +∞, 0, e^{- y})))$

Metamath Proof Explorer

Theorem xrge0iifcnv

Proof