Theorem dfadjliftmap2

Description: Alternate definition of the adjoined lift map. (Contributed by Peter Mazsa, 28-Jan-2026)

	Ref	Expression
Assertion	dfadjliftmap2	⊢ ( 𝑅 AdjLiftMap 𝐴 ) = ( 𝑚 ∈ ( 𝐴 ∩ ( dom 𝑅 ∪ ( V ∖ { ∅ } ) ) ) ↦ ( 𝑚 ∪ [ 𝑚 ] 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		df-adjliftmap	⊢ ( 𝑅 AdjLiftMap 𝐴 ) = ( 𝑚 ∈ dom ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) ↦ [ 𝑚 ] ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) )
2		elinel1	⊢ ( 𝑚 ∈ ( 𝐴 ∩ ( dom 𝑅 ∪ ( V ∖ { ∅ } ) ) ) → 𝑚 ∈ 𝐴 )
3		dmuncnvepres	⊢ dom ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) = ( 𝐴 ∩ ( dom 𝑅 ∪ ( V ∖ { ∅ } ) ) )
4	2 3	eleq2s	⊢ ( 𝑚 ∈ dom ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) → 𝑚 ∈ 𝐴 )
5		ecuncnvepres	⊢ ( 𝑚 ∈ 𝐴 → [ 𝑚 ] ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) = ( 𝑚 ∪ [ 𝑚 ] 𝑅 ) )
6	4 5	syl	⊢ ( 𝑚 ∈ dom ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) → [ 𝑚 ] ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) = ( 𝑚 ∪ [ 𝑚 ] 𝑅 ) )
7	6	mpteq2ia	⊢ ( 𝑚 ∈ dom ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) ↦ [ 𝑚 ] ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) ) = ( 𝑚 ∈ dom ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) ↦ ( 𝑚 ∪ [ 𝑚 ] 𝑅 ) )
8	3	mpteq1i	⊢ ( 𝑚 ∈ dom ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) ↦ ( 𝑚 ∪ [ 𝑚 ] 𝑅 ) ) = ( 𝑚 ∈ ( 𝐴 ∩ ( dom 𝑅 ∪ ( V ∖ { ∅ } ) ) ) ↦ ( 𝑚 ∪ [ 𝑚 ] 𝑅 ) )
9	1 7 8	3eqtri	⊢ ( 𝑅 AdjLiftMap 𝐴 ) = ( 𝑚 ∈ ( 𝐴 ∩ ( dom 𝑅 ∪ ( V ∖ { ∅ } ) ) ) ↦ ( 𝑚 ∪ [ 𝑚 ] 𝑅 ) )