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