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	⊢ ( 𝐴 ⊗ 𝐵 ) = ( ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ 𝐴 ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ 𝐵 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	ctxp	⊢ ( 𝐴 ⊗ 𝐵 )
3		c1st	⊢ 1^st
4		cvv	⊢ V
5	4 4	cxp	⊢ ( V × V )
6	3 5	cres	⊢ ( 1^st ↾ ( V × V ) )
7	6	ccnv	⊢ ^◡ ( 1^st ↾ ( V × V ) )
8	7 0	ccom	⊢ ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ 𝐴 )
9		c2nd	⊢ 2^nd
10	9 5	cres	⊢ ( 2^nd ↾ ( V × V ) )
11	10	ccnv	⊢ ^◡ ( 2^nd ↾ ( V × V ) )
12	11 1	ccom	⊢ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ 𝐵 )
13	8 12	cin	⊢ ( ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ 𝐴 ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ 𝐵 ) )
14	2 13	wceq	⊢ ( 𝐴 ⊗ 𝐵 ) = ( ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ 𝐴 ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ 𝐵 ) )