Theorem diacnvclN

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

	Ref	Expression
Hypotheses	dia1o.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dia1o.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion	diacnvclN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ dom 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		dia1o.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dia1o.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
3	1 2	diaf11N	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 )
4		f1ocnvdm	⊢ ( ( 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ dom 𝐼 )
5	3 4	sylan	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ dom 𝐼 )