Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rngoiso Structured version   Visualization version   GIF version

Definition df-rngoiso 32945
 Description: Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011.)
Assertion
Ref Expression
df-rngoiso RngIso = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)})
Distinct variable group:   𝑠,𝑟,𝑓

Detailed syntax breakdown of Definition df-rngoiso
StepHypRef Expression
1 crngiso 32930 . 2 class RngIso
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 crngo 32863 . . 3 class RingOps
52cv 1474 . . . . . . 7 class 𝑟
6 c1st 7057 . . . . . . 7 class 1st
75, 6cfv 5804 . . . . . 6 class (1st𝑟)
87crn 5039 . . . . 5 class ran (1st𝑟)
93cv 1474 . . . . . . 7 class 𝑠
109, 6cfv 5804 . . . . . 6 class (1st𝑠)
1110crn 5039 . . . . 5 class ran (1st𝑠)
12 vf . . . . . 6 setvar 𝑓
1312cv 1474 . . . . 5 class 𝑓
148, 11, 13wf1o 5803 . . . 4 wff 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)
15 crnghom 32929 . . . . 5 class RngHom
165, 9, 15co 6549 . . . 4 class (𝑟 RngHom 𝑠)
1714, 12, 16crab 2900 . . 3 class {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)}
182, 3, 4, 4, 17cmpt2 6551 . 2 class (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)})
191, 18wceq 1475 1 wff RngIso = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)})
 Colors of variables: wff setvar class This definition is referenced by:  rngoisoval  32946
 Copyright terms: Public domain W3C validator