Theorem ndmaovcom

Description: Any operation is commutative outside its domain, analogous to ndmovcom . (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypothesis	ndmaov.1	$$⊢\mathrm{dom}F=S\times S$$
Assertion	ndmaovcom	$$⊢\neg \left(A\in S\wedge B\in S\right)\to ((AFB))=((BFA))$$

Proof

Step	Hyp	Ref	Expression
1		ndmaov.1	$$⊢\mathrm{dom}F=S\times S$$
2		opelxp	$$⊢⟨A,B⟩\in \left(S\times S\right)\leftrightarrow \left(A\in S\wedge B\in S\right)$$
3	1	eqcomi	$$⊢S\times S=\mathrm{dom}F$$
4	3	eleq2i	$$⊢⟨A,B⟩\in \left(S\times S\right)\leftrightarrow ⟨A,B⟩\in \mathrm{dom}F$$
5	2 4	bitr3i	$$⊢\left(A\in S\wedge B\in S\right)\leftrightarrow ⟨A,B⟩\in \mathrm{dom}F$$
6		ndmaov	$$⊢\neg ⟨A,B⟩\in \mathrm{dom}F\to ((AFB))=\mathrm{V}$$
7	5 6	sylnbi	$$⊢\neg \left(A\in S\wedge B\in S\right)\to ((AFB))=\mathrm{V}$$
8		ancom	$$⊢\left(A\in S\wedge B\in S\right)\leftrightarrow \left(B\in S\wedge A\in S\right)$$
9		opelxp	$$⊢⟨B,A⟩\in \left(S\times S\right)\leftrightarrow \left(B\in S\wedge A\in S\right)$$
10	3	eleq2i	$$⊢⟨B,A⟩\in \left(S\times S\right)\leftrightarrow ⟨B,A⟩\in \mathrm{dom}F$$
11	8 9 10	3bitr2i	$$⊢\left(A\in S\wedge B\in S\right)\leftrightarrow ⟨B,A⟩\in \mathrm{dom}F$$
12		ndmaov	$$⊢\neg ⟨B,A⟩\in \mathrm{dom}F\to ((BFA))=\mathrm{V}$$
13	11 12	sylnbi	$$⊢\neg \left(A\in S\wedge B\in S\right)\to ((BFA))=\mathrm{V}$$
14	7 13	eqtr4d	$$⊢\neg \left(A\in S\wedge B\in S\right)\to ((AFB))=((BFA))$$