Theorem dmxrnuncnvepres

Description: Domain of the combined relation of two special relations, see blockadjliftmap . (Contributed by Peter Mazsa, 28-Jan-2026)

	Ref	Expression
Assertion	dmxrnuncnvepres	$$⊢\mathrm{dom}\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)=A\setminus \left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		dmuncnvepres	$$⊢\mathrm{dom}\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)=A\cap \left(\mathrm{dom}R⋉{\mathrm{E}}^{-1}\cup \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)\right)$$
2		dmxrncnvep	$$⊢\mathrm{dom}R⋉{\mathrm{E}}^{-1}=\mathrm{dom}R\setminus \left\{\varnothing \right\}$$
3	2	uneq1i	$$⊢\mathrm{dom}R⋉{\mathrm{E}}^{-1}\cup \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)=\left(\mathrm{dom}R\setminus \left\{\varnothing \right\}\right)\cup \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$$
4		difundir	$$⊢\left(\mathrm{dom}R\cup \mathrm{V}\right)\setminus \left\{\varnothing \right\}=\left(\mathrm{dom}R\setminus \left\{\varnothing \right\}\right)\cup \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$$
5		unv	$$⊢\mathrm{dom}R\cup \mathrm{V}=\mathrm{V}$$
6	5	difeq1i	$$⊢\left(\mathrm{dom}R\cup \mathrm{V}\right)\setminus \left\{\varnothing \right\}=\mathrm{V}\setminus \left\{\varnothing \right\}$$
7	3 4 6	3eqtr2i	$$⊢\mathrm{dom}R⋉{\mathrm{E}}^{-1}\cup \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)=\mathrm{V}\setminus \left\{\varnothing \right\}$$
8	7	ineq2i	$$⊢A\cap \left(\mathrm{dom}R⋉{\mathrm{E}}^{-1}\cup \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)\right)=A\cap \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$$
9		invdif	$$⊢A\cap \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)=A\setminus \left\{\varnothing \right\}$$
10	1 8 9	3eqtri	$$⊢\mathrm{dom}\left({\left(R⋉{\mathrm{E}}^{-1}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)=A\setminus \left\{\varnothing \right\}$$