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

Metamath Proof Explorer

Theorem blockadjliftmap

Description: A "two-stage" construction is obtained by first forming the block relation ( R |X.`'E ) and then adjoining elements as "BlockAdj". Combined, it uses the relation ( ( R |X. ``' E ) u. ``' _E ) ` . (Contributed by Peter Mazsa, 28-Jan-2026)

Ref Expression
Assertion blockadjliftmap 
|- ( ( R |X. `' _E ) AdjLiftMap A ) = { <. m , n >. | ( m e. ( A \ { (/) } ) /\ n = ( m u. ( [ m ] R X. m ) ) ) }

Proof

Step Hyp Ref Expression
1 df-adjliftmap 
 |-  ( ( R |X. `' _E ) AdjLiftMap A ) = ( m e. dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) |-> [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) )
2 df-mpt 
 |-  ( m e. dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) |-> [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) ) = { <. m , n >. | ( m e. dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) /\ n = [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) ) }
3 dmxrnuncnvepres 
 |-  dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) = ( A \ { (/) } )
4 3 eleq2i 
 |-  ( m e. dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) <-> m e. ( A \ { (/) } ) )
5 4 anbi1i 
 |-  ( ( m e. dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) /\ n = [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) ) <-> ( m e. ( A \ { (/) } ) /\ n = [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) ) )
6 eldifi 
 |-  ( m e. ( A \ { (/) } ) -> m e. A )
7 ecuncnvepres 
 |-  ( m e. A -> [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) = ( m u. [ m ] ( R |X. `' _E ) ) )
8 6 7 syl 
 |-  ( m e. ( A \ { (/) } ) -> [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) = ( m u. [ m ] ( R |X. `' _E ) ) )
9 ecxrncnvep2 
 |-  ( m e. _V -> [ m ] ( R |X. `' _E ) = ( [ m ] R X. m ) )
10 9 elv 
 |-  [ m ] ( R |X. `' _E ) = ( [ m ] R X. m )
11 10 uneq2i 
 |-  ( m u. [ m ] ( R |X. `' _E ) ) = ( m u. ( [ m ] R X. m ) )
12 8 11 eqtrdi 
 |-  ( m e. ( A \ { (/) } ) -> [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) = ( m u. ( [ m ] R X. m ) ) )
13 12 eqeq2d 
 |-  ( m e. ( A \ { (/) } ) -> ( n = [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) <-> n = ( m u. ( [ m ] R X. m ) ) ) )
14 13 pm5.32i 
 |-  ( ( m e. ( A \ { (/) } ) /\ n = [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) ) <-> ( m e. ( A \ { (/) } ) /\ n = ( m u. ( [ m ] R X. m ) ) ) )
15 5 14 bitri 
 |-  ( ( m e. dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) /\ n = [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) ) <-> ( m e. ( A \ { (/) } ) /\ n = ( m u. ( [ m ] R X. m ) ) ) )
16 15 opabbii 
 |-  { <. m , n >. | ( m e. dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) /\ n = [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) ) } = { <. m , n >. | ( m e. ( A \ { (/) } ) /\ n = ( m u. ( [ m ] R X. m ) ) ) }
17 1 2 16 3eqtri 
 |-  ( ( R |X. `' _E ) AdjLiftMap A ) = { <. m , n >. | ( m e. ( A \ { (/) } ) /\ n = ( m u. ( [ m ] R X. m ) ) ) }