Description: The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015) (Revised by Thierry Arnoux, 15-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | reldmprds | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-prds | |
|
2 | 1 | reldmmpo | |