Step |
Hyp |
Ref |
Expression |
1 |
|
oprabco.1 |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝐷 ) |
2 |
|
oprabco.2 |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) |
3 |
|
oprabco.3 |
⊢ 𝐺 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐻 ‘ 𝐶 ) ) |
4 |
1
|
adantl |
⊢ ( ( 𝐻 Fn 𝐷 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐷 ) |
5 |
2
|
a1i |
⊢ ( 𝐻 Fn 𝐷 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ) |
6 |
|
dffn5 |
⊢ ( 𝐻 Fn 𝐷 ↔ 𝐻 = ( 𝑧 ∈ 𝐷 ↦ ( 𝐻 ‘ 𝑧 ) ) ) |
7 |
6
|
biimpi |
⊢ ( 𝐻 Fn 𝐷 → 𝐻 = ( 𝑧 ∈ 𝐷 ↦ ( 𝐻 ‘ 𝑧 ) ) ) |
8 |
|
fveq2 |
⊢ ( 𝑧 = 𝐶 → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ 𝐶 ) ) |
9 |
4 5 7 8
|
fmpoco |
⊢ ( 𝐻 Fn 𝐷 → ( 𝐻 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐻 ‘ 𝐶 ) ) ) |
10 |
3 9
|
eqtr4id |
⊢ ( 𝐻 Fn 𝐷 → 𝐺 = ( 𝐻 ∘ 𝐹 ) ) |