Definition df-txp

Description: Define the tail cross of two classes. Membership in this class is defined by txpss3v and brtxp . (Contributed by Scott Fenton, 31-Mar-2012)

	Ref	Expression
Assertion	df-txp	$$⊢\left(A\otimes B\right)=\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	ctxp	$$class\left(A\otimes B\right)$$
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	$$wff\left(A\otimes B\right)=\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)$$