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∈01⟼ifx=1+∞x1−x
Assertion iccpnfcnv ⊢F:01⟶1-1 onto0+∞∧F-1=y∈0+∞⟼ify=+∞1y1+y

Proof

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