MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rngiso Structured version   Visualization version   GIF version

Definition df-rngiso 18488
Description: Define the set of ring isomorphisms from 𝑟 to 𝑠. (Contributed by Stefan O'Rear, 7-Mar-2015.)
Assertion
Ref Expression
df-rngiso RingIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ 𝑓 ∈ (𝑠 RingHom 𝑟)})
Distinct variable group:   𝑠,𝑟,𝑓

Detailed syntax breakdown of Definition df-rngiso
StepHypRef Expression
1 crs 18485 . 2 class RingIso
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 cvv 3173 . . 3 class V
5 vf . . . . . . 7 setvar 𝑓
65cv 1474 . . . . . 6 class 𝑓
76ccnv 5027 . . . . 5 class 𝑓
83cv 1474 . . . . . 6 class 𝑠
92cv 1474 . . . . . 6 class 𝑟
10 crh 18484 . . . . . 6 class RingHom
118, 9, 10co 6527 . . . . 5 class (𝑠 RingHom 𝑟)
127, 11wcel 1977 . . . 4 wff 𝑓 ∈ (𝑠 RingHom 𝑟)
139, 8, 10co 6527 . . . 4 class (𝑟 RingHom 𝑠)
1412, 5, 13crab 2900 . . 3 class {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ 𝑓 ∈ (𝑠 RingHom 𝑟)}
152, 3, 4, 4, 14cmpt2 6529 . 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ 𝑓 ∈ (𝑠 RingHom 𝑟)})
161, 15wceq 1475 1 wff RingIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ 𝑓 ∈ (𝑠 RingHom 𝑟)})
Colors of variables: wff setvar class
This definition is referenced by:  isrim0  18495  rimrcl  18496  brric  18516
  Copyright terms: Public domain W3C validator