Users' Mathboxes 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 36113
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 36098 . 2 class RngIso
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 crngo 36031 . . 3 class RingOps
52cv 1540 . . . . . . 7 class 𝑟
6 c1st 7815 . . . . . . 7 class 1st
75, 6cfv 6430 . . . . . 6 class (1st𝑟)
87crn 5589 . . . . 5 class ran (1st𝑟)
93cv 1540 . . . . . . 7 class 𝑠
109, 6cfv 6430 . . . . . 6 class (1st𝑠)
1110crn 5589 . . . . 5 class ran (1st𝑠)
12 vf . . . . . 6 setvar 𝑓
1312cv 1540 . . . . 5 class 𝑓
148, 11, 13wf1o 6429 . . . 4 wff 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)
15 crnghom 36097 . . . . 5 class RngHom
165, 9, 15co 7268 . . . 4 class (𝑟 RngHom 𝑠)
1714, 12, 16crab 3069 . . 3 class {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)}
182, 3, 4, 4, 17cmpo 7270 . 2 class (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st𝑟)–1-1-onto→ran (1st𝑠)})
191, 18wceq 1541 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  36114
  Copyright terms: Public domain W3C validator