| Step |
Hyp |
Ref |
Expression |
| 1 |
|
funcestrcsetc.e |
⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 ) |
| 2 |
|
funcestrcsetc.s |
⊢ 𝑆 = ( SetCat ‘ 𝑈 ) |
| 3 |
|
funcestrcsetc.b |
⊢ 𝐵 = ( Base ‘ 𝐸 ) |
| 4 |
|
funcestrcsetc.c |
⊢ 𝐶 = ( Base ‘ 𝑆 ) |
| 5 |
|
funcestrcsetc.u |
⊢ ( 𝜑 → 𝑈 ∈ WUni ) |
| 6 |
|
funcestrcsetc.f |
⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) ) |
| 7 |
|
funcestrcsetc.g |
⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) ) |
| 8 |
|
funcestrcsetc.m |
⊢ 𝑀 = ( Base ‘ 𝑋 ) |
| 9 |
|
funcestrcsetc.n |
⊢ 𝑁 = ( Base ‘ 𝑌 ) |
| 10 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) ) |
| 11 |
|
fveq2 |
⊢ ( 𝑦 = 𝑌 → ( Base ‘ 𝑦 ) = ( Base ‘ 𝑌 ) ) |
| 12 |
|
fveq2 |
⊢ ( 𝑥 = 𝑋 → ( Base ‘ 𝑥 ) = ( Base ‘ 𝑋 ) ) |
| 13 |
11 12
|
oveqan12rd |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) = ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) |
| 14 |
9 8
|
oveq12i |
⊢ ( 𝑁 ↑m 𝑀 ) = ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) |
| 15 |
13 14
|
eqtr4di |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) = ( 𝑁 ↑m 𝑀 ) ) |
| 16 |
15
|
reseq2d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) = ( I ↾ ( 𝑁 ↑m 𝑀 ) ) ) |
| 17 |
16
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) = ( I ↾ ( 𝑁 ↑m 𝑀 ) ) ) |
| 18 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 ) |
| 19 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 ) |
| 20 |
|
ovexd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑁 ↑m 𝑀 ) ∈ V ) |
| 21 |
20
|
resiexd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( I ↾ ( 𝑁 ↑m 𝑀 ) ) ∈ V ) |
| 22 |
10 17 18 19 21
|
ovmpod |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 𝐺 𝑌 ) = ( I ↾ ( 𝑁 ↑m 𝑀 ) ) ) |