Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rngisom Structured version   Visualization version   GIF version

Definition df-rngisom 44499
 Description: Define the set of non-unital ring isomorphisms from 𝑟 to 𝑠. (Contributed by AV, 20-Feb-2020.)
Assertion
Ref Expression
df-rngisom RngIsom = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RngHomo 𝑠) ∣ 𝑓 ∈ (𝑠 RngHomo 𝑟)})
Distinct variable group:   𝑠,𝑟,𝑓

Detailed syntax breakdown of Definition df-rngisom
StepHypRef Expression
1 crngs 44497 . 2 class RngIsom
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 cvv 3444 . . 3 class V
5 vf . . . . . . 7 setvar 𝑓
65cv 1537 . . . . . 6 class 𝑓
76ccnv 5522 . . . . 5 class 𝑓
83cv 1537 . . . . . 6 class 𝑠
92cv 1537 . . . . . 6 class 𝑟
10 crngh 44496 . . . . . 6 class RngHomo
118, 9, 10co 7139 . . . . 5 class (𝑠 RngHomo 𝑟)
127, 11wcel 2112 . . . 4 wff 𝑓 ∈ (𝑠 RngHomo 𝑟)
139, 8, 10co 7139 . . . 4 class (𝑟 RngHomo 𝑠)
1412, 5, 13crab 3113 . . 3 class {𝑓 ∈ (𝑟 RngHomo 𝑠) ∣ 𝑓 ∈ (𝑠 RngHomo 𝑟)}
152, 3, 4, 4, 14cmpo 7141 . 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RngHomo 𝑠) ∣ 𝑓 ∈ (𝑠 RngHomo 𝑟)})
161, 15wceq 1538 1 wff RngIsom = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RngHomo 𝑠) ∣ 𝑓 ∈ (𝑠 RngHomo 𝑟)})
 Colors of variables: wff setvar class This definition is referenced by:  isrngisom  44507  rngimrcl  44508
 Copyright terms: Public domain W3C validator