Step |
Hyp |
Ref |
Expression |
1 |
|
hoicoto2.i |
⊢ ( 𝜑 → 𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) ) |
2 |
|
hoicoto2.a |
⊢ 𝐴 = ( 𝑘 ∈ 𝑋 ↦ ( 1st ‘ ( 𝐼 ‘ 𝑘 ) ) ) |
3 |
|
hoicoto2.b |
⊢ 𝐵 = ( 𝑘 ∈ 𝑋 ↦ ( 2nd ‘ ( 𝐼 ‘ 𝑘 ) ) ) |
4 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) ) |
5 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 ) |
6 |
4 5
|
fvovco |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) = ( ( 1st ‘ ( 𝐼 ‘ 𝑘 ) ) [,) ( 2nd ‘ ( 𝐼 ‘ 𝑘 ) ) ) ) |
7 |
1
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐼 ‘ 𝑘 ) ∈ ( ℝ × ℝ ) ) |
8 |
|
xp1st |
⊢ ( ( 𝐼 ‘ 𝑘 ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ ℝ ) |
9 |
7 8
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ ℝ ) |
10 |
9
|
elexd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ V ) |
11 |
2
|
fvmpt2 |
⊢ ( ( 𝑘 ∈ 𝑋 ∧ ( 1st ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ V ) → ( 𝐴 ‘ 𝑘 ) = ( 1st ‘ ( 𝐼 ‘ 𝑘 ) ) ) |
12 |
5 10 11
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑘 ) = ( 1st ‘ ( 𝐼 ‘ 𝑘 ) ) ) |
13 |
12
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 1st ‘ ( 𝐼 ‘ 𝑘 ) ) = ( 𝐴 ‘ 𝑘 ) ) |
14 |
|
xp2nd |
⊢ ( ( 𝐼 ‘ 𝑘 ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ ℝ ) |
15 |
7 14
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ ℝ ) |
16 |
15
|
elexd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ V ) |
17 |
3
|
fvmpt2 |
⊢ ( ( 𝑘 ∈ 𝑋 ∧ ( 2nd ‘ ( 𝐼 ‘ 𝑘 ) ) ∈ V ) → ( 𝐵 ‘ 𝑘 ) = ( 2nd ‘ ( 𝐼 ‘ 𝑘 ) ) ) |
18 |
5 16 17
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑘 ) = ( 2nd ‘ ( 𝐼 ‘ 𝑘 ) ) ) |
19 |
18
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 2nd ‘ ( 𝐼 ‘ 𝑘 ) ) = ( 𝐵 ‘ 𝑘 ) ) |
20 |
13 19
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 1st ‘ ( 𝐼 ‘ 𝑘 ) ) [,) ( 2nd ‘ ( 𝐼 ‘ 𝑘 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) |
21 |
6 20
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) |
22 |
21
|
ixpeq2dva |
⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) |