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	|- ( A. a e. D A. b e. E ( a F b ) =/= (/) -> ( ( D X. E ) C_ dom F /\ Fun ( F |` ( D X. E ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( p = <. a , b >. -> ( F ` p ) = ( F ` <. a , b >. ) )
2		df-ov	|- ( a F b ) = ( F ` <. a , b >. )
3	1 2	eqtr4di	|- ( p = <. a , b >. -> ( F ` p ) = ( a F b ) )
4	3	neeq1d	|- ( p = <. a , b >. -> ( ( F ` p ) =/= (/) <-> ( a F b ) =/= (/) ) )
5	4	ralxp	|- ( A. p e. ( D X. E ) ( F ` p ) =/= (/) <-> A. a e. D A. b e. E ( a F b ) =/= (/) )
6		fvn0ssdmfun	|- ( A. p e. ( D X. E ) ( F ` p ) =/= (/) -> ( ( D X. E ) C_ dom F /\ Fun ( F |` ( D X. E ) ) ) )
7	5 6	sylbir	|- ( A. a e. D A. b e. E ( a F b ) =/= (/) -> ( ( D X. E ) C_ dom F /\ Fun ( F |` ( D X. E ) ) ) )