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	Could not format assertion : No typesetting found for |- ( ( R |X. `' _E ) AdjLiftMap A ) = { <. m , n >. | ( m e. ( A \ { (/) } ) /\ n = ( m u. ( [ m ] R X. m ) ) ) } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-adjliftmap	Could not format ( ( R |X. `' _E ) AdjLiftMap A ) = ( m e. dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) |-> [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) ) : No typesetting found for |- ( ( R |X. `' _E ) AdjLiftMap A ) = ( m e. dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) |-> [ m ] ( ( ( R |X. `' _E ) u. `' _E ) |` A ) ) with typecode |-
2		df-mpt	$$⊢\left(m\in \mathrm{dom}\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)⟼\left[m\right]\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)\right)=\left\{⟨m,n⟩|\left(m\in \mathrm{dom}\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)\wedge n=\left[m\right]\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)\right)\right\}$$
3		dmxrnuncnvepres	$$⊢\mathrm{dom}\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)=A\setminus \left\{\varnothing \right\}$$
4	3	eleq2i	$$⊢m\in \mathrm{dom}\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)\leftrightarrow m\in \left(A\setminus \left\{\varnothing \right\}\right)$$
5	4	anbi1i	$$⊢\left(m\in \mathrm{dom}\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)\wedge n=\left[m\right]\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)\right)\leftrightarrow \left(m\in \left(A\setminus \left\{\varnothing \right\}\right)\wedge n=\left[m\right]\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)\right)$$
6		eldifi	$$⊢m\in \left(A\setminus \left\{\varnothing \right\}\right)\to m\in A$$
7		ecuncnvepres	$$⊢m\in A\to \left[m\right]\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)=m\cup \left[m\right]R⋉{\mathrm{E}}^{-1}$$
8	6 7	syl	$$⊢m\in \left(A\setminus \left\{\varnothing \right\}\right)\to \left[m\right]\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)=m\cup \left[m\right]R⋉{\mathrm{E}}^{-1}$$
9		ecxrncnvep2	$$⊢m\in \mathrm{V}\to \left[m\right]R⋉{\mathrm{E}}^{-1}=\left[m\right]R\times m$$
10	9	elv	$$⊢\left[m\right]R⋉{\mathrm{E}}^{-1}=\left[m\right]R\times m$$
11	10	uneq2i	$$⊢m\cup \left[m\right]R⋉{\mathrm{E}}^{-1}=m\cup \left(\left[m\right]R\times m\right)$$
12	8 11	eqtrdi	$$⊢m\in \left(A\setminus \left\{\varnothing \right\}\right)\to \left[m\right]\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)=m\cup \left(\left[m\right]R\times m\right)$$
13	12	eqeq2d	$$⊢m\in \left(A\setminus \left\{\varnothing \right\}\right)\to \left(n=\left[m\right]\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)\leftrightarrow n=m\cup \left(\left[m\right]R\times m\right)\right)$$
14	13	pm5.32i	$$⊢\left(m\in \left(A\setminus \left\{\varnothing \right\}\right)\wedge n=\left[m\right]\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)\right)\leftrightarrow \left(m\in \left(A\setminus \left\{\varnothing \right\}\right)\wedge n=m\cup \left(\left[m\right]R\times m\right)\right)$$
15	5 14	bitri	$$⊢\left(m\in \mathrm{dom}\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)\wedge n=\left[m\right]\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)\right)\leftrightarrow \left(m\in \left(A\setminus \left\{\varnothing \right\}\right)\wedge n=m\cup \left(\left[m\right]R\times m\right)\right)$$
16	15	opabbii	$$⊢\left\{⟨m,n⟩|\left(m\in \mathrm{dom}\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)\wedge n=\left[m\right]\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)\right)\right\}=\left\{⟨m,n⟩|\left(m\in \left(A\setminus \left\{\varnothing \right\}\right)\wedge n=m\cup \left(\left[m\right]R\times m\right)\right)\right\}$$
17	1 2 16	3eqtri	Could not format ( ( R |X. `' _E ) AdjLiftMap A ) = { <. m , n >. | ( m e. ( A \ { (/) } ) /\ n = ( m u. ( [ m ] R X. m ) ) ) } : No typesetting found for |- ( ( R |X. `' _E ) AdjLiftMap A ) = { <. m , n >. | ( m e. ( A \ { (/) } ) /\ n = ( m u. ( [ m ] R X. m ) ) ) } with typecode |-