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 𝑅 ∖ { ∅ } ) ) ↦ ( [ 𝑚 ] 𝑅 × 𝑚 ) )