MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iccpnfcnv Structured version   Visualization version   GIF version
Theorem iccpnfcnv 22743
Description: Define a bijection from [0, 1] to [0, +∞]. (Contributed by Mario Carneiro, 9-Sep-2015.)
Hypothesis
Ref Expression
iccpnfhmeo.f 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))
Assertion
Ref Expression
iccpnfcnv (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,]+∞) ↦ if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦)))))
Distinct variable groups:   𝑥,𝑦   𝑦,𝐹
Allowed substitution hint:   𝐹(𝑥)
Proof of Theorem iccpnfcnv
StepHypRef Expression
1 iccpnfhmeo.f . . 3 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))
2 0xr 10086 . . . . . . 7 0 ∈ ℝ*
3 pnfxr 10092 . . . . . . 7 +∞ ∈ ℝ*
4 0lepnf 11966 . . . . . . 7 0 ≤ +∞
5 ubicc2 12289 . . . . . . 7 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 ≤ +∞) → +∞ ∈ (0[,]+∞))
62, 3, 4, 5mp3an 1424 . . . . . 6 +∞ ∈ (0[,]+∞)
76a1i 11 . . . . 5 ((𝑥 ∈ (0[,]1) ∧ 𝑥 = 1) → +∞ ∈ (0[,]+∞))
8 icossicc 12260 . . . . . 6 (0[,)+∞) ⊆ (0[,]+∞)
9 1re 10039 . . . . . . . . . . . . . . 15 1 ∈ ℝ
109rexri 10097 . . . . . . . . . . . . . 14 1 ∈ ℝ*
11 0le1 10551 . . . . . . . . . . . . . 14 0 ≤ 1
12 snunico 12299 . . . . . . . . . . . . . 14 ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1) → ((0[,)1) ∪ {1}) = (0[,]1))
132, 10, 11, 12mp3an 1424 . . . . . . . . . . . . 13 ((0[,)1) ∪ {1}) = (0[,]1)
1413eleq2i 2693 . . . . . . . . . . . 12 (𝑥 ∈ ((0[,)1) ∪ {1}) ↔ 𝑥 ∈ (0[,]1))
15 elun 3753 . . . . . . . . . . . 12 (𝑥 ∈ ((0[,)1) ∪ {1}) ↔ (𝑥 ∈ (0[,)1) ∨ 𝑥 ∈ {1}))
1614, 15bitr3i 266 . . . . . . . . . . 11 (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ (0[,)1) ∨ 𝑥 ∈ {1}))
17 pm2.53 388 . . . . . . . . . . 11 ((𝑥 ∈ (0[,)1) ∨ 𝑥 ∈ {1}) → (¬ 𝑥 ∈ (0[,)1) → 𝑥 ∈ {1}))
1816, 17sylbi 207 . . . . . . . . . 10 (𝑥 ∈ (0[,]1) → (¬ 𝑥 ∈ (0[,)1) → 𝑥 ∈ {1}))
19 elsni 4194 . . . . . . . . . 10 (𝑥 ∈ {1} → 𝑥 = 1)
2018, 19syl6 35 . . . . . . . . 9 (𝑥 ∈ (0[,]1) → (¬ 𝑥 ∈ (0[,)1) → 𝑥 = 1))
2120con1d 139 . . . . . . . 8 (𝑥 ∈ (0[,]1) → (¬ 𝑥 = 1 → 𝑥 ∈ (0[,)1)))
2221imp 445 . . . . . . 7 ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 = 1) → 𝑥 ∈ (0[,)1))
23 eqid 2622 . . . . . . . . . . . 12 (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))) = (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))
2423icopnfcnv 22741 . . . . . . . . . . 11 ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))):(0[,)1)–1-1-onto→(0[,)+∞) ∧ ◡(𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))) = (𝑦 ∈ (0[,)+∞) ↦ (𝑦 / (1 + 𝑦))))
2524simpli 474 . . . . . . . . . 10 (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))):(0[,)1)–1-1-onto→(0[,)+∞)
26 f1of 6137 . . . . . . . . . 10 ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))):(0[,)1)–1-1-onto→(0[,)+∞) → (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))):(0[,)1)⟶(0[,)+∞))
2725, 26ax-mp 5 . . . . . . . . 9 (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))):(0[,)1)⟶(0[,)+∞)
2823fmpt 6381 . . . . . . . . 9 (∀𝑥 ∈ (0[,)1)(𝑥 / (1 − 𝑥)) ∈ (0[,)+∞) ↔ (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))):(0[,)1)⟶(0[,)+∞))
2927, 28mpbir 221 . . . . . . . 8 ∀𝑥 ∈ (0[,)1)(𝑥 / (1 − 𝑥)) ∈ (0[,)+∞)
3029rspec 2931 . . . . . . 7 (𝑥 ∈ (0[,)1) → (𝑥 / (1 − 𝑥)) ∈ (0[,)+∞))
3122, 30syl 17 . . . . . 6 ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 = 1) → (𝑥 / (1 − 𝑥)) ∈ (0[,)+∞))
328, 31sseldi 3601 . . . . 5 ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 = 1) → (𝑥 / (1 − 𝑥)) ∈ (0[,]+∞))
337, 32ifclda 4120 . . . 4 (𝑥 ∈ (0[,]1) → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) ∈ (0[,]+∞))
3433adantl 482 . . 3 ((⊤ ∧ 𝑥 ∈ (0[,]1)) → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) ∈ (0[,]+∞))
35 1elunit 12291 . . . . . 6 1 ∈ (0[,]1)
3635a1i 11 . . . . 5 ((𝑦 ∈ (0[,]+∞) ∧ 𝑦 = +∞) → 1 ∈ (0[,]1))
37 icossicc 12260 . . . . . 6 (0[,)1) ⊆ (0[,]1)
38 snunico 12299 . . . . . . . . . . . . . 14 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 ≤ +∞) → ((0[,)+∞) ∪ {+∞}) = (0[,]+∞))
392, 3, 4, 38mp3an 1424 . . . . . . . . . . . . 13 ((0[,)+∞) ∪ {+∞}) = (0[,]+∞)
4039eleq2i 2693 . . . . . . . . . . . 12 (𝑦 ∈ ((0[,)+∞) ∪ {+∞}) ↔ 𝑦 ∈ (0[,]+∞))
41 elun 3753 . . . . . . . . . . . 12 (𝑦 ∈ ((0[,)+∞) ∪ {+∞}) ↔ (𝑦 ∈ (0[,)+∞) ∨ 𝑦 ∈ {+∞}))
4240, 41bitr3i 266 . . . . . . . . . . 11 (𝑦 ∈ (0[,]+∞) ↔ (𝑦 ∈ (0[,)+∞) ∨ 𝑦 ∈ {+∞}))
43 pm2.53 388 . . . . . . . . . . 11 ((𝑦 ∈ (0[,)+∞) ∨ 𝑦 ∈ {+∞}) → (¬ 𝑦 ∈ (0[,)+∞) → 𝑦 ∈ {+∞}))
4442, 43sylbi 207 . . . . . . . . . 10 (𝑦 ∈ (0[,]+∞) → (¬ 𝑦 ∈ (0[,)+∞) → 𝑦 ∈ {+∞}))
45 elsni 4194 . . . . . . . . . 10 (𝑦 ∈ {+∞} → 𝑦 = +∞)
4644, 45syl6 35 . . . . . . . . 9 (𝑦 ∈ (0[,]+∞) → (¬ 𝑦 ∈ (0[,)+∞) → 𝑦 = +∞))
4746con1d 139 . . . . . . . 8 (𝑦 ∈ (0[,]+∞) → (¬ 𝑦 = +∞ → 𝑦 ∈ (0[,)+∞)))
4847imp 445 . . . . . . 7 ((𝑦 ∈ (0[,]+∞) ∧ ¬ 𝑦 = +∞) → 𝑦 ∈ (0[,)+∞))
49 f1ocnv 6149 . . . . . . . . . 10 ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))):(0[,)1)–1-1-onto→(0[,)+∞) → ◡(𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))):(0[,)+∞)–1-1-onto→(0[,)1))
50 f1of 6137 . . . . . . . . . 10 (◡(𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))):(0[,)+∞)–1-1-onto→(0[,)1) → ◡(𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))):(0[,)+∞)⟶(0[,)1))
5125, 49, 50mp2b 10 . . . . . . . . 9 ◡(𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))):(0[,)+∞)⟶(0[,)1)
5224simpri 478 . . . . . . . . . 10 ◡(𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))) = (𝑦 ∈ (0[,)+∞) ↦ (𝑦 / (1 + 𝑦)))
5352fmpt 6381 . . . . . . . . 9 (∀𝑦 ∈ (0[,)+∞)(𝑦 / (1 + 𝑦)) ∈ (0[,)1) ↔ ◡(𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))):(0[,)+∞)⟶(0[,)1))
5451, 53mpbir 221 . . . . . . . 8 ∀𝑦 ∈ (0[,)+∞)(𝑦 / (1 + 𝑦)) ∈ (0[,)1)
5554rspec 2931 . . . . . . 7 (𝑦 ∈ (0[,)+∞) → (𝑦 / (1 + 𝑦)) ∈ (0[,)1))
5648, 55syl 17 . . . . . 6 ((𝑦 ∈ (0[,]+∞) ∧ ¬ 𝑦 = +∞) → (𝑦 / (1 + 𝑦)) ∈ (0[,)1))
5737, 56sseldi 3601 . . . . 5 ((𝑦 ∈ (0[,]+∞) ∧ ¬ 𝑦 = +∞) → (𝑦 / (1 + 𝑦)) ∈ (0[,]1))
5836, 57ifclda 4120 . . . 4 (𝑦 ∈ (0[,]+∞) → if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦))) ∈ (0[,]1))
5958adantl 482 . . 3 ((⊤ ∧ 𝑦 ∈ (0[,]+∞)) → if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦))) ∈ (0[,]1))
60 eqeq2 2633 . . . . . 6 (1 = if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦))) → (𝑥 = 1 ↔ 𝑥 = if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦)))))
6160bibi1d 333 . . . . 5 (1 = if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦))) → ((𝑥 = 1 ↔ 𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥)))) ↔ (𝑥 = if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦))) ↔ 𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))))
62 eqeq2 2633 . . . . . 6 ((𝑦 / (1 + 𝑦)) = if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦))) → (𝑥 = (𝑦 / (1 + 𝑦)) ↔ 𝑥 = if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦)))))
6362bibi1d 333 . . . . 5 ((𝑦 / (1 + 𝑦)) = if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦))) → ((𝑥 = (𝑦 / (1 + 𝑦)) ↔ 𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥)))) ↔ (𝑥 = if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦))) ↔ 𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))))
64 simpr 477 . . . . . . 7 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 𝑦 = +∞) → 𝑦 = +∞)
65 iftrue 4092 . . . . . . . 8 (𝑥 = 1 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) = +∞)
6665eqeq2d 2632 . . . . . . 7 (𝑥 = 1 → (𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) ↔ 𝑦 = +∞))
6764, 66syl5ibrcom 237 . . . . . 6 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 𝑦 = +∞) → (𝑥 = 1 → 𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥)))))
68 pnfnre 10081 . . . . . . . . 9 +∞ ∉ ℝ
69 neleq1 2902 . . . . . . . . . 10 (𝑦 = +∞ → (𝑦 ∉ ℝ ↔ +∞ ∉ ℝ))
7069adantl 482 . . . . . . . . 9 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 𝑦 = +∞) → (𝑦 ∉ ℝ ↔ +∞ ∉ ℝ))
7168, 70mpbiri 248 . . . . . . . 8 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 𝑦 = +∞) → 𝑦 ∉ ℝ)
72 neleq1 2902 . . . . . . . 8 (𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) → (𝑦 ∉ ℝ ↔ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) ∉ ℝ))
7371, 72syl5ibcom 235 . . . . . . 7 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 𝑦 = +∞) → (𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) ∉ ℝ))
74 df-nel 2898 . . . . . . . 8 (if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) ∉ ℝ ↔ ¬ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) ∈ ℝ)
75 iffalse 4095 . . . . . . . . . . . . 13 (¬ 𝑥 = 1 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) = (𝑥 / (1 − 𝑥)))
7675adantl 482 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 = 1) → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) = (𝑥 / (1 − 𝑥)))
77 rge0ssre 12280 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ ℝ
7877, 31sseldi 3601 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 = 1) → (𝑥 / (1 − 𝑥)) ∈ ℝ)
7976, 78eqeltrd 2701 . . . . . . . . . . 11 ((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 = 1) → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) ∈ ℝ)
8079ex 450 . . . . . . . . . 10 (𝑥 ∈ (0[,]1) → (¬ 𝑥 = 1 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) ∈ ℝ))
8180ad2antrr 762 . . . . . . . . 9 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 𝑦 = +∞) → (¬ 𝑥 = 1 → if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) ∈ ℝ))
8281con1d 139 . . . . . . . 8 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 𝑦 = +∞) → (¬ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) ∈ ℝ → 𝑥 = 1))
8374, 82syl5bi 232 . . . . . . 7 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 𝑦 = +∞) → (if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) ∉ ℝ → 𝑥 = 1))
8473, 83syld 47 . . . . . 6 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 𝑦 = +∞) → (𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) → 𝑥 = 1))
8567, 84impbid 202 . . . . 5 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ 𝑦 = +∞) → (𝑥 = 1 ↔ 𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥)))))
86 eqeq2 2633 . . . . . . 7 (+∞ = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) → (𝑦 = +∞ ↔ 𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥)))))
8786bibi2d 332 . . . . . 6 (+∞ = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) → ((𝑥 = (𝑦 / (1 + 𝑦)) ↔ 𝑦 = +∞) ↔ (𝑥 = (𝑦 / (1 + 𝑦)) ↔ 𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))))
88 eqeq2 2633 . . . . . . 7 ((𝑥 / (1 − 𝑥)) = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) → (𝑦 = (𝑥 / (1 − 𝑥)) ↔ 𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥)))))
8988bibi2d 332 . . . . . 6 ((𝑥 / (1 − 𝑥)) = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))) → ((𝑥 = (𝑦 / (1 + 𝑦)) ↔ 𝑦 = (𝑥 / (1 − 𝑥))) ↔ (𝑥 = (𝑦 / (1 + 𝑦)) ↔ 𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))))
90 0re 10040 . . . . . . . . . . . . . . 15 0 ∈ ℝ
91 elico2 12237 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ 1 ∈ ℝ*) → ((𝑦 / (1 + 𝑦)) ∈ (0[,)1) ↔ ((𝑦 / (1 + 𝑦)) ∈ ℝ ∧ 0 ≤ (𝑦 / (1 + 𝑦)) ∧ (𝑦 / (1 + 𝑦)) < 1)))
9290, 10, 91mp2an 708 . . . . . . . . . . . . . 14 ((𝑦 / (1 + 𝑦)) ∈ (0[,)1) ↔ ((𝑦 / (1 + 𝑦)) ∈ ℝ ∧ 0 ≤ (𝑦 / (1 + 𝑦)) ∧ (𝑦 / (1 + 𝑦)) < 1))
9356, 92sylib 208 . . . . . . . . . . . . 13 ((𝑦 ∈ (0[,]+∞) ∧ ¬ 𝑦 = +∞) → ((𝑦 / (1 + 𝑦)) ∈ ℝ ∧ 0 ≤ (𝑦 / (1 + 𝑦)) ∧ (𝑦 / (1 + 𝑦)) < 1))
9493simp1d 1073 . . . . . . . . . . . 12 ((𝑦 ∈ (0[,]+∞) ∧ ¬ 𝑦 = +∞) → (𝑦 / (1 + 𝑦)) ∈ ℝ)
9593simp3d 1075 . . . . . . . . . . . 12 ((𝑦 ∈ (0[,]+∞) ∧ ¬ 𝑦 = +∞) → (𝑦 / (1 + 𝑦)) < 1)
9694, 95gtned 10172 . . . . . . . . . . 11 ((𝑦 ∈ (0[,]+∞) ∧ ¬ 𝑦 = +∞) → 1 ≠ (𝑦 / (1 + 𝑦)))
9796adantll 750 . . . . . . . . . 10 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ ¬ 𝑦 = +∞) → 1 ≠ (𝑦 / (1 + 𝑦)))
9897neneqd 2799 . . . . . . . . 9 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ ¬ 𝑦 = +∞) → ¬ 1 = (𝑦 / (1 + 𝑦)))
99 eqeq1 2626 . . . . . . . . . 10 (𝑥 = 1 → (𝑥 = (𝑦 / (1 + 𝑦)) ↔ 1 = (𝑦 / (1 + 𝑦))))
10099notbid 308 . . . . . . . . 9 (𝑥 = 1 → (¬ 𝑥 = (𝑦 / (1 + 𝑦)) ↔ ¬ 1 = (𝑦 / (1 + 𝑦))))
10198, 100syl5ibrcom 237 . . . . . . . 8 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ ¬ 𝑦 = +∞) → (𝑥 = 1 → ¬ 𝑥 = (𝑦 / (1 + 𝑦))))
102101imp 445 . . . . . . 7 ((((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ ¬ 𝑦 = +∞) ∧ 𝑥 = 1) → ¬ 𝑥 = (𝑦 / (1 + 𝑦)))
103 simplr 792 . . . . . . 7 ((((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ ¬ 𝑦 = +∞) ∧ 𝑥 = 1) → ¬ 𝑦 = +∞)
104102, 1032falsed 366 . . . . . 6 ((((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ ¬ 𝑦 = +∞) ∧ 𝑥 = 1) → (𝑥 = (𝑦 / (1 + 𝑦)) ↔ 𝑦 = +∞))
105 f1ocnvfvb 6535 . . . . . . . . . . . 12 (((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))):(0[,)1)–1-1-onto→(0[,)+∞) ∧ 𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) → (((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑥) = 𝑦 ↔ (◡(𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑦) = 𝑥))
10625, 105mp3an1 1411 . . . . . . . . . . 11 ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) → (((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑥) = 𝑦 ↔ (◡(𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑦) = 𝑥))
107 simpl 473 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) → 𝑥 ∈ (0[,)1))
108 ovex 6678 . . . . . . . . . . . . 13 (𝑥 / (1 − 𝑥)) ∈ V
10923fvmpt2 6291 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,)1) ∧ (𝑥 / (1 − 𝑥)) ∈ V) → ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑥) = (𝑥 / (1 − 𝑥)))
110107, 108, 109sylancl 694 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) → ((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑥) = (𝑥 / (1 − 𝑥)))
111110eqeq1d 2624 . . . . . . . . . . 11 ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) → (((𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑥) = 𝑦 ↔ (𝑥 / (1 − 𝑥)) = 𝑦))
112 simpr 477 . . . . . . . . . . . . 13 ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) → 𝑦 ∈ (0[,)+∞))
113 ovex 6678 . . . . . . . . . . . . 13 (𝑦 / (1 + 𝑦)) ∈ V
11452fvmpt2 6291 . . . . . . . . . . . . 13 ((𝑦 ∈ (0[,)+∞) ∧ (𝑦 / (1 + 𝑦)) ∈ V) → (◡(𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑦) = (𝑦 / (1 + 𝑦)))
115112, 113, 114sylancl 694 . . . . . . . . . . . 12 ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) → (◡(𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑦) = (𝑦 / (1 + 𝑦)))
116115eqeq1d 2624 . . . . . . . . . . 11 ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) → ((◡(𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))‘𝑦) = 𝑥 ↔ (𝑦 / (1 + 𝑦)) = 𝑥))
117106, 111, 1163bitr3rd 299 . . . . . . . . . 10 ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) → ((𝑦 / (1 + 𝑦)) = 𝑥 ↔ (𝑥 / (1 − 𝑥)) = 𝑦))
118 eqcom 2629 . . . . . . . . . 10 (𝑥 = (𝑦 / (1 + 𝑦)) ↔ (𝑦 / (1 + 𝑦)) = 𝑥)
119 eqcom 2629 . . . . . . . . . 10 (𝑦 = (𝑥 / (1 − 𝑥)) ↔ (𝑥 / (1 − 𝑥)) = 𝑦)
120117, 118, 1193bitr4g 303 . . . . . . . . 9 ((𝑥 ∈ (0[,)1) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 = (𝑦 / (1 + 𝑦)) ↔ 𝑦 = (𝑥 / (1 − 𝑥))))
12122, 48, 120syl2an 494 . . . . . . . 8 (((𝑥 ∈ (0[,]1) ∧ ¬ 𝑥 = 1) ∧ (𝑦 ∈ (0[,]+∞) ∧ ¬ 𝑦 = +∞)) → (𝑥 = (𝑦 / (1 + 𝑦)) ↔ 𝑦 = (𝑥 / (1 − 𝑥))))
122121an4s 869 . . . . . . 7 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ (¬ 𝑥 = 1 ∧ ¬ 𝑦 = +∞)) → (𝑥 = (𝑦 / (1 + 𝑦)) ↔ 𝑦 = (𝑥 / (1 − 𝑥))))
123122anass1rs 849 . . . . . 6 ((((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ ¬ 𝑦 = +∞) ∧ ¬ 𝑥 = 1) → (𝑥 = (𝑦 / (1 + 𝑦)) ↔ 𝑦 = (𝑥 / (1 − 𝑥))))
12487, 89, 104, 123ifbothda 4123 . . . . 5 (((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) ∧ ¬ 𝑦 = +∞) → (𝑥 = (𝑦 / (1 + 𝑦)) ↔ 𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥)))))
12561, 63, 85, 124ifbothda 4123 . . . 4 ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞)) → (𝑥 = if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦))) ↔ 𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥)))))
126125adantl 482 . . 3 ((⊤ ∧ (𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]+∞))) → (𝑥 = if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦))) ↔ 𝑦 = if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥)))))
1271, 34, 59, 126f1ocnv2d 6886 . 2 (⊤ → (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,]+∞) ↦ if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦))))))
128127trud 1493 1 (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,]+∞) ↦ if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∧ w3a 1037   = wceq 1483  ⊤wtru 1484   ∈ wcel 1990   ≠ wne 2794   ∉ wnel 2897  ∀wral 2912  Vcvv 3200   ∪ cun 3572  ifcif 4086  {csn 4177   class class class wbr 4653   ↦ cmpt 4729  ◡ccnv 5113  ⟶wf 5884  –1-1-onto→wf1o 5887  ‘cfv 5888  (class class class)co 6650  ℝcr 9935  0cc0 9936  1c1 9937   + caddc 9939  +∞cpnf 10071  ℝ*cxr 10073   < clt 10074   ≤ cle 10075   − cmin 10266   / cdiv 10684  [,)cico 12177  [,]cicc 12178
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-rp 11833  df-ico 12181  df-icc 12182
This theorem is referenced by:  iccpnfhmeo  22744  xrhmeo  22745
  Copyright terms: Public domain W3C validator