Theorem shftdm

Description: Domain of a relation shifted by A . The set on the right is more commonly notated as ( dom F + A ) (meaning add A to every element of dom F ). (Contributed by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Hypothesis	shftfval.1	$$⊢F\in \mathrm{V}$$
Assertion	shftdm	$$⊢A\in ℂ\to \mathrm{dom}\left(F\mathrm{shift}A\right)=\left\{x\in ℂ|x-A\in \mathrm{dom}F\right\}$$

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	$$⊢F\in \mathrm{V}$$
2	1	shftfval	$$⊢A\in ℂ\to F\mathrm{shift}A=\left\{⟨x,y⟩|\left(x\in ℂ\wedge \left(x-A\right)Fy\right)\right\}$$
3	2	dmeqd	$$⊢A\in ℂ\to \mathrm{dom}\left(F\mathrm{shift}A\right)=\mathrm{dom}\left\{⟨x,y⟩|\left(x\in ℂ\wedge \left(x-A\right)Fy\right)\right\}$$
4		19.42v	$$⊢\exists y\left(x\in ℂ\wedge \left(x-A\right)Fy\right)\leftrightarrow \left(x\in ℂ\wedge \exists y\left(x-A\right)Fy\right)$$
5		ovex	$$⊢x-A\in \mathrm{V}$$
6	5	eldm	$$⊢x-A\in \mathrm{dom}F\leftrightarrow \exists y\left(x-A\right)Fy$$
7	6	anbi2i	$$⊢\left(x\in ℂ\wedge x-A\in \mathrm{dom}F\right)\leftrightarrow \left(x\in ℂ\wedge \exists y\left(x-A\right)Fy\right)$$
8	4 7	bitr4i	$$⊢\exists y\left(x\in ℂ\wedge \left(x-A\right)Fy\right)\leftrightarrow \left(x\in ℂ\wedge x-A\in \mathrm{dom}F\right)$$
9	8	abbii	$$⊢\left\{x|\exists y\left(x\in ℂ\wedge \left(x-A\right)Fy\right)\right\}=\left\{x|\left(x\in ℂ\wedge x-A\in \mathrm{dom}F\right)\right\}$$
10		dmopab	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\left(x\in ℂ\wedge \left(x-A\right)Fy\right)\right\}=\left\{x|\exists y\left(x\in ℂ\wedge \left(x-A\right)Fy\right)\right\}$$
11		df-rab	$$⊢\left\{x\in ℂ|x-A\in \mathrm{dom}F\right\}=\left\{x|\left(x\in ℂ\wedge x-A\in \mathrm{dom}F\right)\right\}$$
12	9 10 11	3eqtr4i	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\left(x\in ℂ\wedge \left(x-A\right)Fy\right)\right\}=\left\{x\in ℂ|x-A\in \mathrm{dom}F\right\}$$
13	3 12	eqtrdi	$$⊢A\in ℂ\to \mathrm{dom}\left(F\mathrm{shift}A\right)=\left\{x\in ℂ|x-A\in \mathrm{dom}F\right\}$$