This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐼 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) )