Metamath Proof Explorer

Definition df-rngisom

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

Ref Expression
Assertion df-rngisom ⊢ RngIsom = r ∈ V , s ∈ V ⟼ f ∈ r RngHomo s | f -1 ∈ s RngHomo r

Detailed syntax breakdown

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