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	|- ( ( x e. S /\ y e. S ) -> (( x F y )) e. S )
Assertion	aoprssdm	|- ( S X. S ) C_ dom F

Proof

Step	Hyp	Ref	Expression
1		aoprssdm.1	|- ( ( x e. S /\ y e. S ) -> (( x F y )) e. S )
2		relxp	|- Rel ( S X. S )
3		opelxp	|- ( <. x , y >. e. ( S X. S ) <-> ( x e. S /\ y e. S ) )
4		df-aov	|- (( x F y )) = ( F ''' <. x , y >. )
5	4 1	eqeltrrid	|- ( ( x e. S /\ y e. S ) -> ( F ''' <. x , y >. ) e. S )
6		afvvdm	|- ( ( F ''' <. x , y >. ) e. S -> <. x , y >. e. dom F )
7	5 6	syl	|- ( ( x e. S /\ y e. S ) -> <. x , y >. e. dom F )
8	3 7	sylbi	|- ( <. x , y >. e. ( S X. S ) -> <. x , y >. e. dom F )
9	2 8	relssi	|- ( S X. S ) C_ dom F