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 \in AbelOp \land h : ran g \times ran g ⟶ ran g) \land (\forall x \in ran g \forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \land \exists x \in ran g \forall y \in ran g (x h y = y \land y h x = y)))\}$
2	1	relopabiv	$⊢ Rel RingOps$

Metamath Proof Explorer

Theorem relrngo

Proof