Step |
Hyp |
Ref |
Expression |
1 |
|
relxpchom.t |
⊢ 𝑇 = ( 𝐶 ×c 𝐷 ) |
2 |
|
relxpchom.k |
⊢ 𝐾 = ( Hom ‘ 𝑇 ) |
3 |
|
xpss |
⊢ ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑣 ) ) ) ⊆ ( V × V ) |
4 |
3
|
rgen2w |
⊢ ∀ 𝑢 ∈ ( Base ‘ 𝑇 ) ∀ 𝑣 ∈ ( Base ‘ 𝑇 ) ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑣 ) ) ) ⊆ ( V × V ) |
5 |
|
eqid |
⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 ) |
6 |
|
eqid |
⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) |
7 |
|
eqid |
⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 ) |
8 |
1 5 6 7 2
|
xpchomfval |
⊢ 𝐾 = ( 𝑢 ∈ ( Base ‘ 𝑇 ) , 𝑣 ∈ ( Base ‘ 𝑇 ) ↦ ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑣 ) ) ) ) |
9 |
8
|
ovmptss |
⊢ ( ∀ 𝑢 ∈ ( Base ‘ 𝑇 ) ∀ 𝑣 ∈ ( Base ‘ 𝑇 ) ( ( ( 1st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑣 ) ) ) ⊆ ( V × V ) → ( 𝑋 𝐾 𝑌 ) ⊆ ( V × V ) ) |
10 |
4 9
|
ax-mp |
⊢ ( 𝑋 𝐾 𝑌 ) ⊆ ( V × V ) |
11 |
|
df-rel |
⊢ ( Rel ( 𝑋 𝐾 𝑌 ) ↔ ( 𝑋 𝐾 𝑌 ) ⊆ ( V × V ) ) |
12 |
10 11
|
mpbir |
⊢ Rel ( 𝑋 𝐾 𝑌 ) |