Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-disoa Structured version   Visualization version   GIF version

Definition df-disoa 36820
 Description: Define partial isomorphism A. (Contributed by NM, 15-Oct-2013.)
Assertion
Ref Expression
df-disoa DIsoA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})))
Distinct variable group:   𝑤,𝑘,𝑥,𝑦,𝑓

Detailed syntax breakdown of Definition df-disoa
StepHypRef Expression
1 cdia 36819 . 2 class DIsoA
2 vk . . 3 setvar 𝑘
3 cvv 3340 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1631 . . . . 5 class 𝑘
6 clh 35773 . . . . 5 class LHyp
75, 6cfv 6049 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
9 vy . . . . . . . 8 setvar 𝑦
109cv 1631 . . . . . . 7 class 𝑦
114cv 1631 . . . . . . 7 class 𝑤
12 cple 16150 . . . . . . . 8 class le
135, 12cfv 6049 . . . . . . 7 class (le‘𝑘)
1410, 11, 13wbr 4804 . . . . . 6 wff 𝑦(le‘𝑘)𝑤
15 cbs 16059 . . . . . . 7 class Base
165, 15cfv 6049 . . . . . 6 class (Base‘𝑘)
1714, 9, 16crab 3054 . . . . 5 class {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤}
18 vf . . . . . . . . 9 setvar 𝑓
1918cv 1631 . . . . . . . 8 class 𝑓
20 ctrl 35948 . . . . . . . . . 10 class trL
215, 20cfv 6049 . . . . . . . . 9 class (trL‘𝑘)
2211, 21cfv 6049 . . . . . . . 8 class ((trL‘𝑘)‘𝑤)
2319, 22cfv 6049 . . . . . . 7 class (((trL‘𝑘)‘𝑤)‘𝑓)
248cv 1631 . . . . . . 7 class 𝑥
2523, 24, 13wbr 4804 . . . . . 6 wff (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥
26 cltrn 35890 . . . . . . . 8 class LTrn
275, 26cfv 6049 . . . . . . 7 class (LTrn‘𝑘)
2811, 27cfv 6049 . . . . . 6 class ((LTrn‘𝑘)‘𝑤)
2925, 18, 28crab 3054 . . . . 5 class {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥}
308, 17, 29cmpt 4881 . . . 4 class (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})
314, 7, 30cmpt 4881 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥}))
322, 3, 31cmpt 4881 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})))
331, 32wceq 1632 1 wff DIsoA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})))
 Colors of variables: wff setvar class This definition is referenced by:  diaffval  36821
 Copyright terms: Public domain W3C validator