# Metamath Proof Explorer

## Theorem diacnvclN

Description: Closure of partial isomorphism A converse. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses dia1o.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dia1o.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
Assertion diacnvclN ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {{I}}^{-1}\left({X}\right)\in \mathrm{dom}{I}$

### Proof

Step Hyp Ref Expression
1 dia1o.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dia1o.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
3 1 2 diaf11N ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}$
4 f1ocnvdm ${⊢}\left({I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}\wedge {X}\in \mathrm{ran}{I}\right)\to {{I}}^{-1}\left({X}\right)\in \mathrm{dom}{I}$
5 3 4 sylan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {{I}}^{-1}\left({X}\right)\in \mathrm{dom}{I}$