| Step | Hyp | Ref
| Expression |
| 1 | | phtpycc.3 |
. 2
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
| 2 | | phtpycc.5 |
. 2
⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐽)) |
| 3 | | phtpycc.1 |
. . 3
⊢ 𝑀 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), (𝑥𝐾(2 · 𝑦)), (𝑥𝐿((2 · 𝑦) − 1)))) |
| 4 | | iitopon 24905 |
. . . 4
⊢ II ∈
(TopOn‘(0[,]1)) |
| 5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → II ∈
(TopOn‘(0[,]1))) |
| 6 | | phtpycc.4 |
. . 3
⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) |
| 7 | 1, 6 | phtpyhtpy 25014 |
. . . 4
⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐺) ⊆ (𝐹(II Htpy 𝐽)𝐺)) |
| 8 | | phtpycc.6 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ (𝐹(PHtpy‘𝐽)𝐺)) |
| 9 | 7, 8 | sseldd 3984 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (𝐹(II Htpy 𝐽)𝐺)) |
| 10 | 6, 2 | phtpyhtpy 25014 |
. . . 4
⊢ (𝜑 → (𝐺(PHtpy‘𝐽)𝐻) ⊆ (𝐺(II Htpy 𝐽)𝐻)) |
| 11 | | phtpycc.7 |
. . . 4
⊢ (𝜑 → 𝐿 ∈ (𝐺(PHtpy‘𝐽)𝐻)) |
| 12 | 10, 11 | sseldd 3984 |
. . 3
⊢ (𝜑 → 𝐿 ∈ (𝐺(II Htpy 𝐽)𝐻)) |
| 13 | 3, 5, 1, 6, 2, 9, 12 | htpycc 25012 |
. 2
⊢ (𝜑 → 𝑀 ∈ (𝐹(II Htpy 𝐽)𝐻)) |
| 14 | | 0elunit 13509 |
. . . 4
⊢ 0 ∈
(0[,]1) |
| 15 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → 𝑠 ∈ (0[,]1)) |
| 16 | | simpr 484 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑦 = 𝑠) |
| 17 | 16 | breq1d 5153 |
. . . . . 6
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (𝑦 ≤ (1 / 2) ↔ 𝑠 ≤ (1 / 2))) |
| 18 | | simpl 482 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → 𝑥 = 0) |
| 19 | 16 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (2 · 𝑦) = (2 · 𝑠)) |
| 20 | 18, 19 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (𝑥𝐾(2 · 𝑦)) = (0𝐾(2 · 𝑠))) |
| 21 | 19 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → ((2 · 𝑦) − 1) = ((2 · 𝑠) − 1)) |
| 22 | 18, 21 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → (𝑥𝐿((2 · 𝑦) − 1)) = (0𝐿((2 · 𝑠) − 1))) |
| 23 | 17, 20, 22 | ifbieq12d 4554 |
. . . . 5
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑠) → if(𝑦 ≤ (1 / 2), (𝑥𝐾(2 · 𝑦)), (𝑥𝐿((2 · 𝑦) − 1))) = if(𝑠 ≤ (1 / 2), (0𝐾(2 · 𝑠)), (0𝐿((2 · 𝑠) − 1)))) |
| 24 | | ovex 7464 |
. . . . . 6
⊢ (0𝐾(2 · 𝑠)) ∈ V |
| 25 | | ovex 7464 |
. . . . . 6
⊢ (0𝐿((2 · 𝑠) − 1)) ∈ V |
| 26 | 24, 25 | ifex 4576 |
. . . . 5
⊢ if(𝑠 ≤ (1 / 2), (0𝐾(2 · 𝑠)), (0𝐿((2 · 𝑠) − 1))) ∈ V |
| 27 | 23, 3, 26 | ovmpoa 7588 |
. . . 4
⊢ ((0
∈ (0[,]1) ∧ 𝑠
∈ (0[,]1)) → (0𝑀𝑠) = if(𝑠 ≤ (1 / 2), (0𝐾(2 · 𝑠)), (0𝐿((2 · 𝑠) − 1)))) |
| 28 | 14, 15, 27 | sylancr 587 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝑀𝑠) = if(𝑠 ≤ (1 / 2), (0𝐾(2 · 𝑠)), (0𝐿((2 · 𝑠) − 1)))) |
| 29 | | simpll 767 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → 𝜑) |
| 30 | | elii1 24964 |
. . . . . . . 8
⊢ (𝑠 ∈ (0[,](1 / 2)) ↔
(𝑠 ∈ (0[,]1) ∧
𝑠 ≤ (1 /
2))) |
| 31 | | iihalf1 24958 |
. . . . . . . 8
⊢ (𝑠 ∈ (0[,](1 / 2)) → (2
· 𝑠) ∈
(0[,]1)) |
| 32 | 30, 31 | sylbir 235 |
. . . . . . 7
⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≤ (1 / 2)) → (2
· 𝑠) ∈
(0[,]1)) |
| 33 | 32 | adantll 714 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → (2 · 𝑠) ∈
(0[,]1)) |
| 34 | 1, 6, 8 | phtpyi 25016 |
. . . . . 6
⊢ ((𝜑 ∧ (2 · 𝑠) ∈ (0[,]1)) →
((0𝐾(2 · 𝑠)) = (𝐹‘0) ∧ (1𝐾(2 · 𝑠)) = (𝐹‘1))) |
| 35 | 29, 33, 34 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → ((0𝐾(2 · 𝑠)) = (𝐹‘0) ∧ (1𝐾(2 · 𝑠)) = (𝐹‘1))) |
| 36 | 35 | simpld 494 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → (0𝐾(2 · 𝑠)) = (𝐹‘0)) |
| 37 | | simpll 767 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → 𝜑) |
| 38 | | elii2 24965 |
. . . . . . . . 9
⊢ ((𝑠 ∈ (0[,]1) ∧ ¬
𝑠 ≤ (1 / 2)) →
𝑠 ∈ ((1 /
2)[,]1)) |
| 39 | | iihalf2 24961 |
. . . . . . . . 9
⊢ (𝑠 ∈ ((1 / 2)[,]1) → ((2
· 𝑠) − 1)
∈ (0[,]1)) |
| 40 | 38, 39 | syl 17 |
. . . . . . . 8
⊢ ((𝑠 ∈ (0[,]1) ∧ ¬
𝑠 ≤ (1 / 2)) → ((2
· 𝑠) − 1)
∈ (0[,]1)) |
| 41 | 40 | adantll 714 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → ((2
· 𝑠) − 1)
∈ (0[,]1)) |
| 42 | 6, 2, 11 | phtpyi 25016 |
. . . . . . 7
⊢ ((𝜑 ∧ ((2 · 𝑠) − 1) ∈ (0[,]1))
→ ((0𝐿((2 ·
𝑠) − 1)) = (𝐺‘0) ∧ (1𝐿((2 · 𝑠) − 1)) = (𝐺‘1))) |
| 43 | 37, 41, 42 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → ((0𝐿((2 · 𝑠) − 1)) = (𝐺‘0) ∧ (1𝐿((2 · 𝑠) − 1)) = (𝐺‘1))) |
| 44 | 43 | simpld 494 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → (0𝐿((2 · 𝑠) − 1)) = (𝐺‘0)) |
| 45 | 1, 6, 8 | phtpy01 25017 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘0) = (𝐺‘0) ∧ (𝐹‘1) = (𝐺‘1))) |
| 46 | 45 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → ((𝐹‘0) = (𝐺‘0) ∧ (𝐹‘1) = (𝐺‘1))) |
| 47 | 46 | simpld 494 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → (𝐹‘0) = (𝐺‘0)) |
| 48 | 44, 47 | eqtr4d 2780 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → (0𝐿((2 · 𝑠) − 1)) = (𝐹‘0)) |
| 49 | 36, 48 | ifeqda 4562 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → if(𝑠 ≤ (1 / 2), (0𝐾(2 · 𝑠)), (0𝐿((2 · 𝑠) − 1))) = (𝐹‘0)) |
| 50 | 28, 49 | eqtrd 2777 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝑀𝑠) = (𝐹‘0)) |
| 51 | | 1elunit 13510 |
. . . 4
⊢ 1 ∈
(0[,]1) |
| 52 | | simpr 484 |
. . . . . . 7
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → 𝑦 = 𝑠) |
| 53 | 52 | breq1d 5153 |
. . . . . 6
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (𝑦 ≤ (1 / 2) ↔ 𝑠 ≤ (1 / 2))) |
| 54 | | simpl 482 |
. . . . . . 7
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → 𝑥 = 1) |
| 55 | 52 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (2 · 𝑦) = (2 · 𝑠)) |
| 56 | 54, 55 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (𝑥𝐾(2 · 𝑦)) = (1𝐾(2 · 𝑠))) |
| 57 | 55 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → ((2 · 𝑦) − 1) = ((2 · 𝑠) − 1)) |
| 58 | 54, 57 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → (𝑥𝐿((2 · 𝑦) − 1)) = (1𝐿((2 · 𝑠) − 1))) |
| 59 | 53, 56, 58 | ifbieq12d 4554 |
. . . . 5
⊢ ((𝑥 = 1 ∧ 𝑦 = 𝑠) → if(𝑦 ≤ (1 / 2), (𝑥𝐾(2 · 𝑦)), (𝑥𝐿((2 · 𝑦) − 1))) = if(𝑠 ≤ (1 / 2), (1𝐾(2 · 𝑠)), (1𝐿((2 · 𝑠) − 1)))) |
| 60 | | ovex 7464 |
. . . . . 6
⊢ (1𝐾(2 · 𝑠)) ∈ V |
| 61 | | ovex 7464 |
. . . . . 6
⊢ (1𝐿((2 · 𝑠) − 1)) ∈ V |
| 62 | 60, 61 | ifex 4576 |
. . . . 5
⊢ if(𝑠 ≤ (1 / 2), (1𝐾(2 · 𝑠)), (1𝐿((2 · 𝑠) − 1))) ∈ V |
| 63 | 59, 3, 62 | ovmpoa 7588 |
. . . 4
⊢ ((1
∈ (0[,]1) ∧ 𝑠
∈ (0[,]1)) → (1𝑀𝑠) = if(𝑠 ≤ (1 / 2), (1𝐾(2 · 𝑠)), (1𝐿((2 · 𝑠) − 1)))) |
| 64 | 51, 15, 63 | sylancr 587 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝑀𝑠) = if(𝑠 ≤ (1 / 2), (1𝐾(2 · 𝑠)), (1𝐿((2 · 𝑠) − 1)))) |
| 65 | 35 | simprd 495 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≤ (1 / 2)) → (1𝐾(2 · 𝑠)) = (𝐹‘1)) |
| 66 | 43 | simprd 495 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → (1𝐿((2 · 𝑠) − 1)) = (𝐺‘1)) |
| 67 | 46 | simprd 495 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → (𝐹‘1) = (𝐺‘1)) |
| 68 | 66, 67 | eqtr4d 2780 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ (0[,]1)) ∧ ¬ 𝑠 ≤ (1 / 2)) → (1𝐿((2 · 𝑠) − 1)) = (𝐹‘1)) |
| 69 | 65, 68 | ifeqda 4562 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → if(𝑠 ≤ (1 / 2), (1𝐾(2 · 𝑠)), (1𝐿((2 · 𝑠) − 1))) = (𝐹‘1)) |
| 70 | 64, 69 | eqtrd 2777 |
. 2
⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝑀𝑠) = (𝐹‘1)) |
| 71 | 1, 2, 13, 50, 70 | isphtpyd 25018 |
1
⊢ (𝜑 → 𝑀 ∈ (𝐹(PHtpy‘𝐽)𝐻)) |