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 𝐻 = ( LHyp ‘ 𝐾 )
dia1o.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion diaclN ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝐼𝑋 ) ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dia1o.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dia1o.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
3 1 2 diaf11N ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐼 : dom 𝐼1-1-onto→ ran 𝐼 )
4 f1ofun ( 𝐼 : dom 𝐼1-1-onto→ ran 𝐼 → Fun 𝐼 )
5 3 4 syl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → Fun 𝐼 )
6 fvelrn ( ( Fun 𝐼𝑋 ∈ dom 𝐼 ) → ( 𝐼𝑋 ) ∈ ran 𝐼 )
7 5 6 sylan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝐼𝑋 ) ∈ ran 𝐼 )