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 = LHyp ⁡ K
dia1o.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion diacnvclN ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ∈ dom ⁡ I

Proof

Step Hyp Ref Expression
1 dia1o.h ⊢ H = LHyp ⁡ K
2 dia1o.i ⊢ I = DIsoA ⁡ K ⁡ W
3 1 2 diaf11N ⊢ K ∈ HL ∧ W ∈ H → I : dom ⁡ I ⟶ 1-1 onto ran ⁡ I
4 f1ocnvdm ⊢ I : dom ⁡ I ⟶ 1-1 onto ran ⁡ I ∧ X ∈ ran ⁡ I → I -1 ⁡ X ∈ dom ⁡ I
5 3 4 sylan ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ∈ dom ⁡ I