Metamath Proof Explorer

Theorem iccpnfcnv

Description: Define a bijection from [ 0 , 1 ] to [ 0 , +oo ] . (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypothesis iccpnfhmeo.f ⊢ F = x ∈ 0 1 ⟼ if x = 1 +∞ x 1 − x
Assertion iccpnfcnv ⊢ F : 0 1 ⟶ 1-1 onto 0 +∞ ∧ F -1 = y ∈ 0 +∞ ⟼ if y = +∞ 1 y 1 + y

Proof

Step Hyp Ref Expression
1 iccpnfhmeo.f ⊢ F = x ∈ 0 1 ⟼ if x = 1 +∞ x 1 − x
2 0xr ⊢ 0 ∈ ℝ *
3 pnfxr ⊢ +∞ ∈ ℝ *
4 0lepnf ⊢ 0 ≤ +∞
5 ubicc2 ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ 0 ≤ +∞ → +∞ ∈ 0 +∞
6 2 3 4 5 mp3an ⊢ +∞ ∈ 0 +∞
7 6 a1i ⊢ x ∈ 0 1 ∧ x = 1 → +∞ ∈ 0 +∞
8 icossicc ⊢ 0 +∞ ⊆ 0 +∞
9 1xr ⊢ 1 ∈ ℝ *
10 0le1 ⊢ 0 ≤ 1
11 snunico ⊢ 0 ∈ ℝ * ∧ 1 ∈ ℝ * ∧ 0 ≤ 1 → 0 1 ∪ 1 = 0 1
12 2 9 10 11 mp3an ⊢ 0 1 ∪ 1 = 0 1
13 12 eleq2i ⊢ x ∈ 0 1 ∪ 1 ↔ x ∈ 0 1
14 elun ⊢ x ∈ 0 1 ∪ 1 ↔ x ∈ 0 1 ∨ x ∈ 1
15 13 14 bitr3i ⊢ x ∈ 0 1 ↔ x ∈ 0 1 ∨ x ∈ 1
16 pm2.53 ⊢ x ∈ 0 1 ∨ x ∈ 1 → ¬ x ∈ 0 1 → x ∈ 1
17 15 16 sylbi ⊢ x ∈ 0 1 → ¬ x ∈ 0 1 → x ∈ 1
18 elsni ⊢ x ∈ 1 → x = 1
19 17 18 syl6 ⊢ x ∈ 0 1 → ¬ x ∈ 0 1 → x = 1
20 19 con1d ⊢ x ∈ 0 1 → ¬ x = 1 → x ∈ 0 1
21 20 imp ⊢ x ∈ 0 1 ∧ ¬ x = 1 → x ∈ 0 1
22 eqid ⊢ x ∈ 0 1 ⟼ x 1 − x = x ∈ 0 1 ⟼ x 1 − x
23 22 icopnfcnv ⊢ x ∈ 0 1 ⟼ x 1 − x : 0 1 ⟶ 1-1 onto 0 +∞ ∧ x ∈ 0 1 ⟼ x 1 − x -1 = y ∈ 0 +∞ ⟼ y 1 + y
24 23 simpli ⊢ x ∈ 0 1 ⟼ x 1 − x : 0 1 ⟶ 1-1 onto 0 +∞
25 f1of ⊢ x ∈ 0 1 ⟼ x 1 − x : 0 1 ⟶ 1-1 onto 0 +∞ → x ∈ 0 1 ⟼ x 1 − x : 0 1 ⟶ 0 +∞
26 24 25 ax-mp ⊢ x ∈ 0 1 ⟼ x 1 − x : 0 1 ⟶ 0 +∞
27 22 fmpt ⊢ ∀ x ∈ 0 1 x 1 − x ∈ 0 +∞ ↔ x ∈ 0 1 ⟼ x 1 − x : 0 1 ⟶ 0 +∞
28 26 27 mpbir ⊢ ∀ x ∈ 0 1 x 1 − x ∈ 0 +∞
29 28 rspec ⊢ x ∈ 0 1 → x 1 − x ∈ 0 +∞
30 21 29 syl ⊢ x ∈ 0 1 ∧ ¬ x = 1 → x 1 − x ∈ 0 +∞
31 8 30 sseldi ⊢ x ∈ 0 1 ∧ ¬ x = 1 → x 1 − x ∈ 0 +∞
32 7 31 ifclda ⊢ x ∈ 0 1 → if x = 1 +∞ x 1 − x ∈ 0 +∞
33 32 adantl ⊢ ⊤ ∧ x ∈ 0 1 → if x = 1 +∞ x 1 − x ∈ 0 +∞
34 1elunit ⊢ 1 ∈ 0 1
35 34 a1i ⊢ y ∈ 0 +∞ ∧ y = +∞ → 1 ∈ 0 1
36 icossicc ⊢ 0 1 ⊆ 0 1
37 snunico ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ 0 ≤ +∞ → 0 +∞ ∪ +∞ = 0 +∞
38 2 3 4 37 mp3an ⊢ 0 +∞ ∪ +∞ = 0 +∞
39 38 eleq2i ⊢ y ∈ 0 +∞ ∪ +∞ ↔ y ∈ 0 +∞
40 elun ⊢ y ∈ 0 +∞ ∪ +∞ ↔ y ∈ 0 +∞ ∨ y ∈ +∞
41 39 40 bitr3i ⊢ y ∈ 0 +∞ ↔ y ∈ 0 +∞ ∨ y ∈ +∞
42 pm2.53 ⊢ y ∈ 0 +∞ ∨ y ∈ +∞ → ¬ y ∈ 0 +∞ → y ∈ +∞
43 41 42 sylbi ⊢ y ∈ 0 +∞ → ¬ y ∈ 0 +∞ → y ∈ +∞
44 elsni ⊢ y ∈ +∞ → y = +∞
45 43 44 syl6 ⊢ y ∈ 0 +∞ → ¬ y ∈ 0 +∞ → y = +∞
46 45 con1d ⊢ y ∈ 0 +∞ → ¬ y = +∞ → y ∈ 0 +∞
47 46 imp ⊢ y ∈ 0 +∞ ∧ ¬ y = +∞ → y ∈ 0 +∞
48 f1ocnv ⊢ x ∈ 0 1 ⟼ x 1 − x : 0 1 ⟶ 1-1 onto 0 +∞ → x ∈ 0 1 ⟼ x 1 − x -1 : 0 +∞ ⟶ 1-1 onto 0 1
49 f1of ⊢ x ∈ 0 1 ⟼ x 1 − x -1 : 0 +∞ ⟶ 1-1 onto 0 1 → x ∈ 0 1 ⟼ x 1 − x -1 : 0 +∞ ⟶ 0 1
50 24 48 49 mp2b ⊢ x ∈ 0 1 ⟼ x 1 − x -1 : 0 +∞ ⟶ 0 1
51 23 simpri ⊢ x ∈ 0 1 ⟼ x 1 − x -1 = y ∈ 0 +∞ ⟼ y 1 + y
52 51 fmpt ⊢ ∀ y ∈ 0 +∞ y 1 + y ∈ 0 1 ↔ x ∈ 0 1 ⟼ x 1 − x -1 : 0 +∞ ⟶ 0 1
53 50 52 mpbir ⊢ ∀ y ∈ 0 +∞ y 1 + y ∈ 0 1
54 53 rspec ⊢ y ∈ 0 +∞ → y 1 + y ∈ 0 1
55 47 54 syl ⊢ y ∈ 0 +∞ ∧ ¬ y = +∞ → y 1 + y ∈ 0 1
56 36 55 sseldi ⊢ y ∈ 0 +∞ ∧ ¬ y = +∞ → y 1 + y ∈ 0 1
57 35 56 ifclda ⊢ y ∈ 0 +∞ → if y = +∞ 1 y 1 + y ∈ 0 1
58 57 adantl ⊢ ⊤ ∧ y ∈ 0 +∞ → if y = +∞ 1 y 1 + y ∈ 0 1
59 eqeq2 ⊢ 1 = if y = +∞ 1 y 1 + y → x = 1 ↔ x = if y = +∞ 1 y 1 + y
60 59 bibi1d ⊢ 1 = if y = +∞ 1 y 1 + y → x = 1 ↔ y = if x = 1 +∞ x 1 − x ↔ x = if y = +∞ 1 y 1 + y ↔ y = if x = 1 +∞ x 1 − x
61 eqeq2 ⊢ y 1 + y = if y = +∞ 1 y 1 + y → x = y 1 + y ↔ x = if y = +∞ 1 y 1 + y
62 61 bibi1d ⊢ y 1 + y = if y = +∞ 1 y 1 + y → x = y 1 + y ↔ y = if x = 1 +∞ x 1 − x ↔ x = if y = +∞ 1 y 1 + y ↔ y = if x = 1 +∞ x 1 − x
63 simpr ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ y = +∞ → y = +∞
64 iftrue ⊢ x = 1 → if x = 1 +∞ x 1 − x = +∞
65 64 eqeq2d ⊢ x = 1 → y = if x = 1 +∞ x 1 − x ↔ y = +∞
66 63 65 syl5ibrcom ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ y = +∞ → x = 1 → y = if x = 1 +∞ x 1 − x
67 pnfnre ⊢ +∞ ∉ ℝ
68 neleq1 ⊢ y = +∞ → y ∉ ℝ ↔ +∞ ∉ ℝ
69 68 adantl ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ y = +∞ → y ∉ ℝ ↔ +∞ ∉ ℝ
70 67 69 mpbiri ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ y = +∞ → y ∉ ℝ
71 neleq1 ⊢ y = if x = 1 +∞ x 1 − x → y ∉ ℝ ↔ if x = 1 +∞ x 1 − x ∉ ℝ
72 70 71 syl5ibcom ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ y = +∞ → y = if x = 1 +∞ x 1 − x → if x = 1 +∞ x 1 − x ∉ ℝ
73 df-nel ⊢ if x = 1 +∞ x 1 − x ∉ ℝ ↔ ¬ if x = 1 +∞ x 1 − x ∈ ℝ
74 iffalse ⊢ ¬ x = 1 → if x = 1 +∞ x 1 − x = x 1 − x
75 74 adantl ⊢ x ∈ 0 1 ∧ ¬ x = 1 → if x = 1 +∞ x 1 − x = x 1 − x
76 rge0ssre ⊢ 0 +∞ ⊆ ℝ
77 76 30 sseldi ⊢ x ∈ 0 1 ∧ ¬ x = 1 → x 1 − x ∈ ℝ
78 75 77 eqeltrd ⊢ x ∈ 0 1 ∧ ¬ x = 1 → if x = 1 +∞ x 1 − x ∈ ℝ
79 78 ex ⊢ x ∈ 0 1 → ¬ x = 1 → if x = 1 +∞ x 1 − x ∈ ℝ
80 79 ad2antrr ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ y = +∞ → ¬ x = 1 → if x = 1 +∞ x 1 − x ∈ ℝ
81 80 con1d ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ y = +∞ → ¬ if x = 1 +∞ x 1 − x ∈ ℝ → x = 1
82 73 81 syl5bi ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ y = +∞ → if x = 1 +∞ x 1 − x ∉ ℝ → x = 1
83 72 82 syld ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ y = +∞ → y = if x = 1 +∞ x 1 − x → x = 1
84 66 83 impbid ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ y = +∞ → x = 1 ↔ y = if x = 1 +∞ x 1 − x
85 eqeq2 ⊢ +∞ = if x = 1 +∞ x 1 − x → y = +∞ ↔ y = if x = 1 +∞ x 1 − x
86 85 bibi2d ⊢ +∞ = if x = 1 +∞ x 1 − x → x = y 1 + y ↔ y = +∞ ↔ x = y 1 + y ↔ y = if x = 1 +∞ x 1 − x
87 eqeq2 ⊢ x 1 − x = if x = 1 +∞ x 1 − x → y = x 1 − x ↔ y = if x = 1 +∞ x 1 − x
88 87 bibi2d ⊢ x 1 − x = if x = 1 +∞ x 1 − x → x = y 1 + y ↔ y = x 1 − x ↔ x = y 1 + y ↔ y = if x = 1 +∞ x 1 − x
89 0re ⊢ 0 ∈ ℝ
90 elico2 ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ * → y 1 + y ∈ 0 1 ↔ y 1 + y ∈ ℝ ∧ 0 ≤ y 1 + y ∧ y 1 + y < 1
91 89 9 90 mp2an ⊢ y 1 + y ∈ 0 1 ↔ y 1 + y ∈ ℝ ∧ 0 ≤ y 1 + y ∧ y 1 + y < 1
92 55 91 sylib ⊢ y ∈ 0 +∞ ∧ ¬ y = +∞ → y 1 + y ∈ ℝ ∧ 0 ≤ y 1 + y ∧ y 1 + y < 1
93 92 simp1d ⊢ y ∈ 0 +∞ ∧ ¬ y = +∞ → y 1 + y ∈ ℝ
94 92 simp3d ⊢ y ∈ 0 +∞ ∧ ¬ y = +∞ → y 1 + y < 1
95 93 94 gtned ⊢ y ∈ 0 +∞ ∧ ¬ y = +∞ → 1 ≠ y 1 + y
96 95 adantll ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ ¬ y = +∞ → 1 ≠ y 1 + y
97 96 neneqd ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ ¬ y = +∞ → ¬ 1 = y 1 + y
98 eqeq1 ⊢ x = 1 → x = y 1 + y ↔ 1 = y 1 + y
99 98 notbid ⊢ x = 1 → ¬ x = y 1 + y ↔ ¬ 1 = y 1 + y
100 97 99 syl5ibrcom ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ ¬ y = +∞ → x = 1 → ¬ x = y 1 + y
101 100 imp ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ ¬ y = +∞ ∧ x = 1 → ¬ x = y 1 + y
102 simplr ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ ¬ y = +∞ ∧ x = 1 → ¬ y = +∞
103 101 102 2falsed ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ ¬ y = +∞ ∧ x = 1 → x = y 1 + y ↔ y = +∞
104 f1ocnvfvb ⊢ x ∈ 0 1 ⟼ x 1 − x : 0 1 ⟶ 1-1 onto 0 +∞ ∧ x ∈ 0 1 ∧ y ∈ 0 +∞ → x ∈ 0 1 ⟼ x 1 − x ⁡ x = y ↔ x ∈ 0 1 ⟼ x 1 − x -1 ⁡ y = x
105 24 104 mp3an1 ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ → x ∈ 0 1 ⟼ x 1 − x ⁡ x = y ↔ x ∈ 0 1 ⟼ x 1 − x -1 ⁡ y = x
106 simpl ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ → x ∈ 0 1
107 ovex ⊢ x 1 − x ∈ V
108 22 fvmpt2 ⊢ x ∈ 0 1 ∧ x 1 − x ∈ V → x ∈ 0 1 ⟼ x 1 − x ⁡ x = x 1 − x
109 106 107 108 sylancl ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ → x ∈ 0 1 ⟼ x 1 − x ⁡ x = x 1 − x
110 109 eqeq1d ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ → x ∈ 0 1 ⟼ x 1 − x ⁡ x = y ↔ x 1 − x = y
111 simpr ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ → y ∈ 0 +∞
112 ovex ⊢ y 1 + y ∈ V
113 51 fvmpt2 ⊢ y ∈ 0 +∞ ∧ y 1 + y ∈ V → x ∈ 0 1 ⟼ x 1 − x -1 ⁡ y = y 1 + y
114 111 112 113 sylancl ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ → x ∈ 0 1 ⟼ x 1 − x -1 ⁡ y = y 1 + y
115 114 eqeq1d ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ → x ∈ 0 1 ⟼ x 1 − x -1 ⁡ y = x ↔ y 1 + y = x
116 105 110 115 3bitr3rd ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ → y 1 + y = x ↔ x 1 − x = y
117 eqcom ⊢ x = y 1 + y ↔ y 1 + y = x
118 eqcom ⊢ y = x 1 − x ↔ x 1 − x = y
119 116 117 118 3bitr4g ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ → x = y 1 + y ↔ y = x 1 − x
120 21 47 119 syl2an ⊢ x ∈ 0 1 ∧ ¬ x = 1 ∧ y ∈ 0 +∞ ∧ ¬ y = +∞ → x = y 1 + y ↔ y = x 1 − x
121 120 an4s ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ ¬ x = 1 ∧ ¬ y = +∞ → x = y 1 + y ↔ y = x 1 − x
122 121 anass1rs ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ ¬ y = +∞ ∧ ¬ x = 1 → x = y 1 + y ↔ y = x 1 − x
123 86 88 103 122 ifbothda ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ ∧ ¬ y = +∞ → x = y 1 + y ↔ y = if x = 1 +∞ x 1 − x
124 60 62 84 123 ifbothda ⊢ x ∈ 0 1 ∧ y ∈ 0 +∞ → x = if y = +∞ 1 y 1 + y ↔ y = if x = 1 +∞ x 1 − x
125 124 adantl ⊢ ⊤ ∧ x ∈ 0 1 ∧ y ∈ 0 +∞ → x = if y = +∞ 1 y 1 + y ↔ y = if x = 1 +∞ x 1 − x
126 1 33 58 125 f1ocnv2d ⊢ ⊤ → F : 0 1 ⟶ 1-1 onto 0 +∞ ∧ F -1 = y ∈ 0 +∞ ⟼ if y = +∞ 1 y 1 + y
127 126 mptru ⊢ F : 0 1 ⟶ 1-1 onto 0 +∞ ∧ F -1 = y ∈ 0 +∞ ⟼ if y = +∞ 1 y 1 + y