Metamath Proof Explorer

Theorem ndmovass

Description: Any operation is associative outside its domain, if the domain doesn't contain the empty set. (Contributed by NM, 24-Aug-1995)

Ref Expression
Hypotheses ndmov.1 
|- dom F = ( S X. S )
ndmov.5 
|- -. (/) e. S
Assertion ndmovass 
|- ( -. ( A e. S /\ B e. S /\ C e. S ) -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )

Proof

Step Hyp Ref Expression
1 ndmov.1 
 |-  dom F = ( S X. S )
2 ndmov.5 
 |-  -. (/) e. S
3 1 2 ndmovrcl 
 |-  ( ( A F B ) e. S -> ( A e. S /\ B e. S ) )
4 3 anim1i 
 |-  ( ( ( A F B ) e. S /\ C e. S ) -> ( ( A e. S /\ B e. S ) /\ C e. S ) )
5 df-3an 
 |-  ( ( A e. S /\ B e. S /\ C e. S ) <-> ( ( A e. S /\ B e. S ) /\ C e. S ) )
6 4 5 sylibr 
 |-  ( ( ( A F B ) e. S /\ C e. S ) -> ( A e. S /\ B e. S /\ C e. S ) )
7 1 ndmov 
 |-  ( -. ( ( A F B ) e. S /\ C e. S ) -> ( ( A F B ) F C ) = (/) )
8 6 7 nsyl5 
 |-  ( -. ( A e. S /\ B e. S /\ C e. S ) -> ( ( A F B ) F C ) = (/) )
9 1 2 ndmovrcl 
 |-  ( ( B F C ) e. S -> ( B e. S /\ C e. S ) )
10 9 anim2i 
 |-  ( ( A e. S /\ ( B F C ) e. S ) -> ( A e. S /\ ( B e. S /\ C e. S ) ) )
11 3anass 
 |-  ( ( A e. S /\ B e. S /\ C e. S ) <-> ( A e. S /\ ( B e. S /\ C e. S ) ) )
12 10 11 sylibr 
 |-  ( ( A e. S /\ ( B F C ) e. S ) -> ( A e. S /\ B e. S /\ C e. S ) )
13 1 ndmov 
 |-  ( -. ( A e. S /\ ( B F C ) e. S ) -> ( A F ( B F C ) ) = (/) )
14 12 13 nsyl5 
 |-  ( -. ( A e. S /\ B e. S /\ C e. S ) -> ( A F ( B F C ) ) = (/) )
15 8 14 eqtr4d 
 |-  ( -. ( A e. S /\ B e. S /\ C e. S ) -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )