Metamath Proof Explorer


Theorem diaeldm

Description: Member of domain of the partial isomorphism A. (Contributed by NM, 4-Dec-2013)

Ref Expression
Hypotheses diafn.b 𝐵 = ( Base ‘ 𝐾 )
diafn.l = ( le ‘ 𝐾 )
diafn.h 𝐻 = ( LHyp ‘ 𝐾 )
diafn.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion diaeldm ( ( 𝐾𝑉𝑊𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ ( 𝑋𝐵𝑋 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 diafn.b 𝐵 = ( Base ‘ 𝐾 )
2 diafn.l = ( le ‘ 𝐾 )
3 diafn.h 𝐻 = ( LHyp ‘ 𝐾 )
4 diafn.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
5 1 2 3 4 diadm ( ( 𝐾𝑉𝑊𝐻 ) → dom 𝐼 = { 𝑥𝐵𝑥 𝑊 } )
6 5 eleq2d ( ( 𝐾𝑉𝑊𝐻 ) → ( 𝑋 ∈ dom 𝐼𝑋 ∈ { 𝑥𝐵𝑥 𝑊 } ) )
7 breq1 ( 𝑥 = 𝑋 → ( 𝑥 𝑊𝑋 𝑊 ) )
8 7 elrab ( 𝑋 ∈ { 𝑥𝐵𝑥 𝑊 } ↔ ( 𝑋𝐵𝑋 𝑊 ) )
9 6 8 bitrdi ( ( 𝐾𝑉𝑊𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ ( 𝑋𝐵𝑋 𝑊 ) ) )