This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (A \otimes B) = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cB	$class B$
2	0 1	ctxp	$class (A \otimes B)$
3		c1st	$class 1^{st}$
4		cvv	$class V$
5	4 4	cxp	$class (V \times V)$
6	3 5	cres	$class ({1^{st} ↾}_{(V \times V)})$
7	6	ccnv	$class {({1^{st} ↾}_{(V \times V)})}^{-1}$
8	7 0	ccom	$class ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A)$
9		c2nd	$class 2^{nd}$
10	9 5	cres	$class ({2^{nd} ↾}_{(V \times V)})$
11	10	ccnv	$class {({2^{nd} ↾}_{(V \times V)})}^{-1}$
12	11 1	ccom	$class ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B)$
13	8 12	cin	$class (({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B))$
14	2 13	wceq	$wff (A \otimes B) = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B)$