Description: Member of a projective map. (Contributed by NM, 27-Jan-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pmapfval.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
pmapfval.l | ⊢ ≤ = ( le ‘ 𝐾 ) | ||
pmapfval.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | ||
pmapfval.m | ⊢ 𝑀 = ( pmap ‘ 𝐾 ) | ||
Assertion | elpmap | ⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑃 ∈ ( 𝑀 ‘ 𝑋 ) ↔ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑋 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pmapfval.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
2 | pmapfval.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
3 | pmapfval.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | |
4 | pmapfval.m | ⊢ 𝑀 = ( pmap ‘ 𝐾 ) | |
5 | 1 2 3 4 | pmapval | ⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) = { 𝑥 ∈ 𝐴 ∣ 𝑥 ≤ 𝑋 } ) |
6 | 5 | eleq2d | ⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑃 ∈ ( 𝑀 ‘ 𝑋 ) ↔ 𝑃 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑥 ≤ 𝑋 } ) ) |
7 | breq1 | ⊢ ( 𝑥 = 𝑃 → ( 𝑥 ≤ 𝑋 ↔ 𝑃 ≤ 𝑋 ) ) | |
8 | 7 | elrab | ⊢ ( 𝑃 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑥 ≤ 𝑋 } ↔ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑋 ) ) |
9 | 6 8 | bitrdi | ⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑃 ∈ ( 𝑀 ‘ 𝑋 ) ↔ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑋 ) ) ) |