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 𝐼 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ) |
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 | syl6bb | ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ) |