Metamath Proof Explorer

Definition df-disoa

Description: Define partial isomorphism A. (Contributed by NM, 15-Oct-2013)

Ref Expression
Assertion 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 } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdia 
 |-  DIsoA
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vw 
 |-  w
4 clh 
 |-  LHyp
5 1 cv 
 |-  k
6 5 4 cfv 
 |-  ( LHyp ` k )
7 vx 
 |-  x
8 vy 
 |-  y
9 cbs 
 |-  Base
10 5 9 cfv 
 |-  ( Base ` k )
11 8 cv 
 |-  y
12 cple 
 |-  le
13 5 12 cfv 
 |-  ( le ` k )
14 3 cv 
 |-  w
15 11 14 13 wbr 
 |-  y ( le ` k ) w
16 15 8 10 crab 
 |-  { y e. ( Base ` k ) | y ( le ` k ) w }
17 vf 
 |-  f
18 cltrn 
 |-  LTrn
19 5 18 cfv 
 |-  ( LTrn ` k )
20 14 19 cfv 
 |-  ( ( LTrn ` k ) ` w )
21 ctrl 
 |-  trL
22 5 21 cfv 
 |-  ( trL ` k )
23 14 22 cfv 
 |-  ( ( trL ` k ) ` w )
24 17 cv 
 |-  f
25 24 23 cfv 
 |-  ( ( ( trL ` k ) ` w ) ` f )
26 7 cv 
 |-  x
27 25 26 13 wbr 
 |-  ( ( ( trL ` k ) ` w ) ` f ) ( le ` k ) x
28 27 17 20 crab 
 |-  { f e. ( ( LTrn ` k ) ` w ) | ( ( ( trL ` k ) ` w ) ` f ) ( le ` k ) x }
29 7 16 28 cmpt 
 |-  ( x e. { y e. ( Base ` k ) | y ( le ` k ) w } |-> { f e. ( ( LTrn ` k ) ` w ) | ( ( ( trL ` k ) ` w ) ` f ) ( le ` k ) x } )
30 3 6 29 cmpt 
 |-  ( 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 } ) )
31 1 2 30 cmpt 
 |-  ( 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 } ) ) )
32 0 31 wceq 
 |-  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 } ) ) )