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 = ( x e. _V , y e. _V |-> ( z e. M |-> { a e. N | ph } ) )
	ovmpt3rab1.m	|- ( ( x = X /\ y = Y ) -> M = K )
	ovmpt3rab1.n	|- ( ( x = X /\ y = Y ) -> N = L )
Assertion	ovmpt3rabdm	|- ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> dom ( X O Y ) = K )

Proof

Step	Hyp	Ref	Expression
1		ovmpt3rab1.o	|- O = ( x e. _V , y e. _V |-> ( z e. M |-> { a e. N | ph } ) )
2		ovmpt3rab1.m	|- ( ( x = X /\ y = Y ) -> M = K )
3		ovmpt3rab1.n	|- ( ( x = X /\ y = Y ) -> N = L )
4		sbceq1a	|- ( y = Y -> ( ph <-> [. Y / y ]. ph ) )
5		sbceq1a	|- ( x = X -> ( [. Y / y ]. ph <-> [. X / x ]. [. Y / y ]. ph ) )
6	4 5	sylan9bbr	|- ( ( x = X /\ y = Y ) -> ( ph <-> [. X / x ]. [. Y / y ]. ph ) )
7		nfsbc1v	|- F/ x [. X / x ]. [. Y / y ]. ph
8		nfcv	|- F/_ y X
9		nfsbc1v	|- F/ y [. Y / y ]. ph
10	8 9	nfsbcw	|- F/ y [. X / x ]. [. Y / y ]. ph
11	1 2 3 6 7 10	ovmpt3rab1	|- ( ( X e. V /\ Y e. W /\ K e. U ) -> ( X O Y ) = ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) )
12	11	adantr	|- ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> ( X O Y ) = ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) )
13	12	dmeqd	|- ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> dom ( X O Y ) = dom ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) )
14		rabexg	|- ( L e. T -> { a e. L | [. X / x ]. [. Y / y ]. ph } e. _V )
15	14	adantl	|- ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> { a e. L | [. X / x ]. [. Y / y ]. ph } e. _V )
16	15	ralrimivw	|- ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> A. z e. K { a e. L | [. X / x ]. [. Y / y ]. ph } e. _V )
17		dmmptg	|- ( A. z e. K { a e. L | [. X / x ]. [. Y / y ]. ph } e. _V -> dom ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) = K )
18	16 17	syl	|- ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> dom ( z e. K |-> { a e. L | [. X / x ]. [. Y / y ]. ph } ) = K )
19	13 18	eqtrd	|- ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> dom ( X O Y ) = K )