This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Alternate (expanded) definition of the adjoined lift map. (Contributed by Peter Mazsa, 28-Jan-2026) (Revised by Peter Mazsa, 22-Feb-2026)
|
|
Ref |
Expression |
|
Assertion |
dfadjliftmap |
⊢ ( 𝑅 AdjLiftMap 𝐴 ) = ( 𝑚 ∈ dom ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) ↦ [ 𝑚 ] ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-adjliftmap |
⊢ ( 𝑅 AdjLiftMap 𝐴 ) = QMap ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) |
| 2 |
|
df-qmap |
⊢ QMap ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) = ( 𝑚 ∈ dom ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) ↦ [ 𝑚 ] ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) ) |
| 3 |
1 2
|
eqtri |
⊢ ( 𝑅 AdjLiftMap 𝐴 ) = ( 𝑚 ∈ dom ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) ↦ [ 𝑚 ] ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) ) |