Theorem ovn0ssdmfun

Description: If a class' operation value for two operands is not the empty set, the operands are contained in the domain of the class, and the class restricted to the operands is a function, analogous to fvfundmfvn0 . (Contributed by AV, 27-Jan-2020)

	Ref	Expression
Assertion	ovn0ssdmfun	$$⊢\forall a\in D\forall b\in EaFb\ne \varnothing \to \left(D\times E\subseteq \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left(D\times E\right)}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢p=⟨a,b⟩\to F\left(p\right)=F\left(⟨a,b⟩\right)$$
2		df-ov	$$⊢aFb=F\left(⟨a,b⟩\right)$$
3	1 2	eqtr4di	$$⊢p=⟨a,b⟩\to F\left(p\right)=aFb$$
4	3	neeq1d	$$⊢p=⟨a,b⟩\to \left(F\left(p\right)\ne \varnothing \leftrightarrow aFb\ne \varnothing \right)$$
5	4	ralxp	$$⊢\forall p\in \left(D\times E\right)F\left(p\right)\ne \varnothing \leftrightarrow \forall a\in D\forall b\in EaFb\ne \varnothing$$
6		fvn0ssdmfun	$$⊢\forall p\in \left(D\times E\right)F\left(p\right)\ne \varnothing \to \left(D\times E\subseteq \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left(D\times E\right)}\right)\right)$$
7	5 6	sylbir	$$⊢\forall a\in D\forall b\in EaFb\ne \varnothing \to \left(D\times E\subseteq \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left(D\times E\right)}\right)\right)$$