This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: A range Cartesian product is a relation. This is Scott Fenton's txprel with a different symbol, see
https://github.com/metamath/set.mm/issues/2469 . (Contributed by Scott
Fenton, 31-Mar-2012)
|
|
Ref |
Expression |
|
Assertion |
xrnrel |
⊢ Rel ( 𝐴 ⋉ 𝐵 ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
xrnss3v |
⊢ ( 𝐴 ⋉ 𝐵 ) ⊆ ( V × ( V × V ) ) |
| 2 |
|
xpss |
⊢ ( V × ( V × V ) ) ⊆ ( V × V ) |
| 3 |
1 2
|
sstri |
⊢ ( 𝐴 ⋉ 𝐵 ) ⊆ ( V × V ) |
| 4 |
|
df-rel |
⊢ ( Rel ( 𝐴 ⋉ 𝐵 ) ↔ ( 𝐴 ⋉ 𝐵 ) ⊆ ( V × V ) ) |
| 5 |
3 4
|
mpbir |
⊢ Rel ( 𝐴 ⋉ 𝐵 ) |