Theorem ovmpt3rabdm

Description: If the value of a function which is the result of an operation defined by the maps-to notation is not empty, the operands and the argument of the function must be sets. (Contributed by AV, 16-May-2019)

	Ref	Expression
Hypotheses	ovmpt3rab1.o	$$⊢O=\left(x\in \mathrm{V},y\in \mathrm{V}⟼\left(z\in M⟼\left\{a\in N|\phi \right\}\right)\right)$$
	ovmpt3rab1.m	$$⊢\left(x=X\wedge y=Y\right)\to M=K$$
	ovmpt3rab1.n	$$⊢\left(x=X\wedge y=Y\right)\to N=L$$
Assertion	ovmpt3rabdm	$$⊢\left(\left(X\in V\wedge Y\in W\wedge K\in U\right)\wedge L\in T\right)\to \mathrm{dom}\left(XOY\right)=K$$

Proof

Step	Hyp	Ref	Expression
1		ovmpt3rab1.o	$$⊢O=\left(x\in \mathrm{V},y\in \mathrm{V}⟼\left(z\in M⟼\left\{a\in N|\phi \right\}\right)\right)$$
2		ovmpt3rab1.m	$$⊢\left(x=X\wedge y=Y\right)\to M=K$$
3		ovmpt3rab1.n	$$⊢\left(x=X\wedge y=Y\right)\to N=L$$
4		sbceq1a	$$⊢y=Y\to \left(\phi \leftrightarrow \underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right)$$
5		sbceq1a	$$⊢x=X\to \left(\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right)$$
6	4 5	sylan9bbr	$$⊢\left(x=X\wedge y=Y\right)\to \left(\phi \leftrightarrow \underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right)$$
7		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}yX$$
9		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi$$
10	8 9	nfsbcw	$$⊢Ⅎy\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi$$
11	1 2 3 6 7 10	ovmpt3rab1	$$⊢\left(X\in V\wedge Y\in W\wedge K\in U\right)\to XOY=\left(z\in K⟼\left\{a\in L|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right\}\right)$$
12	11	adantr	$$⊢\left(\left(X\in V\wedge Y\in W\wedge K\in U\right)\wedge L\in T\right)\to XOY=\left(z\in K⟼\left\{a\in L|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right\}\right)$$
13	12	dmeqd	$$⊢\left(\left(X\in V\wedge Y\in W\wedge K\in U\right)\wedge L\in T\right)\to \mathrm{dom}\left(XOY\right)=\mathrm{dom}\left(z\in K⟼\left\{a\in L|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right\}\right)$$
14		rabexg	$$⊢L\in T\to \left\{a\in L|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}$$
15	14	adantl	$$⊢\left(\left(X\in V\wedge Y\in W\wedge K\in U\right)\wedge L\in T\right)\to \left\{a\in L|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}$$
16	15	ralrimivw	$$⊢\left(\left(X\in V\wedge Y\in W\wedge K\in U\right)\wedge L\in T\right)\to \forall z\in K\left\{a\in L|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}$$
17		dmmptg	$$⊢\forall z\in K\left\{a\in L|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}\to \mathrm{dom}\left(z\in K⟼\left\{a\in L|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right\}\right)=K$$
18	16 17	syl	$$⊢\left(\left(X\in V\wedge Y\in W\wedge K\in U\right)\wedge L\in T\right)\to \mathrm{dom}\left(z\in K⟼\left\{a\in L|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right\}\right)=K$$
19	13 18	eqtrd	$$⊢\left(\left(X\in V\wedge Y\in W\wedge K\in U\right)\wedge L\in T\right)\to \mathrm{dom}\left(XOY\right)=K$$