Theorem aoprssdm

Description: Domain of closure of an operation. In contrast to oprssdm , no additional property for S ( -. (/) e. S ) is required! (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypothesis	aoprssdm.1	$$⊢\left(x\in S\wedge y\in S\right)\to ((xFy))\in S$$
Assertion	aoprssdm	$$⊢S\times S\subseteq \mathrm{dom}F$$

Proof

Step	Hyp	Ref	Expression
1		aoprssdm.1	$$⊢\left(x\in S\wedge y\in S\right)\to ((xFy))\in S$$
2		relxp	$$⊢\mathrm{Rel}\left(S\times S\right)$$
3		opelxp	$$⊢⟨x,y⟩\in \left(S\times S\right)\leftrightarrow \left(x\in S\wedge y\in S\right)$$
4		df-aov	$$⊢((xFy))=\left(F\mathrm{\text{'}\text{'}\text{'}}⟨x,y⟩\right)$$
5	4 1	eqeltrrid	$$⊢\left(x\in S\wedge y\in S\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}}⟨x,y⟩\right)\in S$$
6		afvvdm	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}⟨x,y⟩\right)\in S\to ⟨x,y⟩\in \mathrm{dom}F$$
7	5 6	syl	$$⊢\left(x\in S\wedge y\in S\right)\to ⟨x,y⟩\in \mathrm{dom}F$$
8	3 7	sylbi	$$⊢⟨x,y⟩\in \left(S\times S\right)\to ⟨x,y⟩\in \mathrm{dom}F$$
9	2 8	relssi	$$⊢S\times S\subseteq \mathrm{dom}F$$