Theorem diadmclN

Description: A member of domain of the partial isomorphism A is a lattice element. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	diadmcl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	diadmcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	diadmcl.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion	diadmclN	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝑋 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		diadmcl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		diadmcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		diadmcl.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
4		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5	1 4 2 3	diaeldm	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) )
6	5	simprbda	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝑋 ∈ 𝐵 )