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	|- dom F = ( S X. S )
Assertion	ndmaovcom	|- ( -. ( A e. S /\ B e. S ) -> (( A F B )) = (( B F A )) )

Proof

Step	Hyp	Ref	Expression
1		ndmaov.1	|- dom F = ( S X. S )
2		opelxp	|- ( <. A , B >. e. ( S X. S ) <-> ( A e. S /\ B e. S ) )
3	1	eqcomi	|- ( S X. S ) = dom F
4	3	eleq2i	|- ( <. A , B >. e. ( S X. S ) <-> <. A , B >. e. dom F )
5	2 4	bitr3i	|- ( ( A e. S /\ B e. S ) <-> <. A , B >. e. dom F )
6		ndmaov	|- ( -. <. A , B >. e. dom F -> (( A F B )) = _V )
7	5 6	sylnbi	|- ( -. ( A e. S /\ B e. S ) -> (( A F B )) = _V )
8		ancom	|- ( ( A e. S /\ B e. S ) <-> ( B e. S /\ A e. S ) )
9		opelxp	|- ( <. B , A >. e. ( S X. S ) <-> ( B e. S /\ A e. S ) )
10	3	eleq2i	|- ( <. B , A >. e. ( S X. S ) <-> <. B , A >. e. dom F )
11	8 9 10	3bitr2i	|- ( ( A e. S /\ B e. S ) <-> <. B , A >. e. dom F )
12		ndmaov	|- ( -. <. B , A >. e. dom F -> (( B F A )) = _V )
13	11 12	sylnbi	|- ( -. ( A e. S /\ B e. S ) -> (( B F A )) = _V )
14	7 13	eqtr4d	|- ( -. ( A e. S /\ B e. S ) -> (( A F B )) = (( B F A )) )