Description: Domain of the partial isomorphism A. (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dibfn.b | |- B = ( Base ` K ) |
|
dibfn.l | |- .<_ = ( le ` K ) |
||
dibfn.h | |- H = ( LHyp ` K ) |
||
dibfn.i | |- I = ( ( DIsoB ` K ) ` W ) |
||
Assertion | dibdmN | |- ( ( K e. V /\ W e. H ) -> dom I = { x e. B | x .<_ W } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dibfn.b | |- B = ( Base ` K ) |
|
2 | dibfn.l | |- .<_ = ( le ` K ) |
|
3 | dibfn.h | |- H = ( LHyp ` K ) |
|
4 | dibfn.i | |- I = ( ( DIsoB ` K ) ` W ) |
|
5 | 1 2 3 4 | dibfnN | |- ( ( K e. V /\ W e. H ) -> I Fn { x e. B | x .<_ W } ) |
6 | 5 | fndmd | |- ( ( K e. V /\ W e. H ) -> dom I = { x e. B | x .<_ W } ) |