Step |
Hyp |
Ref |
Expression |
1 |
|
oprab2co.1 |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝑅 ) |
2 |
|
oprab2co.2 |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ 𝑆 ) |
3 |
|
oprab2co.3 |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 〈 𝐶 , 𝐷 〉 ) |
4 |
|
oprab2co.4 |
⊢ 𝐺 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐶 𝑀 𝐷 ) ) |
5 |
1 2
|
opelxpd |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 〈 𝐶 , 𝐷 〉 ∈ ( 𝑅 × 𝑆 ) ) |
6 |
|
df-ov |
⊢ ( 𝐶 𝑀 𝐷 ) = ( 𝑀 ‘ 〈 𝐶 , 𝐷 〉 ) |
7 |
6
|
a1i |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐶 𝑀 𝐷 ) = ( 𝑀 ‘ 〈 𝐶 , 𝐷 〉 ) ) |
8 |
7
|
mpoeq3ia |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐶 𝑀 𝐷 ) ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑀 ‘ 〈 𝐶 , 𝐷 〉 ) ) |
9 |
4 8
|
eqtri |
⊢ 𝐺 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝑀 ‘ 〈 𝐶 , 𝐷 〉 ) ) |
10 |
5 3 9
|
oprabco |
⊢ ( 𝑀 Fn ( 𝑅 × 𝑆 ) → 𝐺 = ( 𝑀 ∘ 𝐹 ) ) |