Step |
Hyp |
Ref |
Expression |
1 |
|
hoissrrn.1 |
⊢ ( 𝜑 → 𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) ) |
2 |
|
fvex |
⊢ ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ∈ V |
3 |
2
|
rgenw |
⊢ ∀ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ∈ V |
4 |
|
ixpssmapg |
⊢ ( ∀ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ∈ V → X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ( ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ↑m 𝑋 ) ) |
5 |
3 4
|
ax-mp |
⊢ X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ( ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ↑m 𝑋 ) |
6 |
5
|
a1i |
⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ( ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ↑m 𝑋 ) ) |
7 |
|
reex |
⊢ ℝ ∈ V |
8 |
7
|
a1i |
⊢ ( 𝜑 → ℝ ∈ V ) |
9 |
1
|
hoissre |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ℝ ) |
10 |
9
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ℝ ) |
11 |
|
iunss |
⊢ ( ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ℝ ↔ ∀ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ℝ ) |
12 |
10 11
|
sylibr |
⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ℝ ) |
13 |
|
mapss |
⊢ ( ( ℝ ∈ V ∧ ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ℝ ) → ( ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ↑m 𝑋 ) ⊆ ( ℝ ↑m 𝑋 ) ) |
14 |
8 12 13
|
syl2anc |
⊢ ( 𝜑 → ( ∪ 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ↑m 𝑋 ) ⊆ ( ℝ ↑m 𝑋 ) ) |
15 |
6 14
|
sstrd |
⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) ⊆ ( ℝ ↑m 𝑋 ) ) |