Theorem reldmxpcALT

Description: Alternate proof of reldmxpc . (Contributed by Zhi Wang, 15-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-xpc	$$⊢{\times }_c=\left(r\in \mathrm{V},s\in \mathrm{V}⟼⦋\left({\mathrm{Base}}_r\times {\mathrm{Base}}_s\right)/b⦌⦋\left(u\in b,v\in b⟼\left(1^{st}\left(u\right)\mathrm{Hom}\left(r\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(s\right)2^{nd}\left(v\right)\right)\right)/h⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),h⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(x\in \left(b\times b\right),y\in b⟼\left(g\in \left(2^{nd}\left(x\right)hy\right),f\in h\left(x\right)⟼⟨1^{st}\left(g\right)\left(⟨1^{st}\left(1^{st}\left(x\right)\right),1^{st}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(r\right)1^{st}\left(y\right)\right)1^{st}\left(f\right),2^{nd}\left(g\right)\left(⟨2^{nd}\left(1^{st}\left(x\right)\right),2^{nd}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(s\right)2^{nd}\left(y\right)\right)2^{nd}\left(f\right)⟩\right)\right)⟩\right\}\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}{\times }_c$$