Theorem aovprc

Description: The value of an operation when the one of the arguments is a proper class, analogous to ovprc . (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypothesis	aovprc.1	$$⊢\mathrm{Rel}\mathrm{dom}F$$
Assertion	aovprc	$$⊢\neg \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to ((AFB))=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		aovprc.1	$$⊢\mathrm{Rel}\mathrm{dom}F$$
2		df-aov	$$⊢((AFB))=\left(F\mathrm{\text{'}\text{'}\text{'}}⟨A,B⟩\right)$$
3		df-br	$$⊢A\mathrm{dom}FB\leftrightarrow ⟨A,B⟩\in \mathrm{dom}F$$
4	1	brrelex12i	$$⊢A\mathrm{dom}FB\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
5	3 4	sylbir	$$⊢⟨A,B⟩\in \mathrm{dom}F\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
6		ndmafv	$$⊢\neg ⟨A,B⟩\in \mathrm{dom}F\to \left(F\mathrm{\text{'}\text{'}\text{'}}⟨A,B⟩\right)=\mathrm{V}$$
7	5 6	nsyl5	$$⊢\neg \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}}⟨A,B⟩\right)=\mathrm{V}$$
8	2 7	eqtrid	$$⊢\neg \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to ((AFB))=\mathrm{V}$$