Theorem brovmptimex

Description: If a binary relation holds and the relation is the value of a binary operation built with maps-to, then the arguments to that operation are sets. (Contributed by RP, 22-May-2021)

	Ref	Expression
Hypotheses	brovmptimex.mpt	$$⊢F=\left(x\in E,y\in G⟼H\right)$$
	brovmptimex.br	$$⊢\phi \to ARB$$
	brovmptimex.ov	$$⊢\phi \to R=CFD$$
Assertion	brovmptimex	$$⊢\phi \to \left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		brovmptimex.mpt	$$⊢F=\left(x\in E,y\in G⟼H\right)$$
2		brovmptimex.br	$$⊢\phi \to ARB$$
3		brovmptimex.ov	$$⊢\phi \to R=CFD$$
4	3 2	breqdi	$$⊢\phi \to A\left(CFD\right)B$$
5		brne0	$$⊢A\left(CFD\right)B\to CFD\ne \varnothing$$
6	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}F$$
7	6	ovprc	$$⊢\neg \left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)\to CFD=\varnothing$$
8	7	necon1ai	$$⊢CFD\ne \varnothing \to \left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)$$
9	4 5 8	3syl	$$⊢\phi \to \left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)$$