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 
|- ( R AdjLiftMap A ) = ( m e. ( A i^i ( dom R u. ( _V \ { (/) } ) ) ) |-> ( m u. [ m ] R ) )

Proof

Step Hyp Ref Expression
1 df-adjliftmap 
 |-  ( R AdjLiftMap A ) = ( m e. dom ( ( R u. `' _E ) |` A ) |-> [ m ] ( ( R u. `' _E ) |` A ) )
2 elinel1 
 |-  ( m e. ( A i^i ( dom R u. ( _V \ { (/) } ) ) ) -> m e. A )
3 dmuncnvepres 
 |-  dom ( ( R u. `' _E ) |` A ) = ( A i^i ( dom R u. ( _V \ { (/) } ) ) )
4 2 3 eleq2s 
 |-  ( m e. dom ( ( R u. `' _E ) |` A ) -> m e. A )
5 ecuncnvepres 
 |-  ( m e. A -> [ m ] ( ( R u. `' _E ) |` A ) = ( m u. [ m ] R ) )
6 4 5 syl 
 |-  ( m e. dom ( ( R u. `' _E ) |` A ) -> [ m ] ( ( R u. `' _E ) |` A ) = ( m u. [ m ] R ) )
7 6 mpteq2ia 
 |-  ( m e. dom ( ( R u. `' _E ) |` A ) |-> [ m ] ( ( R u. `' _E ) |` A ) ) = ( m e. dom ( ( R u. `' _E ) |` A ) |-> ( m u. [ m ] R ) )
8 3 mpteq1i 
 |-  ( m e. dom ( ( R u. `' _E ) |` A ) |-> ( m u. [ m ] R ) ) = ( m e. ( A i^i ( dom R u. ( _V \ { (/) } ) ) ) |-> ( m u. [ m ] R ) )
9 1 7 8 3eqtri 
 |-  ( R AdjLiftMap A ) = ( m e. ( A i^i ( dom R u. ( _V \ { (/) } ) ) ) |-> ( m u. [ m ] R ) )