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