This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
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 ) ) ∘ 𝐵 ) ) |