Theorem oprssdm

Description: Domain of closure of an operation. (Contributed by NM, 24-Aug-1995)

	Ref	Expression
Hypotheses	oprssdm.1	$$⊢\neg \varnothing \in S$$
	oprssdm.2	$$⊢\left(x\in S\wedge y\in S\right)\to xFy\in S$$
Assertion	oprssdm	$$⊢S\times S\subseteq \mathrm{dom}F$$

Proof

Step	Hyp	Ref	Expression
1		oprssdm.1	$$⊢\neg \varnothing \in S$$
2		oprssdm.2	$$⊢\left(x\in S\wedge y\in S\right)\to xFy\in S$$
3		relxp	$$⊢\mathrm{Rel}\left(S\times S\right)$$
4		opelxp	$$⊢⟨x,y⟩\in \left(S\times S\right)\leftrightarrow \left(x\in S\wedge y\in S\right)$$
5		df-ov	$$⊢xFy=F\left(⟨x,y⟩\right)$$
6	5 2	eqeltrrid	$$⊢\left(x\in S\wedge y\in S\right)\to F\left(⟨x,y⟩\right)\in S$$
7		ndmfv	$$⊢\neg ⟨x,y⟩\in \mathrm{dom}F\to F\left(⟨x,y⟩\right)=\varnothing$$
8	7	eleq1d	$$⊢\neg ⟨x,y⟩\in \mathrm{dom}F\to \left(F\left(⟨x,y⟩\right)\in S\leftrightarrow \varnothing \in S\right)$$
9	1 8	mtbiri	$$⊢\neg ⟨x,y⟩\in \mathrm{dom}F\to \neg F\left(⟨x,y⟩\right)\in S$$
10	9	con4i	$$⊢F\left(⟨x,y⟩\right)\in S\to ⟨x,y⟩\in \mathrm{dom}F$$
11	6 10	syl	$$⊢\left(x\in S\wedge y\in S\right)\to ⟨x,y⟩\in \mathrm{dom}F$$
12	4 11	sylbi	$$⊢⟨x,y⟩\in \left(S\times S\right)\to ⟨x,y⟩\in \mathrm{dom}F$$
13	3 12	relssi	$$⊢S\times S\subseteq \mathrm{dom}F$$