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 35336
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 35335 . 2 class DIsoA
2 vk . . 3 setvar 𝑘
3 cvv 3173 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1474 . . . . 5 class 𝑘
6 clh 34288 . . . . 5 class LHyp
75, 6cfv 5804 . . . 4 class (LHyp‘𝑘)
8 vx . . . . 5 setvar 𝑥
9 vy . . . . . . . 8 setvar 𝑦
109cv 1474 . . . . . . 7 class 𝑦
114cv 1474 . . . . . . 7 class 𝑤
12 cple 15775 . . . . . . . 8 class le
135, 12cfv 5804 . . . . . . 7 class (le‘𝑘)
1410, 11, 13wbr 4583 . . . . . 6 wff 𝑦(le‘𝑘)𝑤
15 cbs 15695 . . . . . . 7 class Base
165, 15cfv 5804 . . . . . 6 class (Base‘𝑘)
1714, 9, 16crab 2900 . . . . 5 class {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤}
18 vf . . . . . . . . 9 setvar 𝑓
1918cv 1474 . . . . . . . 8 class 𝑓
20 ctrl 34463 . . . . . . . . . 10 class trL
215, 20cfv 5804 . . . . . . . . 9 class (trL‘𝑘)
2211, 21cfv 5804 . . . . . . . 8 class ((trL‘𝑘)‘𝑤)
2319, 22cfv 5804 . . . . . . 7 class (((trL‘𝑘)‘𝑤)‘𝑓)
248cv 1474 . . . . . . 7 class 𝑥
2523, 24, 13wbr 4583 . . . . . 6 wff (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥
26 cltrn 34405 . . . . . . . 8 class LTrn
275, 26cfv 5804 . . . . . . 7 class (LTrn‘𝑘)
2811, 27cfv 5804 . . . . . 6 class ((LTrn‘𝑘)‘𝑤)
2925, 18, 28crab 2900 . . . . 5 class {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥}
308, 17, 29cmpt 4643 . . . 4 class (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})
314, 7, 30cmpt 4643 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥}))
322, 3, 31cmpt 4643 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})))
331, 32wceq 1475 1 wff DIsoA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})))
Colors of variables: wff setvar class
This definition is referenced by:  diaffval  35337
  Copyright terms: Public domain W3C validator