Metamath Proof Explorer

Theorem dfblockliftmap2

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

Ref Expression
Assertion dfblockliftmap2 
|- ( R BlockLiftMap A ) = ( m e. ( A i^i ( dom R \ { (/) } ) ) |-> ( [ m ] R X. m ) )

Proof

Step Hyp Ref Expression
1 df-blockliftmap 
 |-  ( R BlockLiftMap A ) = ( m e. dom ( R |X. ( `' _E |` A ) ) |-> [ m ] ( R |X. ( `' _E |` A ) ) )
2 elinel1 
 |-  ( m e. ( A i^i ( dom R \ { (/) } ) ) -> m e. A )
3 dmxrncnvepres2 
 |-  dom ( R |X. ( `' _E |` A ) ) = ( A i^i ( dom R \ { (/) } ) )
4 2 3 eleq2s 
 |-  ( m e. dom ( R |X. ( `' _E |` A ) ) -> m e. A )
5 xrnres2 
 |-  ( ( R |X. `' _E ) |` A ) = ( R |X. ( `' _E |` A ) )
6 5 eceq2i 
 |-  [ m ] ( ( R |X. `' _E ) |` A ) = [ m ] ( R |X. ( `' _E |` A ) )
7 elecreseq 
 |-  ( m e. A -> [ m ] ( ( R |X. `' _E ) |` A ) = [ m ] ( R |X. `' _E ) )
8 6 7 eqtr3id 
 |-  ( m e. A -> [ m ] ( R |X. ( `' _E |` A ) ) = [ m ] ( R |X. `' _E ) )
9 ecxrncnvep2 
 |-  ( m e. A -> [ m ] ( R |X. `' _E ) = ( [ m ] R X. m ) )
10 8 9 eqtrd 
 |-  ( m e. A -> [ m ] ( R |X. ( `' _E |` A ) ) = ( [ m ] R X. m ) )
11 4 10 syl 
 |-  ( m e. dom ( R |X. ( `' _E |` A ) ) -> [ m ] ( R |X. ( `' _E |` A ) ) = ( [ m ] R X. m ) )
12 11 mpteq2ia 
 |-  ( m e. dom ( R |X. ( `' _E |` A ) ) |-> [ m ] ( R |X. ( `' _E |` A ) ) ) = ( m e. dom ( R |X. ( `' _E |` A ) ) |-> ( [ m ] R X. m ) )
13 3 mpteq1i 
 |-  ( m e. dom ( R |X. ( `' _E |` A ) ) |-> ( [ m ] R X. m ) ) = ( m e. ( A i^i ( dom R \ { (/) } ) ) |-> ( [ m ] R X. m ) )
14 1 12 13 3eqtri 
 |-  ( R BlockLiftMap A ) = ( m e. ( A i^i ( dom R \ { (/) } ) ) |-> ( [ m ] R X. m ) )