Theorem dibfna

Description: Functionality and domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014)

	Ref	Expression
Hypotheses	dibfna.h	|- H = ( LHyp ` K )
	dibfna.j	|- J = ( ( DIsoA ` K ) ` W )
	dibfna.i	|- I = ( ( DIsoB ` K ) ` W )
Assertion	dibfna	|- ( ( K e. V /\ W e. H ) -> I Fn dom J )

Proof

Step	Hyp	Ref	Expression
1		dibfna.h	|- H = ( LHyp ` K )
2		dibfna.j	|- J = ( ( DIsoA ` K ) ` W )
3		dibfna.i	|- I = ( ( DIsoB ` K ) ` W )
4		fvex	|- ( J ` y ) e. _V
5		snex	|- { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } e. _V
6	4 5	xpex	|- ( ( J ` y ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) e. _V
7		eqid	|- ( y e. dom J |-> ( ( J ` y ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) ) = ( y e. dom J |-> ( ( J ` y ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) )
8	6 7	fnmpti	|- ( y e. dom J |-> ( ( J ` y ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) ) Fn dom J
9		eqid	|- ( Base ` K ) = ( Base ` K )
10		eqid	|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
11		eqid	|- ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) )
12	9 1 10 11 2 3	dibfval	|- ( ( K e. V /\ W e. H ) -> I = ( y e. dom J |-> ( ( J ` y ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) ) )
13	12	fneq1d	|- ( ( K e. V /\ W e. H ) -> ( I Fn dom J <-> ( y e. dom J |-> ( ( J ` y ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) } ) ) Fn dom J ) )
14	8 13	mpbiri	|- ( ( K e. V /\ W e. H ) -> I Fn dom J )