Users' Mathboxes 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 38047
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 38046 . 2 class DIsoA
2 vk . . 3 setvar 𝑘
3 cvv 3495 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1527 . . . . 5 class 𝑘
6 clh 37002 . . . . 5 class LHyp
75, 6cfv 6349 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
9 vy . . . . . . . 8 setvar 𝑦
109cv 1527 . . . . . . 7 class 𝑦
114cv 1527 . . . . . . 7 class 𝑤
12 cple 16562 . . . . . . . 8 class le
135, 12cfv 6349 . . . . . . 7 class (le‘𝑘)
1410, 11, 13wbr 5058 . . . . . 6 wff 𝑦(le‘𝑘)𝑤
15 cbs 16473 . . . . . . 7 class Base
165, 15cfv 6349 . . . . . 6 class (Base‘𝑘)
1714, 9, 16crab 3142 . . . . 5 class {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤}
18 vf . . . . . . . . 9 setvar 𝑓
1918cv 1527 . . . . . . . 8 class 𝑓
20 ctrl 37176 . . . . . . . . . 10 class trL
215, 20cfv 6349 . . . . . . . . 9 class (trL‘𝑘)
2211, 21cfv 6349 . . . . . . . 8 class ((trL‘𝑘)‘𝑤)
2319, 22cfv 6349 . . . . . . 7 class (((trL‘𝑘)‘𝑤)‘𝑓)
248cv 1527 . . . . . . 7 class 𝑥
2523, 24, 13wbr 5058 . . . . . 6 wff (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥
26 cltrn 37119 . . . . . . . 8 class LTrn
275, 26cfv 6349 . . . . . . 7 class (LTrn‘𝑘)
2811, 27cfv 6349 . . . . . 6 class ((LTrn‘𝑘)‘𝑤)
2925, 18, 28crab 3142 . . . . 5 class {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥}
308, 17, 29cmpt 5138 . . . 4 class (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})
314, 7, 30cmpt 5138 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥}))
322, 3, 31cmpt 5138 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})))
331, 32wceq 1528 1 wff DIsoA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})))
Colors of variables: wff setvar class
This definition is referenced by:  diaffval  38048
  Copyright terms: Public domain W3C validator