Metamath Proof Explorer

Theorem relrngo

Description: The class of all unital rings is a relation. (Contributed by FL, 31-Aug-2009) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion relrngo 
|- Rel RingOps

Proof

Step Hyp Ref Expression
1 df-rngo 
 |-  RingOps = { <. g , h >. | ( ( g e. AbelOp /\ h : ( ran g X. ran g ) --> ran g ) /\ ( A. x e. ran g A. y e. ran g A. z e. ran g ( ( ( x h y ) h z ) = ( x h ( y h z ) ) /\ ( x h ( y g z ) ) = ( ( x h y ) g ( x h z ) ) /\ ( ( x g y ) h z ) = ( ( x h z ) g ( y h z ) ) ) /\ E. x e. ran g A. y e. ran g ( ( x h y ) = y /\ ( y h x ) = y ) ) ) }
2 1 relopabiv 
 |-  Rel RingOps