Theorem dibeldmN

Description: Member of domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dibfn.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dibfn.l	⊢ ≤ = ( le ‘ 𝐾 )
	dibfn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dibfn.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dibeldmN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dibfn.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dibfn.l	⊢ ≤ = ( le ‘ 𝐾 )
3		dibfn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		dibfn.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
5		eqid	⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
6	3 5 4	dibdiadm	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) )
7	6	eleq2d	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ 𝑋 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ) )
8	1 2 3 5	diaeldm	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) )
9	7 8	bitrd	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) )