Theorem dibfnN

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

	Ref	Expression
Hypotheses	dibfn.b	$$⊢B={\mathrm{Base}}_K$$
	dibfn.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dibfn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dibfn.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
Assertion	dibfnN	$$⊢\left(K\in V\wedge W\in H\right)\to IFn\left\{x\in B|x\underset{\dot{}}{\le }W\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dibfn.b	$$⊢B={\mathrm{Base}}_K$$
2		dibfn.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dibfn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		dibfn.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
5		eqid	$$⊢\mathrm{DIsoA}\left(K\right)\left(W\right)=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
6	3 5 4	dibfna	$$⊢\left(K\in V\wedge W\in H\right)\to IFn\mathrm{dom}\mathrm{DIsoA}\left(K\right)\left(W\right)$$
7	1 2 3 5	diadm	$$⊢\left(K\in V\wedge W\in H\right)\to \mathrm{dom}\mathrm{DIsoA}\left(K\right)\left(W\right)=\left\{x\in B|x\underset{\dot{}}{\le }W\right\}$$
8	7	fneq2d	$$⊢\left(K\in V\wedge W\in H\right)\to \left(IFn\mathrm{dom}\mathrm{DIsoA}\left(K\right)\left(W\right)\leftrightarrow IFn\left\{x\in B|x\underset{\dot{}}{\le }W\right\}\right)$$
9	6 8	mpbid	$$⊢\left(K\in V\wedge W\in H\right)\to IFn\left\{x\in B|x\underset{\dot{}}{\le }W\right\}$$