Definition df-xrn

Description: Define the range Cartesian product of two classes. Definition from Holmes p. 40. Membership in this class is characterized by xrnss3v and brxrn . This is Scott Fenton's df-txp with a different symbol, see https://github.com/metamath/set.mm/issues/2469 . (Contributed by Scott Fenton, 31-Mar-2012)

	Ref	Expression
Assertion	df-xrn	$$⊢A⋉B=\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ A\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ B\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	cxrn	$$classA⋉B$$
3		c1st	$$class{1}^{st}$$
4		cvv	$$class\mathrm{V}$$
5	4 4	cxp	$$class\left(\mathrm{V}\times \mathrm{V}\right)$$
6	3 5	cres	$$class\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
7	6	ccnv	$$class{\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}$$
8	7 0	ccom	$$class\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ A\right)$$
9		c2nd	$$class{2}^{nd}$$
10	9 5	cres	$$class\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
11	10	ccnv	$$class{\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}$$
12	11 1	ccom	$$class\left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ B\right)$$
13	8 12	cin	$$class\left(\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ A\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ B\right)\right)$$
14	2 13	wceq	$$wffA⋉B=\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ A\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ B\right)$$