Proof of Theorem hspval
Step | Hyp | Ref
| Expression |
1 | | hspval.h |
. . . 4
⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑖 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑥 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ))) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐻 = (𝑥 ∈ Fin ↦ (𝑖 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑥 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ)))) |
3 | | id 22 |
. . . . 5
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
4 | | eqidd 2611 |
. . . . 5
⊢ (𝑥 = 𝑋 → ℝ = ℝ) |
5 | | ixpeq1 7805 |
. . . . 5
⊢ (𝑥 = 𝑋 → X𝑘 ∈ 𝑥 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ)) |
6 | 3, 4, 5 | mpt2eq123dv 6615 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝑖 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑥 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ)) = (𝑖 ∈ 𝑋, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ))) |
7 | 6 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑖 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑥 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ)) = (𝑖 ∈ 𝑋, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ))) |
8 | | hspval.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
9 | | reex 9906 |
. . . . 5
⊢ ℝ
∈ V |
10 | 9 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ∈
V) |
11 | | eqid 2610 |
. . . . 5
⊢ (𝑖 ∈ 𝑋, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ)) = (𝑖 ∈ 𝑋, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ)) |
12 | 11 | mpt2exg 7134 |
. . . 4
⊢ ((𝑋 ∈ Fin ∧ ℝ ∈
V) → (𝑖 ∈ 𝑋, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ)) ∈ V) |
13 | 8, 10, 12 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑖 ∈ 𝑋, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ)) ∈ V) |
14 | 2, 7, 8, 13 | fvmptd 6197 |
. 2
⊢ (𝜑 → (𝐻‘𝑋) = (𝑖 ∈ 𝑋, 𝑦 ∈ ℝ ↦ X𝑘 ∈
𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ))) |
15 | | simpl 472 |
. . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑦 = 𝑌) → 𝑖 = 𝐼) |
16 | 15 | eqeq2d 2620 |
. . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑦 = 𝑌) → (𝑘 = 𝑖 ↔ 𝑘 = 𝐼)) |
17 | | simpr 476 |
. . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑦 = 𝑌) → 𝑦 = 𝑌) |
18 | 17 | oveq2d 6565 |
. . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑦 = 𝑌) → (-∞(,)𝑦) = (-∞(,)𝑌)) |
19 | 16, 18 | ifbieq1d 4059 |
. . . 4
⊢ ((𝑖 = 𝐼 ∧ 𝑦 = 𝑌) → if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ) = if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ)) |
20 | 19 | ixpeq2dv 7810 |
. . 3
⊢ ((𝑖 = 𝐼 ∧ 𝑦 = 𝑌) → X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ)) |
21 | 20 | adantl 481 |
. 2
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑦 = 𝑌)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ)) |
22 | | hspval.i |
. 2
⊢ (𝜑 → 𝐼 ∈ 𝑋) |
23 | | hspval.y |
. 2
⊢ (𝜑 → 𝑌 ∈ ℝ) |
24 | | ovex 6577 |
. . . . . 6
⊢
(-∞(,)𝑌)
∈ V |
25 | 24, 9 | keepel 4105 |
. . . . 5
⊢ if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ) ∈ V |
26 | 25 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ) ∈ V) |
27 | 26 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ 𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ) ∈ V) |
28 | | ixpexg 7818 |
. . 3
⊢
(∀𝑘 ∈
𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ) ∈ V → X𝑘 ∈
𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ) ∈ V) |
29 | 27, 28 | syl 17 |
. 2
⊢ (𝜑 → X𝑘 ∈
𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ) ∈ V) |
30 | 14, 21, 22, 23, 29 | ovmpt2d 6686 |
1
⊢ (𝜑 → (𝐼(𝐻‘𝑋)𝑌) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ)) |