Metamath Proof Explorer

Definition df-rngim

Description: Define the set of non-unital ring isomorphisms from r to s . (Contributed by AV, 20-Feb-2020)

Ref Expression
Assertion df-rngim ⊢ RngIso = r ∈ V , s ∈ V ⟼ f ∈ r RngHom s | f -1 ∈ s RngHom r

Detailed syntax breakdown

Step Hyp Ref Expression
0 crngim class RngIso
1 vr setvar r
2 cvv class V
3 vs setvar s
4 vf setvar f
5 1 cv setvar r
6 crnghm class RngHom
7 3 cv setvar s
8 5 7 6 co class r RngHom s
9 4 cv setvar f
10 9 ccnv class f -1
11 7 5 6 co class s RngHom r
12 10 11 wcel wff f -1 ∈ s RngHom r
13 12 4 8 crab class f ∈ r RngHom s | f -1 ∈ s RngHom r
14 1 3 2 2 13 cmpo class r ∈ V , s ∈ V ⟼ f ∈ r RngHom s | f -1 ∈ s RngHom r
15 0 14 wceq wff RngIso = r ∈ V , s ∈ V ⟼ f ∈ r RngHom s | f -1 ∈ s RngHom r