Metamath Proof Explorer
Description: Alternate definition of the block lift map. (Contributed by Peter
Mazsa, 29-Jan-2026) (Revised by Peter Mazsa, 22-Feb-2026)
|
|
Ref |
Expression |
|
Assertion |
dfblockliftmap |
⊢ ( 𝑅 BlockLiftMap 𝐴 ) = ( 𝑚 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↦ [ 𝑚 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-blockliftmap |
⊢ ( 𝑅 BlockLiftMap 𝐴 ) = QMap ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) |
| 2 |
|
df-qmap |
⊢ QMap ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) = ( 𝑚 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↦ [ 𝑚 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) |
| 3 |
1 2
|
eqtri |
⊢ ( 𝑅 BlockLiftMap 𝐴 ) = ( 𝑚 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↦ [ 𝑚 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) |