This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∖ { ∅ } ) ) ) ↦ ( 𝑚 ∪ [ 𝑚 ] 𝑅 ) )