Metamath Proof Explorer


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

Detailed syntax breakdown

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