Theorem dfblockliftmap2

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

	Ref	Expression
Assertion	dfblockliftmap2	Could not format assertion : No typesetting found for |- ( R BlockLiftMap A ) = ( m e. ( A i^i ( dom R \ { (/) } ) ) |-> ( [ m ] R X. m ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-blockliftmap	Could not format ( R BlockLiftMap A ) = ( m e. dom ( R |X. ( `' _E |` A ) ) |-> [ m ] ( R |X. ( `' _E |` A ) ) ) : No typesetting found for |- ( R BlockLiftMap A ) = ( m e. dom ( R |X. ( `' _E |` A ) ) |-> [ m ] ( R |X. ( `' _E |` A ) ) ) with typecode |-
2		elinel1	$$⊢m\in \left(A\cap \left(\mathrm{dom}R\setminus \left\{\varnothing \right\}\right)\right)\to m\in A$$
3		dmxrncnvepres2	$$⊢\mathrm{dom}R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\cap \left(\mathrm{dom}R\setminus \left\{\varnothing \right\}\right)$$
4	2 3	eleq2s	$$⊢m\in \mathrm{dom}R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\to m\in A$$
5		xrnres2	$$⊢{R⋉{\mathrm{E}}^{-1}\upharpoonright }_A=R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
6	5	eceq2i	$$⊢\left[m\right]\left({R⋉{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\left[m\right]R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
7		elecreseq	$$⊢m\in A\to \left[m\right]\left({R⋉{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\left[m\right]R⋉{\mathrm{E}}^{-1}$$
8	6 7	eqtr3id	$$⊢m\in A\to \left[m\right]R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\left[m\right]R⋉{\mathrm{E}}^{-1}$$
9		ecxrncnvep2	$$⊢m\in A\to \left[m\right]R⋉{\mathrm{E}}^{-1}=\left[m\right]R\times m$$
10	8 9	eqtrd	$$⊢m\in A\to \left[m\right]R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\left[m\right]R\times m$$
11	4 10	syl	$$⊢m\in \mathrm{dom}R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\to \left[m\right]R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\left[m\right]R\times m$$
12	11	mpteq2ia	$$⊢\left(m\in \mathrm{dom}R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)⟼\left[m\right]R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\right)=\left(m\in \mathrm{dom}R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)⟼\left[m\right]R\times m\right)$$
13	3	mpteq1i	$$⊢\left(m\in \mathrm{dom}R⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)⟼\left[m\right]R\times m\right)=\left(m\in \left(A\cap \left(\mathrm{dom}R\setminus \left\{\varnothing \right\}\right)\right)⟼\left[m\right]R\times m\right)$$
14	1 12 13	3eqtri	Could not format ( R BlockLiftMap A ) = ( m e. ( A i^i ( dom R \ { (/) } ) ) |-> ( [ m ] R X. m ) ) : No typesetting found for |- ( R BlockLiftMap A ) = ( m e. ( A i^i ( dom R \ { (/) } ) ) |-> ( [ m ] R X. m ) ) with typecode |-