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

Metamath Proof Explorer

Theorem dfblockliftmap2

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

Ref Expression
Assertion dfblockliftmap2 ( 𝑅 BlockLiftMap 𝐴 ) = ( 𝑚 ∈ ( 𝐴 ∩ ( dom 𝑅 ∖ { ∅ } ) ) ↦ ( [ 𝑚 ] 𝑅 × 𝑚 ) )

Proof

Step Hyp Ref Expression
1 df-blockliftmap ⊢ ( 𝑅 BlockLiftMap 𝐴 ) = ( 𝑚 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↦ [ 𝑚 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) )
2 elinel1 ⊢ ( 𝑚 ∈ ( 𝐴 ∩ ( dom 𝑅 ∖ { ∅ } ) ) → 𝑚 ∈ 𝐴 )
3 dmxrncnvepres2 ⊢ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) = ( 𝐴 ∩ ( dom 𝑅 ∖ { ∅ } ) )
4 2 3 eleq2s ⊢ ( 𝑚 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) → 𝑚 ∈ 𝐴 )
5 xrnres2 ⊢ ( ( 𝑅 ⋉ ◡ E ) ↾ 𝐴 ) = ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) )
6 5 eceq2i ⊢ [ 𝑚 ] ( ( 𝑅 ⋉ ◡ E ) ↾ 𝐴 ) = [ 𝑚 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) )
7 elecreseq ⊢ ( 𝑚 ∈ 𝐴 → [ 𝑚 ] ( ( 𝑅 ⋉ ◡ E ) ↾ 𝐴 ) = [ 𝑚 ] ( 𝑅 ⋉ ◡ E ) )
8 6 7 eqtr3id ⊢ ( 𝑚 ∈ 𝐴 → [ 𝑚 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) = [ 𝑚 ] ( 𝑅 ⋉ ◡ E ) )
9 ecxrncnvep2 ⊢ ( 𝑚 ∈ 𝐴 → [ 𝑚 ] ( 𝑅 ⋉ ◡ E ) = ( [ 𝑚 ] 𝑅 × 𝑚 ) )
10 8 9 eqtrd ⊢ ( 𝑚 ∈ 𝐴 → [ 𝑚 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) = ( [ 𝑚 ] 𝑅 × 𝑚 ) )
11 4 10 syl ⊢ ( 𝑚 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) → [ 𝑚 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) = ( [ 𝑚 ] 𝑅 × 𝑚 ) )
12 11 mpteq2ia ⊢ ( 𝑚 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↦ [ 𝑚 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) = ( 𝑚 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↦ ( [ 𝑚 ] 𝑅 × 𝑚 ) )
13 3 mpteq1i ⊢ ( 𝑚 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↦ ( [ 𝑚 ] 𝑅 × 𝑚 ) ) = ( 𝑚 ∈ ( 𝐴 ∩ ( dom 𝑅 ∖ { ∅ } ) ) ↦ ( [ 𝑚 ] 𝑅 × 𝑚 ) )
14 1 12 13 3eqtri ⊢ ( 𝑅 BlockLiftMap 𝐴 ) = ( 𝑚 ∈ ( 𝐴 ∩ ( dom 𝑅 ∖ { ∅ } ) ) ↦ ( [ 𝑚 ] 𝑅 × 𝑚 ) )