Theorem dmmpossx2

Description: The domain of a mapping is a subset of its base classes expressed as union of Cartesian products over its second component, analogous to dmmpossx . (Contributed by AV, 30-Mar-2019)

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

Proof

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