Definition df-disoa 34597

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

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

This definition is referenced by:  diaffval  34598