Description: The domain of the ring isomorphism relation is a relation. (Contributed by AV, 24-Jul-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ricrel | ⊢ Rel ≃𝑟 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ric | ⊢ ≃𝑟 = ( ◡ RingIso “ ( V ∖ 1o ) ) | |
| 2 | cnvimass | ⊢ ( ◡ RingIso “ ( V ∖ 1o ) ) ⊆ dom RingIso | |
| 3 | rimfn | ⊢ RingIso Fn ( V × V ) | |
| 4 | 3 | fndmi | ⊢ dom RingIso = ( V × V ) |
| 5 | 2 4 | sseqtri | ⊢ ( ◡ RingIso “ ( V ∖ 1o ) ) ⊆ ( V × V ) |
| 6 | 1 5 | eqsstri | ⊢ ≃𝑟 ⊆ ( V × V ) |
| 7 | relxp | ⊢ Rel ( V × V ) | |
| 8 | relss | ⊢ ( ≃𝑟 ⊆ ( V × V ) → ( Rel ( V × V ) → Rel ≃𝑟 ) ) | |
| 9 | 6 7 8 | mp2 | ⊢ Rel ≃𝑟 |