Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . 4
⊢ (𝑗 = 𝐽 → (II Cn 𝑗) = (II Cn 𝐽)) |
2 | | eqidd 2623 |
. . . 4
⊢ (𝑗 = 𝐽 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) |
3 | 1, 1, 2 | mpt2eq123dv 6717 |
. . 3
⊢ (𝑗 = 𝐽 → (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))) |
4 | | df-pco 22805 |
. . 3
⊢
*𝑝 = (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))) |
5 | | ovex 6678 |
. . . 4
⊢ (II Cn
𝐽) ∈
V |
6 | 5, 5 | mpt2ex 7247 |
. . 3
⊢ (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) ∈ V |
7 | 3, 4, 6 | fvmpt 6282 |
. 2
⊢ (𝐽 ∈ Top →
(*𝑝‘𝐽) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))) |
8 | 4 | dmmptss 5631 |
. . . . . 6
⊢ dom
*𝑝 ⊆ Top |
9 | 8 | sseli 3599 |
. . . . 5
⊢ (𝐽 ∈ dom
*𝑝 → 𝐽 ∈ Top) |
10 | 9 | con3i 150 |
. . . 4
⊢ (¬
𝐽 ∈ Top → ¬
𝐽 ∈ dom
*𝑝) |
11 | | ndmfv 6218 |
. . . 4
⊢ (¬
𝐽 ∈ dom
*𝑝 → (*𝑝‘𝐽) = ∅) |
12 | 10, 11 | syl 17 |
. . 3
⊢ (¬
𝐽 ∈ Top →
(*𝑝‘𝐽) = ∅) |
13 | | cntop2 21045 |
. . . . . . 7
⊢ (𝑓 ∈ (II Cn 𝐽) → 𝐽 ∈ Top) |
14 | 13 | con3i 150 |
. . . . . 6
⊢ (¬
𝐽 ∈ Top → ¬
𝑓 ∈ (II Cn 𝐽)) |
15 | 14 | eq0rdv 3979 |
. . . . 5
⊢ (¬
𝐽 ∈ Top → (II Cn
𝐽) =
∅) |
16 | | mpt2eq12 6715 |
. . . . 5
⊢ (((II Cn
𝐽) = ∅ ∧ (II Cn
𝐽) = ∅) → (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) = (𝑓 ∈ ∅, 𝑔 ∈ ∅ ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))) |
17 | 15, 15, 16 | syl2anc 693 |
. . . 4
⊢ (¬
𝐽 ∈ Top → (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) = (𝑓 ∈ ∅, 𝑔 ∈ ∅ ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))) |
18 | | mpt20 6725 |
. . . 4
⊢ (𝑓 ∈ ∅, 𝑔 ∈ ∅ ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) = ∅ |
19 | 17, 18 | syl6eq 2672 |
. . 3
⊢ (¬
𝐽 ∈ Top → (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) = ∅) |
20 | 12, 19 | eqtr4d 2659 |
. 2
⊢ (¬
𝐽 ∈ Top →
(*𝑝‘𝐽) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))) |
21 | 7, 20 | pm2.61i 176 |
1
⊢
(*𝑝‘𝐽) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) |