Metamath Proof Explorer

Theorem diaclN

Description: Closure of partial isomorphism A for a lattice K . (Contributed by NM, 4-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses dia1o.h ⊢ H = LHyp ⁡ K
dia1o.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion diaclN ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → I ⁡ X ∈ ran ⁡ 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 f1ofun ⊢ I : dom ⁡ I ⟶ 1-1 onto ran ⁡ I → Fun ⁡ I
5 3 4 syl ⊢ K ∈ HL ∧ W ∈ H → Fun ⁡ I
6 fvelrn ⊢ Fun ⁡ I ∧ X ∈ dom ⁡ I → I ⁡ X ∈ ran ⁡ I
7 5 6 sylan ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → I ⁡ X ∈ ran ⁡ I