dibfna

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

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) \in V$
5		snex	$⊢ \{(f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\} \in V$
6	4 5	xpex	$⊢ J (y) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\} \in V$
7		eqid	$⊢ (y \in dom J ⟼ J (y) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\}) = (y \in dom J ⟼ J (y) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\})$
8	6 7	fnmpti	$⊢ (y \in dom J ⟼ J (y) \times \{(f \in 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 \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})$
12	9 1 10 11 2 3	dibfval	$⊢ (K \in V \land W \in H) \to I = (y \in dom J ⟼ J (y) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\})$
13	12	fneq1d	$⊢ (K \in V \land W \in H) \to (I Fn dom J \leftrightarrow (y \in dom J ⟼ J (y) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\}) Fn dom J)$
14	8 13	mpbiri	$⊢ (K \in V \land W \in H) \to I Fn dom J$

Metamath Proof Explorer