Metamath Proof Explorer

Definition df-rngiso

Description: Define the set of ring isomorphisms from r to s . (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Assertion df-rngiso ⊢ RingIso = r ∈ V , s ∈ V ⟼ f ∈ r RingHom s | f -1 ∈ s RingHom r

Detailed syntax breakdown

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