Metamath Proof Explorer


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 domF=S×S
Assertion ndmaovcom ¬ASBSAFB=BFA

Proof

Step Hyp Ref Expression
1 ndmaov.1 domF=S×S
2 opelxp ABS×SASBS
3 1 eqcomi S×S=domF
4 3 eleq2i ABS×SABdomF
5 2 4 bitr3i ASBSABdomF
6 ndmaov ¬ABdomFAFB=V
7 5 6 sylnbi ¬ASBSAFB=V
8 ancom ASBSBSAS
9 opelxp BAS×SBSAS
10 3 eleq2i BAS×SBAdomF
11 8 9 10 3bitr2i ASBSBAdomF
12 ndmaov ¬BAdomFBFA=V
13 11 12 sylnbi ¬ASBSBFA=V
14 7 13 eqtr4d ¬ASBSAFB=BFA