Proof of Theorem hspval
Step | Hyp | Ref
| Expression |
1 | | hspval.h |
. . 3
⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑖 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑥 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ))) |
2 | | id 22 |
. . . 4
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
3 | | eqidd 2739 |
. . . 4
⊢ (𝑥 = 𝑋 → ℝ = ℝ) |
4 | | ixpeq1 8654 |
. . . 4
⊢ (𝑥 = 𝑋 → X𝑘 ∈ 𝑥 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ)) |
5 | 2, 3, 4 | mpoeq123dv 7328 |
. . 3
⊢ (𝑥 = 𝑋 → (𝑖 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑥 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ)) = (𝑖 ∈ 𝑋, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ))) |
6 | | hspval.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
7 | | reex 10893 |
. . . . 5
⊢ ℝ
∈ V |
8 | 7 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ∈
V) |
9 | | eqid 2738 |
. . . . 5
⊢ (𝑖 ∈ 𝑋, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ)) = (𝑖 ∈ 𝑋, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ)) |
10 | 9 | mpoexg 7890 |
. . . 4
⊢ ((𝑋 ∈ Fin ∧ ℝ ∈
V) → (𝑖 ∈ 𝑋, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ)) ∈ V) |
11 | 6, 8, 10 | syl2anc 583 |
. . 3
⊢ (𝜑 → (𝑖 ∈ 𝑋, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ)) ∈ V) |
12 | 1, 5, 6, 11 | fvmptd3 6880 |
. 2
⊢ (𝜑 → (𝐻‘𝑋) = (𝑖 ∈ 𝑋, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ))) |
13 | | simpl 482 |
. . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑦 = 𝑌) → 𝑖 = 𝐼) |
14 | 13 | eqeq2d 2749 |
. . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑦 = 𝑌) → (𝑘 = 𝑖 ↔ 𝑘 = 𝐼)) |
15 | | simpr 484 |
. . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑦 = 𝑌) → 𝑦 = 𝑌) |
16 | 15 | oveq2d 7271 |
. . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑦 = 𝑌) → (-∞(,)𝑦) = (-∞(,)𝑌)) |
17 | 14, 16 | ifbieq1d 4480 |
. . . 4
⊢ ((𝑖 = 𝐼 ∧ 𝑦 = 𝑌) → if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ) = if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ)) |
18 | 17 | ixpeq2dv 8659 |
. . 3
⊢ ((𝑖 = 𝐼 ∧ 𝑦 = 𝑌) → X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ)) |
19 | 18 | adantl 481 |
. 2
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑦 = 𝑌)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ)) |
20 | | hspval.i |
. 2
⊢ (𝜑 → 𝐼 ∈ 𝑋) |
21 | | hspval.y |
. 2
⊢ (𝜑 → 𝑌 ∈ ℝ) |
22 | | ovex 7288 |
. . . . . 6
⊢
(-∞(,)𝑌)
∈ V |
23 | 22, 7 | ifcli 4503 |
. . . . 5
⊢ if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ) ∈ V |
24 | 23 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ) ∈ V) |
25 | 24 | ralrimiva 3107 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ 𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ) ∈ V) |
26 | | ixpexg 8668 |
. . 3
⊢
(∀𝑘 ∈
𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ) ∈ V → X𝑘 ∈
𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ) ∈ V) |
27 | 25, 26 | syl 17 |
. 2
⊢ (𝜑 → X𝑘 ∈
𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ) ∈ V) |
28 | 12, 19, 20, 21, 27 | ovmpod 7403 |
1
⊢ (𝜑 → (𝐼(𝐻‘𝑋)𝑌) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ)) |