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 ) ) |
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 ) ) |