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
|- ( A |X. B ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 cB
 |-  B
2 0 1 cxrn
 |-  ( A |X. B )
3 c1st
 |-  1st
4 cvv
 |-  _V
5 4 4 cxp
 |-  ( _V X. _V )
6 3 5 cres
 |-  ( 1st |` ( _V X. _V ) )
7 6 ccnv
 |-  `' ( 1st |` ( _V X. _V ) )
8 7 0 ccom
 |-  ( `' ( 1st |` ( _V X. _V ) ) o. A )
9 c2nd
 |-  2nd
10 9 5 cres
 |-  ( 2nd |` ( _V X. _V ) )
11 10 ccnv
 |-  `' ( 2nd |` ( _V X. _V ) )
12 11 1 ccom
 |-  ( `' ( 2nd |` ( _V X. _V ) ) o. B )
13 8 12 cin
 |-  ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) )
14 2 13 wceq
 |-  ( A |X. B ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) )