Theorem dfadjliftmap

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 ) ↾ 𝐴 ) )