Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-disoa Unicode version

Definition df-disoa 31841
Description: Define partial isomorphism A. (Contributed by NM, 15-Oct-2013.)
Assertion
Ref Expression
df-disoa  |-  DIsoA  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  { y  e.  ( Base `  k
)  |  y ( le `  k ) w }  |->  { f  e.  ( ( LTrn `  k ) `  w
)  |  ( ( ( trL `  k
) `  w ) `  f ) ( le
`  k ) x } ) ) )
Distinct variable group:    w, k, x, y, f

Detailed syntax breakdown of Definition df-disoa
StepHypRef Expression
1 cdia 31840 . 2  class  DIsoA
2 vk . . 3  set  k
3 cvv 2801 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1631 . . . . 5  class  k
6 clh 30795 . . . . 5  class  LHyp
75, 6cfv 5271 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  set  x
9 vy . . . . . . . 8  set  y
109cv 1631 . . . . . . 7  class  y
114cv 1631 . . . . . . 7  class  w
12 cple 13231 . . . . . . . 8  class  le
135, 12cfv 5271 . . . . . . 7  class  ( le
`  k )
1410, 11, 13wbr 4039 . . . . . 6  wff  y ( le `  k ) w
15 cbs 13164 . . . . . . 7  class  Base
165, 15cfv 5271 . . . . . 6  class  ( Base `  k )
1714, 9, 16crab 2560 . . . . 5  class  { y  e.  ( Base `  k
)  |  y ( le `  k ) w }
18 vf . . . . . . . . 9  set  f
1918cv 1631 . . . . . . . 8  class  f
20 ctrl 30969 . . . . . . . . . 10  class  trL
215, 20cfv 5271 . . . . . . . . 9  class  ( trL `  k )
2211, 21cfv 5271 . . . . . . . 8  class  ( ( trL `  k ) `
 w )
2319, 22cfv 5271 . . . . . . 7  class  ( ( ( trL `  k
) `  w ) `  f )
248cv 1631 . . . . . . 7  class  x
2523, 24, 13wbr 4039 . . . . . 6  wff  ( ( ( trL `  k
) `  w ) `  f ) ( le
`  k ) x
26 cltrn 30912 . . . . . . . 8  class  LTrn
275, 26cfv 5271 . . . . . . 7  class  ( LTrn `  k )
2811, 27cfv 5271 . . . . . 6  class  ( (
LTrn `  k ) `  w )
2925, 18, 28crab 2560 . . . . 5  class  { f  e.  ( ( LTrn `  k ) `  w
)  |  ( ( ( trL `  k
) `  w ) `  f ) ( le
`  k ) x }
308, 17, 29cmpt 4093 . . . 4  class  ( x  e.  { y  e.  ( Base `  k
)  |  y ( le `  k ) w }  |->  { f  e.  ( ( LTrn `  k ) `  w
)  |  ( ( ( trL `  k
) `  w ) `  f ) ( le
`  k ) x } )
314, 7, 30cmpt 4093 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  ( x  e. 
{ y  e.  (
Base `  k )  |  y ( le
`  k ) w }  |->  { f  e.  ( ( LTrn `  k
) `  w )  |  ( ( ( trL `  k ) `
 w ) `  f ) ( le
`  k ) x } ) )
322, 3, 31cmpt 4093 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  ( x  e. 
{ y  e.  (
Base `  k )  |  y ( le
`  k ) w }  |->  { f  e.  ( ( LTrn `  k
) `  w )  |  ( ( ( trL `  k ) `
 w ) `  f ) ( le
`  k ) x } ) ) )
331, 32wceq 1632 1  wff  DIsoA  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  { y  e.  ( Base `  k
)  |  y ( le `  k ) w }  |->  { f  e.  ( ( LTrn `  k ) `  w
)  |  ( ( ( trL `  k
) `  w ) `  f ) ( le
`  k ) x } ) ) )
Colors of variables: wff set class
This definition is referenced by:  diaffval  31842
  Copyright terms: Public domain W3C validator