Theorem dicdmN

Description: Domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dicfn.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dicfn.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dicfn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dicfn.i	$$⊢I=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
Assertion	dicdmN	$$⊢\left(K\in V\wedge W\in H\right)\to \mathrm{dom}I=\left\{p\in A|\neg p\underset{\dot{}}{\le }W\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dicfn.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dicfn.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3		dicfn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		dicfn.i	$$⊢I=\mathrm{DIsoC}\left(K\right)\left(W\right)$$
5	1 2 3 4	dicfnN	$$⊢\left(K\in V\wedge W\in H\right)\to IFn\left\{p\in A|\neg p\underset{\dot{}}{\le }W\right\}$$
6	5	fndmd	$$⊢\left(K\in V\wedge W\in H\right)\to \mathrm{dom}I=\left\{p\in A|\neg p\underset{\dot{}}{\le }W\right\}$$