Definition df-txp 5737

Description: Define the tail cross product of two classes. Definition from [Holmes] p. 40. See brtxp 5784 for membership. (Contributed by SF, 9-Feb-2015.)

Assertion

Ref	Expression
df-txp	⊢ (A ⊗ B) = ((◡1st ∘ A) ∩ (◡2nd ∘ B))

Detailed syntax breakdown of Definition df-txp

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	ctxp 5736	. 2 class (A ⊗ B)
4		c1st 4718	. . . . 5 class 1st
5	4	ccnv 4772	. . . 4 class ◡1st
6	5, 1	ccom 4722	. . 3 class (◡1st ∘ A)
7		c2nd 4784	. . . . 5 class 2nd
8	7	ccnv 4772	. . . 4 class ◡2nd
9	8, 2	ccom 4722	. . 3 class (◡2nd ∘ B)
10	6, 9	cin 3209	. 2 class ((◡1st ∘ A) ∩ (◡2nd ∘ B))
11	3, 10	wceq 1642	1 wff (A ⊗ B) = ((◡1st ∘ A) ∩ (◡2nd ∘ B))

This definition is referenced by:  txpeq1  5780  txpeq2  5781  trtxp  5782  brtxp  5784  txpexg  5785  cnvpprod  5842