Theorem dmmpossx

Description: The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Hypothesis	fmpox.1	$$⊢F=\left(x\in A,y\in B⟼C\right)$$
Assertion	dmmpossx	$$⊢\mathrm{dom}F\subseteq \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		fmpox.1	$$⊢F=\left(x\in A,y\in B⟼C\right)$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}uB$$
3		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋u/x⦌B$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}uC$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}vC$$
6		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋u/x⦌⦋v/y⦌C$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}yu$$
8		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋v/y⦌C$$
9	7 8	nfcsbw	$$⊢\underset{\_}{Ⅎ}y⦋u/x⦌⦋v/y⦌C$$
10		csbeq1a	$$⊢x=u\to B=⦋u/x⦌B$$
11		csbeq1a	$$⊢y=v\to C=⦋v/y⦌C$$
12		csbeq1a	$$⊢x=u\to ⦋v/y⦌C=⦋u/x⦌⦋v/y⦌C$$
13	11 12	sylan9eqr	$$⊢\left(x=u\wedge y=v\right)\to C=⦋u/x⦌⦋v/y⦌C$$
14	2 3 4 5 6 9 10 13	cbvmpox	$$⊢\left(x\in A,y\in B⟼C\right)=\left(u\in A,v\in ⦋u/x⦌B⟼⦋u/x⦌⦋v/y⦌C\right)$$
15		vex	$$⊢u\in \mathrm{V}$$
16		vex	$$⊢v\in \mathrm{V}$$
17	15 16	op1std	$$⊢t=⟨u,v⟩\to 1^{st}\left(t\right)=u$$
18	17	csbeq1d	$$⊢t=⟨u,v⟩\to ⦋1^{st}\left(t\right)/x⦌⦋2^{nd}\left(t\right)/y⦌C=⦋u/x⦌⦋2^{nd}\left(t\right)/y⦌C$$
19	15 16	op2ndd	$$⊢t=⟨u,v⟩\to 2^{nd}\left(t\right)=v$$
20	19	csbeq1d	$$⊢t=⟨u,v⟩\to ⦋2^{nd}\left(t\right)/y⦌C=⦋v/y⦌C$$
21	20	csbeq2dv	$$⊢t=⟨u,v⟩\to ⦋u/x⦌⦋2^{nd}\left(t\right)/y⦌C=⦋u/x⦌⦋v/y⦌C$$
22	18 21	eqtrd	$$⊢t=⟨u,v⟩\to ⦋1^{st}\left(t\right)/x⦌⦋2^{nd}\left(t\right)/y⦌C=⦋u/x⦌⦋v/y⦌C$$
23	22	mpomptx	$$⊢\left(t\in \bigcup _{u\in A}\left(\left\{u\right\}\times ⦋u/x⦌B\right)⟼⦋1^{st}\left(t\right)/x⦌⦋2^{nd}\left(t\right)/y⦌C\right)=\left(u\in A,v\in ⦋u/x⦌B⟼⦋u/x⦌⦋v/y⦌C\right)$$
24	14 1 23	3eqtr4i	$$⊢F=\left(t\in \bigcup _{u\in A}\left(\left\{u\right\}\times ⦋u/x⦌B\right)⟼⦋1^{st}\left(t\right)/x⦌⦋2^{nd}\left(t\right)/y⦌C\right)$$
25	24	dmmptss	$$⊢\mathrm{dom}F\subseteq \bigcup _{u\in A}\left(\left\{u\right\}\times ⦋u/x⦌B\right)$$
26		nfcv	$$⊢\underset{\_}{Ⅎ}u\left(\left\{x\right\}\times B\right)$$
27		nfcv	$$⊢\underset{\_}{Ⅎ}x\left\{u\right\}$$
28	27 3	nfxp	$$⊢\underset{\_}{Ⅎ}x\left(\left\{u\right\}\times ⦋u/x⦌B\right)$$
29		sneq	$$⊢x=u\to \left\{x\right\}=\left\{u\right\}$$
30	29 10	xpeq12d	$$⊢x=u\to \left\{x\right\}\times B=\left\{u\right\}\times ⦋u/x⦌B$$
31	26 28 30	cbviun	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)=\bigcup _{u\in A}\left(\left\{u\right\}\times ⦋u/x⦌B\right)$$
32	25 31	sseqtrri	$$⊢\mathrm{dom}F\subseteq \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)$$