Metamath Proof Explorer


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 V W 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 V
5 snex f LTrn K W I Base K V
6 4 5 xpex J y × f LTrn K W I Base K V
7 eqid y dom J J y × f LTrn K W I Base K = y dom J J y × f LTrn K W I Base K
8 6 7 fnmpti y dom J J y × f 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 LTrn K W I Base K = f LTrn K W I Base K
12 9 1 10 11 2 3 dibfval K V W H I = y dom J J y × f LTrn K W I Base K
13 12 fneq1d K V W H I Fn dom J y dom J J y × f LTrn K W I Base K Fn dom J
14 8 13 mpbiri K V W H I Fn dom J