Theorem diafn

Description: Functionality and domain of the partial isomorphism A. (Contributed by NM, 26-Nov-2013)

	Ref	Expression
Hypotheses	diafn.b	|- B = ( Base ` K )
	diafn.l	|- .<_ = ( le ` K )
	diafn.h	|- H = ( LHyp ` K )
	diafn.i	|- I = ( ( DIsoA ` K ) ` W )
Assertion	diafn	|- ( ( K e. V /\ W e. H ) -> I Fn { x e. B | x .<_ W } )

Proof

Step	Hyp	Ref	Expression
1		diafn.b	|- B = ( Base ` K )
2		diafn.l	|- .<_ = ( le ` K )
3		diafn.h	|- H = ( LHyp ` K )
4		diafn.i	|- I = ( ( DIsoA ` K ) ` W )
5		fvex	|- ( ( LTrn ` K ) ` W ) e. _V
6	5	rabex	|- { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ y } e. _V
7		eqid	|- ( y e. { x e. B | x .<_ W } |-> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ y } ) = ( y e. { x e. B | x .<_ W } |-> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ y } )
8	6 7	fnmpti	|- ( y e. { x e. B | x .<_ W } |-> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ y } ) Fn { x e. B | x .<_ W }
9		eqid	|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
10		eqid	|- ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
11	1 2 3 9 10 4	diafval	|- ( ( K e. V /\ W e. H ) -> I = ( y e. { x e. B | x .<_ W } |-> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ y } ) )
12	11	fneq1d	|- ( ( K e. V /\ W e. H ) -> ( I Fn { x e. B | x .<_ W } <-> ( y e. { x e. B | x .<_ W } |-> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) .<_ y } ) Fn { x e. B | x .<_ W } ) )
13	8 12	mpbiri	|- ( ( K e. V /\ W e. H ) -> I Fn { x e. B | x .<_ W } )