Theorem reldmxpc

Description: The binary product of categories is a proper operator, so it can be used with ovprc1 , elbasov , strov2rcl , and so on. See reldmxpcALT for an alternate proof with less "essential steps" but more "bytes". (Proposed by SN, 15-Oct-2025.) (Contributed by Zhi Wang, 15-Oct-2025)

	Ref	Expression
Assertion	reldmxpc	$$⊢\mathrm{Rel}\mathrm{dom}{\times }_c$$

Proof

Step	Hyp	Ref	Expression
1		relxp	$$⊢\mathrm{Rel}\left(\mathrm{V}\times \mathrm{V}\right)$$
2		fnxpc	$$⊢{\times }_{c}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$
3	2	fndmi	$$⊢\mathrm{dom}{\times }_c=\mathrm{V}\times \mathrm{V}$$
4	3	releqi	$$⊢\mathrm{Rel}\mathrm{dom}{\times }_c\leftrightarrow \mathrm{Rel}\left(\mathrm{V}\times \mathrm{V}\right)$$
5	1 4	mpbir	$$⊢\mathrm{Rel}\mathrm{dom}{\times }_c$$