Theorem ndmaovcl

Description: The "closure" of an operation outside its domain, when the operation's value is a set in contrast to ndmovcl where it is required that the domain contains the empty set ( (/) e. S ). (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypotheses	ndmaov.1	|- dom F = ( S X. S )
	ndmaovcl.2	|- ( ( A e. S /\ B e. S ) -> (( A F B )) e. S )
	ndmaovcl.3	|- (( A F B )) e. _V
Assertion	ndmaovcl	|- (( A F B )) e. S

Proof

Step	Hyp	Ref	Expression
1		ndmaov.1	|- dom F = ( S X. S )
2		ndmaovcl.2	|- ( ( A e. S /\ B e. S ) -> (( A F B )) e. S )
3		ndmaovcl.3	|- (( A F B )) e. _V
4		opelxp	|- ( <. A , B >. e. ( S X. S ) <-> ( A e. S /\ B e. S ) )
5	1	eqcomi	|- ( S X. S ) = dom F
6	5	eleq2i	|- ( <. A , B >. e. ( S X. S ) <-> <. A , B >. e. dom F )
7		ndmaov	|- ( -. <. A , B >. e. dom F -> (( A F B )) = _V )
8		eleq1	|- ( (( A F B )) = _V -> ( (( A F B )) e. _V <-> _V e. _V ) )
9	8	biimpd	|- ( (( A F B )) = _V -> ( (( A F B )) e. _V -> _V e. _V ) )
10		vprc	|- -. _V e. _V
11	10	pm2.21i	|- ( _V e. _V -> (( A F B )) e. S )
12	9 11	syl6com	|- ( (( A F B )) e. _V -> ( (( A F B )) = _V -> (( A F B )) e. S ) )
13	3 7 12	mpsyl	|- ( -. <. A , B >. e. dom F -> (( A F B )) e. S )
14	6 13	sylnbi	|- ( -. <. A , B >. e. ( S X. S ) -> (( A F B )) e. S )
15	4 14	sylnbir	|- ( -. ( A e. S /\ B e. S ) -> (( A F B )) e. S )
16	2 15	pm2.61i	|- (( A F B )) e. S