Step |
Hyp |
Ref |
Expression |
1 |
|
estrchomfn.c |
⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 ) |
2 |
|
estrchomfn.u |
⊢ ( 𝜑 → 𝑈 ∈ 𝑉 ) |
3 |
|
estrchomfn.h |
⊢ 𝐻 = ( Hom ‘ 𝐶 ) |
4 |
|
eqid |
⊢ ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) |
5 |
|
ovex |
⊢ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ∈ V |
6 |
4 5
|
fnmpoi |
⊢ ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) Fn ( 𝑈 × 𝑈 ) |
7 |
1 2 3
|
estrchomfval |
⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) |
8 |
7
|
fneq1d |
⊢ ( 𝜑 → ( 𝐻 Fn ( 𝑈 × 𝑈 ) ↔ ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) Fn ( 𝑈 × 𝑈 ) ) ) |
9 |
6 8
|
mpbiri |
⊢ ( 𝜑 → 𝐻 Fn ( 𝑈 × 𝑈 ) ) |