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	$$⊢\mathrm{dom}F=S\times S$$
	ndmaovcl.2	$$⊢\left(A\in S\wedge B\in S\right)\to ((AFB))\in S$$
	ndmaovcl.3	$$⊢((AFB))\in \mathrm{V}$$
Assertion	ndmaovcl	$$⊢((AFB))\in S$$

Proof

Step	Hyp	Ref	Expression
1		ndmaov.1	$$⊢\mathrm{dom}F=S\times S$$
2		ndmaovcl.2	$$⊢\left(A\in S\wedge B\in S\right)\to ((AFB))\in S$$
3		ndmaovcl.3	$$⊢((AFB))\in \mathrm{V}$$
4		opelxp	$$⊢⟨A,B⟩\in \left(S\times S\right)\leftrightarrow \left(A\in S\wedge B\in S\right)$$
5	1	eqcomi	$$⊢S\times S=\mathrm{dom}F$$
6	5	eleq2i	$$⊢⟨A,B⟩\in \left(S\times S\right)\leftrightarrow ⟨A,B⟩\in \mathrm{dom}F$$
7		ndmaov	$$⊢\neg ⟨A,B⟩\in \mathrm{dom}F\to ((AFB))=\mathrm{V}$$
8		eleq1	$$⊢((AFB))=\mathrm{V}\to \left(((AFB))\in \mathrm{V}\leftrightarrow \mathrm{V}\in \mathrm{V}\right)$$
9	8	biimpd	$$⊢((AFB))=\mathrm{V}\to \left(((AFB))\in \mathrm{V}\to \mathrm{V}\in \mathrm{V}\right)$$
10		vprc	$$⊢\neg \mathrm{V}\in \mathrm{V}$$
11	10	pm2.21i	$$⊢\mathrm{V}\in \mathrm{V}\to ((AFB))\in S$$
12	9 11	syl6com	$$⊢((AFB))\in \mathrm{V}\to \left(((AFB))=\mathrm{V}\to ((AFB))\in S\right)$$
13	3 7 12	mpsyl	$$⊢\neg ⟨A,B⟩\in \mathrm{dom}F\to ((AFB))\in S$$
14	6 13	sylnbi	$$⊢\neg ⟨A,B⟩\in \left(S\times S\right)\to ((AFB))\in S$$
15	4 14	sylnbir	$$⊢\neg \left(A\in S\wedge B\in S\right)\to ((AFB))\in S$$
16	2 15	pm2.61i	$$⊢((AFB))\in S$$