Description: Obsolete theorem. 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.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | relrngo | ⊢ Rel RingOps |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-rngo | ⊢ RingOps = { ⟨ 𝑔 , ℎ ⟩ ∣ ( ( 𝑔 ∈ AbelOp ∧ ℎ : ( ran 𝑔 × ran 𝑔 ) ⟶ ran 𝑔 ) ∧ ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) ) ) } | |
| 2 | 1 | relopabiv | ⊢ Rel RingOps |