Metamath Proof Explorer

Theorem dibclN

Description: Closure of partial isomorphism B for a lattice K . (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dibcl.h ⊢ H = LHyp ⁡ K
dibcl.i ⊢ I = DIsoB ⁡ K ⁡ W
Assertion dibclN ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → I ⁡ X ∈ ran ⁡ I

Proof

Step Hyp Ref Expression
1 dibcl.h ⊢ H = LHyp ⁡ K
2 dibcl.i ⊢ I = DIsoB ⁡ K ⁡ W
3 eqid ⊢ DIsoA ⁡ K ⁡ W = DIsoA ⁡ K ⁡ W
4 1 3 2 dibfna ⊢ K ∈ HL ∧ W ∈ H → I Fn dom ⁡ DIsoA ⁡ K ⁡ W
5 fnfun ⊢ I Fn dom ⁡ DIsoA ⁡ K ⁡ W → Fun ⁡ I
6 4 5 syl ⊢ K ∈ HL ∧ W ∈ H → Fun ⁡ I
7 fvelrn ⊢ Fun ⁡ I ∧ X ∈ dom ⁡ I → I ⁡ X ∈ ran ⁡ I
8 6 7 sylan ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → I ⁡ X ∈ ran ⁡ I